http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
천윤식(Yoonsik Cheon) 한국정보과학회 1995 한국정보과학회 학술발표논문집 Vol.22 No.2B
정형적 인터페이스 명세는 프로그램 모듈에 관한 모호성이 배제된 정확한 문서이다. 정형성은 명세 언어와 같은 정형적 표기법이 수학을 바탕으로하는 정형적 의미를 갖고 있기 때문에 가능하다. 본 논문에서는 양층형 방식의 Larch 인터페이스 명세 언어의 정형적 의미론을 정립한다. 특히 객체지향을 지원하는 Larch/Smalltalk을 중심으로 하여 모델지향적 및 증명론적 의미을 정의한다. 모델지향적 방법은 직관적이고 풍부한 수학적 이론을 바탕으로 하기 때문에 명세의 의미를 쉽게 파악할 수 있게 한다. 반면 증명론적 방법은 정형적 분석 및 증명을 위한 토대를 제공한다. 즉, 주어진 프로그램이 명세를 만족하는가 하는 정형적 증명 및 프로그램에 관한 추론을 용이하게 한다.
천윤식(Yoonsik Cheon),조수선(Soosun Cho) 한국정보과학회 1996 한국정보과학회 학술발표논문집 Vol.23 No.2B
ISO에서 표준으로 정한 정형적 명세언어 LOTOS의 객체지향 확장에 관한 기초 연구를 소개한다. LOTOS의 객체지향 확장 배경을 살펴보고 예제를 중심으로 하여 객체지향 LOTOS의 기본골격과 핵심적인 설계 방향을 제시한다. OOLOTOS는 클래스를 기반으로 하며 객체, 메세지 전달, 상속, 정제 등의 개념을 지원한다. OOLOTOS의 가장 큰 특징은 LOTOS의 비파괴적 확장, 정제 방식의 정형방법 지원, 객체지향 개념하에서 자료와 제어의 통합이다.
천윤식(Yoonsik Cheon),김철홍(Cheolhong Kim),박원규(Wonkyu Park),김강호(Kangho Kim),정연대(Yeondae Chung) 한국정보과학회 1997 한국정보과학회 학술발표논문집 Vol.24 No.1A
ISO 표준 정형 명세 언어 LOTOS는 사용자의 요구사항이나 시스템 모형을 추상적이고 정형적으로 작성할 수 있도록한다. 반면, 명세로부터 구현을 직접 도출하기는 쉽지 않다. 따라서 추상 명세를 실현가능한 코드로 정제하는 자동화 지원도구가 절실히 필요하며, LOTOS가 산업계에서 받아들여 지고 실제로 사용되는데 지대한 공헌을 할 것으로 기대된다. 본 논문에서는 현재 시스템공학연구소에서 수행하고 있는 LOTOS 코드 생성기 개발 사례를 소개한다.
조수선(Soosun Cho),천윤식(Yoonsik Cheon),오영배(Youngbae Oh),정연대(Yun Dae Chung) 한국정보과학회 2000 정보과학회 컴퓨팅의 실제 논문지 Vol.6 No.2
본 논문에서는 ForTIA라 불리는 LOTOS 지원도구의 개발을 소개한다. ISO 표준 정형 명세언어인 LOTOS는 사용자의 요구사항이나 시스템 모형을 추상화하여 정형적으로 작성할 수 있도록 함으로써 구현에 이르기 전에 명세 상에서 시스템을 확인 및 검증할 수 있게 한다. ForTIA는 LOTOS 정형기법이 산업계에 적용될 수 있도록 확인 위주의 경량 정형기법 기능을 제공한다. ForTIA의 핵심적인 기능은 명세 시뮬레이션과 C++ 코드 생성이다. 시뮬레이션은 편리하고 직관적인 상호작용을 위한 트리 기반의 시각적 명세확인 메카니즘을 제공하고 C++코드생성은 LOTOS로부터 완전한 C++ 코드를 생성하여 시스템의 실제 구현에 이용될 수 있도록 한다. In this paper, we introduce the development of a LOTOS-based tool, supporting formal methods, called ForTIA (A Formalism for Telecommunication and Information Systems). By using LOTOS, an ISO standard formal specification language, the user requirements and system models can be abstracted and represented formally. Therefore, the system can be validated and verified on the specifications, before implementations. ForTIA supports light-weight formal methods based on validation to be used in real industry. Key functions of ForTIA are simulation and C++ code generation. In simulation, tree based visual validation mechanism is provided and in code generation, the full C++ source code is generated to be used for system implementations.