대수명세의 구현과 증분식 테스팅

김규년(Kyoo Nyun Kim),우치수(Chi Su Wu) 한국정보과학회 1990 한국정보과학회 학술발표논문집 Vol.17 No.2

추상자료형이 대수명세로 기술된 경우 이를 단계적으로 구현하기 위한 중간자료형 glist를 정의하고, glist를 이용하여 입력명세가 고급언어로 변환되었을 때 명세의 일관성과 완전성(sufficient-completeness)을 증명하기 위한 증분식 테스팅(incremental testing) 기법을 제안하였다. 이를 위하여 입력 대수명세를 B명세, BE명세, BD명세등으로 분류하고, 자동적으로 생성가능한 기본적인 테스트자료(test case)를 분류된 각 명세의 귀납법의 기본단계의 증명에 이용하고 그 결과를 귀납단계에서의 수동 증명에 사용한다. 단계적으로 구현된 명세를 테스팅 및 각종 특징의 증명에 이용함으로써 작성된 명세가 의도대로 동작하는지의 여부를 파악하여 소프트웨어 생명주기에서의 명세설계 단계의 오류를 쉽게 찾아낼 수 있으므로 생산비용의 절감 효과를 가져올 수 있다.

대수명세의 단계적 구현과 증분식 테스팅

김규년(Kyoo Nyun Kim),우치수(Chi Su Wu) 한국정보과학회 1991 정보과학회논문지 Vol.18 No.1

추상자료형이 대수명세로 기술된 경우 이를 단계적으로 구현하기 위한 중간자료형 glist를 정의하고, glist를 이용하여 입력명세가 고급언어로 변환되었을 때 명세의 일관성의 완전성(sufficient-completeness)을 증명하기 위한 증분식 테스팅(incremental testing) 기법을 제안하였다. 이를 위하여 대수명세를 B명세, BE명세, BD명세 등으로 분류하고, 자동적으로 생성가능한 기본적인 테스트자료(test case)를 분류된 각 명세의 귀납법의 기본단계의 증명에 이용하고 그 결과를 귀납단계에서의 수동 증명에 사용한다. 단계적으로 구현된 명세를 테스팅 및 각종 특징의 증명에 이용함으로써 작성된 명세가 의도대로 동작하는지의 여부를 파악하여 소프트웨어 생명주기에서의 명세설계 단계의 오류를 쉽게 찾아낼 수 있으므로 생산비용의 절감 효과를 가져올 수 있다. In this paper, we define an intermediate abstract data type, glist for the stepwise implementation of the algerbraic specification of an abstract data type. And we presented an incremental testing technique for the proof of the consistency and sufficient-completeness of the given abstract data type when it is implemented via glist. For that purpose we classified given algebraic specification as B-specification, BE-specification and BD-specification and used basic test cases, which can be generated, in the proof of the basic step of the induction and the result in that of the induction step. By the use of the stepwise implementation in the proof and testing of some property of abstract data type, we can demonstrate the specification whether it works as the designer's intent and can debug some errors in the early step of the software life cycle, thus the cost of the software construction can be reduced.

추상자료형 기술을 위한 대수명세의 새로운 접근 방법

김규년(Kyoo Nyun Kim),우치수(Chi Su Wu) 한국정보과학회 1990 정보과학회논문지 Vol.17 No.3

추상자료형(abstract data types)을 기술하기 편리한 결정적 대수명세(determistic algeleraic specification)기법을 제안하였다. 결정적 대수명세란 공리의 수행규칙이 명시된 명세로서, 이를 이용하면 명세의 일관성이 보장되고, 유한종료성 및 sufficient-completeness가 증명될수 있다는 것을 보였으며, 이들의 증명과정을 자동화 시킬 수 있는 알고리즘을 제시하였다. 결정적대수명세는 전통적인 컴퓨터의 순차적인 실행방식을 모방하면서 명세를 형식적으로 기술할 수 있으므로 추상자료형을 이용한 소프트웨어 개발에 효과적으로 응용될 수가 있다. 명세의 sufficient-completeness 및 유한종료성을 증명하기 위하여 본 논문에서 제시한 귀납적완전성을 점검하는 알고리즘은 공리식이 충분하게 기술되지 않은 사실 또는 불필요한 공리를 발견해 낼 수 있으므로 소프트웨어 생명주기의 명세작성단계에서 지원도구로 사용되어 질 수 있다. A deterministic algebraic specification technique which can be used to describe abstract data types easily is presented. A deterministic algebraic specification is a specification of which applying sequence of axioms are determined We show the fact that the consistency is affirmative and that the sufficient-completeness and finite termination of a specification described by deterministic algebra can be proved and present some algorithms to automate the proof processes. A deterministic algebraic specification can be used in software construction with abstract data type because it mimics the sequential execution model of the conventional computers and may be used to describe a specification formally The induction completeness testing algorithm presented in this paper to prove sufficient-completeness and finite termination can be used as an assistant tool in the specification design step of the software life cycle, because it can detect some axioms over or under specified.

수정된 CODARTS 방법론에서의 실시간 병렬 태스크 자동 구성

김규년(Kyoo-Nyun Kim),정민포(Min-Po Jung),이종구(Jong-Gu Lee) 한국정보과학회 1999 정보과학회논문지(B) Vol.26 No.1

실시간 소프트웨어 설계 시에는 시스템을 분석하고 순차적인 실행 단위인 모듈들을 병렬 태스크로 구성하게 된다. 시스템 분석의 결과로 Real-Time Structured Analysis(RTSA) 표기법으로 표현된 Control flow and Data flow Diagram(C&DFD)이 산출물로 나오게 되고 이들을 이용하여 성능에 문제가 생기지 않을 조건 하에서 병렬 태스크로 구성하게 된다. 이러한 병렬 태스크들의 구성 방법이 Gomaa에 의해 제안된 COncurrent Design Approach for Real-Time System(CODARTS)에서 태스크 구조화 지침(Task Structuring Criteria)으로 제시되어 있다. 그러나, 이러한 구조화 지침은 설계자의 경험에 전적으로 의존하기 때문에 이를 이용하여 시스템을 설계하기가 어려운 것이 현실이다. 또한 CODARTS 방법론 자체가 내용이 광범위하고 추상적이기 때문에 설계된 시스템이 해석자마다 다른 관점에서 이해될 수 있고 설계의 일관성이 결여될 수 있다. 본 연구에서는 이미 존재하는 CODARTS 방법론을 적용단계별로 정리하여 개정된 CODARTS 구조와 보완된 태스크 구성 단계를 제안하여 단일한 설계를 도출해내고 일관적인 해석이 가능하도록 하였다. 이러한 개정된 CODARTS 구조와 태스크 구성 단계들은 실시간 병렬 소프트웨어 시스템의 설계를 자동화하는데 이용될 수 있다. 결론으로서 개정된 CODARTS의 구조와 태스크 구성 단계들을 적용한 태스크 구성 예를 제시하고 기존의 방법보다 개선된 점을 제시한다. When we design real-time software target system is analyzed and then we structure sequential executive modules into concurrent tasks. As a result of the analysis, control flow and data flow diagram based on the RTSA notation is produced. This diagram is structured into concurrent tasks under the condition that performance problem is not serious. The criteria structuring concurrent tasks are introduced as COncurrent Design Approach for Real-Time System(CODARTS) by Gomaa. But structuring concurrent tasks using the criteria of CODARTS is somewhat difficult because the criteria are dependent on designer's experience. CODARTS is an wide-range and abstract methodology. As a result, the design can be inconsistent and peoples can understand it differently. In this paper, we restructure the CODARTS methodology, propose a revised CODARTS structure and represent the task structuring steps for this new framework to overcome the understanding and inconsistency problems. The revised CODARTS framework and task structuring steps can be used to automate the design of real time concurrent software systems. Finally, we show an example of task structuring in revised CODARTS framework.

대수명세기법의 새로운 접근방법

김규년(Kyoo Nyun Kim),우치수(Chi Su Wu) 한국정보과학회 1990 한국정보과학회 학술발표논문집 Vol.17 No.1

본 논문에서는 추상자료형(abstract data type)을 기술하기 편리하며 명세의 일관성 및 완전성을 쉽게 증명할 수 있는 결정적대수 명세(determistic algeleraic specification)기법을 제안하였다. 공리의 수행규칙이 명시된 결정적 대수명세를 이용하면 명세의 유한종료성, 일관성 및 sufficient-completeness가 증명될 수 있다는 것을 보였고, 이들을 자동화 시킬 수 있는 알고리즘을 제시하였다. 결정적대수명세는 전통적인 컴퓨터의 순차적인 실행방식을 모방하면서 명세를 형식적으로 기술할 수 있으므로 추상자료형을 이용한 소프트웨어 개발및 자동프로그래밍에 효과적으로 응용될 수가 있다. 명세의 일관성및 유한종료성을 증명하기 위하여 본 논문에서 제시한 귀납적완전성을 점검하는 알고리즘을 이용하면 잘못 작성되거나 불필요한 공리를 발견해 낼 수 있으므로 소프트웨어 생명주기의 설계단계에서 명세작성 지원도구로 사용되어 질 수 있다.

Knuth - Bendix Ordering을 이용한 대수명세의 유한 종료성 증명

김규년(Kyoo Nyun Kim),우치수(Chi Su Wu) 한국정보과학회 1991 한국정보과학회 학술발표논문집 Vol.18 No.1

추상자료형이 대수명세로 기술된 경우 이의 일관성과 완전성을 증명하기 위해서는 먼저 유한 종류(finite termination) 하는지를 증명하여야 한다. 본 논문에서는 Kunth-Bendix completion procedure를 이용하여 대수명세의 여러가지 특징을 증명하려 할 때 반드시 필요한 유한 종료성을 증명하는 방법을 제안하고 그 알고리즘을 제시하였다. Knuth-Bendix 방법으로 유한 종료성을 증명하고자 할 때 연산자의 우선순위가 total ordering을 가질 필요가 없다는 점에 착안하여 먼저 각 항의 가중치를 구하여 서로 비교한 결과 이들이 같은 경우에 연산자의 우선 순위를 검사하는 방법으로서 연산자의 우선 순위가 partial orderiong이더라도 Kunth-Bendix 방법과 같은 효과를 발휘할 수 있으면서 실행시간이 적게 소모되는 장점이 있다.

PLC 기반 제어 시스템을 테스트하기 위한 프로그램 시뮬레이터의 설계 및 구현

정민포(Min-Po Jung),김규년(Kyoo-Nyun Kim) 한국정보과학회 1999 한국정보과학회 학술발표논문집 Vol.26 No.2Ⅲ

산업현장에서의 자동화를 구축하기 위한 핵심 요소는 생산 현장의 제어장치를 직접 제어하는 PLC(Programmable Logical Controller)로 구성된다. PLC를 이용하여 생산 현장의 자동화를 구축하는 기존의 방법론은 대부분의 경우에서 현장의 자동화 구축 기간을 길고 비용이 많이 든다. 또한 이미 구축된 시스템에서 정밀한 테스트를 할 경우, 잘못된 동작으로 인해 발생하는 실제 현장에 설치된 제어장치의 손상될 확률이 높아진다. 본 논문에서는 기존 방법론에서 언급되는 문제점들을 프로그램의 컴포넌트(요소)로 개발하고 개선된 방법론을 이용할 수 있는 프로그램 시뮬레이터를 설계 및 구현한다. 프로그램 시뮬레이터의 개발 효과는 기존 방법론의 문제점들을 해결함으로써 생산성을 높일 수 있고 생산비용을 줄일 수 있다.

컴퓨터음악을 위한 국악보(정간보) 처리 시스템의 설계와 구현

김기영(Ki-Young Kim),김규년(Kyoo-Nyun Kim) 한국정보과학회 2001 한국정보과학회 학술발표논문집 Vol.28 No.1B

각 나라마다 고유한 음악이 있으며 또한 그 음악을 표현하는 전통적인 방식이 존재한다. 그러나 서양음식의 도입으로 우리음악의 표현까지도 서양화가 되어있다. 전통음악을 원형대로 보존하기 위해서는 선조들이 사용하였던 기보법을 사용하는 것이 올바른 일이라고 여겨지므로, 우리나라의 전통악보 중 그 우수성이 인정되는 정간보를 컴퓨터를 통하여 편리하게 처리 할 수 있는 시스템을 개발하였다. 정간보에는 악기마다 서로 다른 표현 방법들이 존재하므로, 이번 시스템은 그 중에서 단소를 위한 정간보 처리를 주된 목표로, 컴퓨터를 이용한 기보법과 오선보로의 변환, 그리고 미디신호로의 변환과 연주를 중점으로 개발하였다.

PLC를 이용한 Portainer Crane의 고장진단 시스템의 개발

최제헌(Jae-Heon Choi),김규년(Kyoo-Nyun Kim),Anatoly Tuzovsky(Anatoly Tuzovsky),정민포(Min-Po Jung),추경환(Gyung-Hwan Chu),이종구(Jong-Gu Lee),엄진아(Jin-Ah Um),정태동(Tae-Dong Jung),김종훈(Jong-Hun Kim),박근현(Gun-Hyun Pak) 한국정보과학회 1995 한국정보과학회 학술발표논문집 Vol.22 No.1

본 논문에서는, 항만에서 사용되고 있는 Portainer Crane의 고장진단 시스템을 객체지향기법으로 설계 및 구현한 내용과, 그 결과를 제시한다. Crane의 각 접점들의 상태를 제어하는 PLC(Programmable Logic controller)를 PC와 RS-232c Serial port로 서로 연결해서 정해진 통신 protocol을 사용하여 Crane의 상태를 진단한다. PLC와의 통신부분은 driver방식으로 구성하여 다른 종류의 PLC도 쉽게 적용할 수 있도록 설계하였다. 주기적으로 PLC로부터 Crane의 각 부분들의 상태를 어떤 시간제한내에 모니터링하기 위해서, 본 시스템은 1개의 생성프로세스와 3개의 프로세스로 구성되었다. 실제 작업을 수행하는것은 Display manager, Disk manager, Signal manager의 3개 프로세스이다. 개발환경은, 다중프로세스와 이후의 네트워크 이용을 고려하여 Windows NT 3.5 환경에서 Visual C++ 2.0을 사용하였다.

Motif GUI Workshop을 위한 Widget Dictionary의 설계

정민포(Min-Po Jung),김규년(Kyoo-Nyun Kim),정기룡(Ki-Ryong Jung),최제헌(Jae-Heon Choi) 한국정보과학회 1994 한국정보과학회 학술발표논문집 Vol.21 No.2A

Motif 프로그래밍 환경이 지원하는 가장 중요한 사항 중의 하나가 GUI(Graphical User Interface)의 구현이다. Motif가 제공하는 GUI의 요소들은 많이 있으나 이를 쉽게 이용하기 위한 도구가 부족하다. 본 논문에서는 보다 쉬운 인터페이스를 가지는 GUI 도구를 제공하기 위한 workshop을 제안하고 이것의 바탕이 되는 widget dictionary에 대하여 중점적으로 논한다. 이 widget dictionary는 Motif가 제공하는 widget set[2]을 시각적인 방법과 GUI를 위한 특성에 따라 분류하여 사용자가 효율적으로 접근할 수 있도록 한다.