본 논문에서는 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.
