In this thesis, we propose a formal object-oriented software development method for concurrent real-time discrete event systems. The systems consist of multiple running modules with real-time constraints, and their state transitions depend wholly on the occurrence of asynchronous discrete events over time. Typical examples include various applications such as communication networks and flexible manufacturing systems. To develop a theoretical underpinning for those systems, we face the difficult challenge of creating a set of unified theories and technologies that will allow us to reason about the correctness, timeliness, and reliability at each level of abstraction and to combine the results of each level into results for the integrated system. As one approach for developing the underpinning, formal methods have been studied in various research communities. A formal method enables ambiguities to be avoided and makes a more rigid process possible because the requirements and characteristics of a system are well defined by formal specification.
DEVS (Discrete Event System Specification) is a set-theoretic formalism devised for specifying discrete event systems. We propose an extended DEVS formalism, called real-time DEVS, for formal real-time software development by employing activities and by augmenting the underlying time base to time intervals. Also, we propose the DEVS-based framework for real-time software development, which encompasses the range of development stages from model construction, through simulation, to generation of executable high-level language codes which can run on real-time execution environments. For a simulation stage, we use the conventional DEVS formalism and implement its simulation engine, DEVS++ Simulator. For an execution stage, we propose abstract executive algorithms which are the conceptual basis of our execution engine, DEVS++ Executive. As an intermediate stage between the simulation and execution stages, we add an analysis stage verifying the worst-case timing and state trajectory for preventing a system from entering unsafe states. Because of the inevitable discrepancy between simulation and execution, in the worst case, the state trajectory and timing of simulation models may differ from those of execution models. Thus, the analysis scheme of real-time DEVS models makes it possible to predict the minimum and maximum time bound as well as to generate state trajectories. We propose a hierarchical real-time analysis method which generates a reachability graph hierarchically for saving system resources. Experimental results show that our method can save about 90% memory and time than a conventional reachability graph generation scheme. As other stages, we develop an analysis engine of real-time DEVS, DEVS++ Analyzer, which implements the method. DEVS++ consists of three engines which are all implemented in C++: DEVS++ Simulator, DEVS++ Analyzer, and DEVS++ Executive. Because DEVS++ provides consistent APIs for the three engines, a modeler can simulate, analyze, and execute DEVS-based models just by adding a couple of functions without changing existing codes. This engine is tightly coupled with its visual framework, named DEVShop, which is a formal system development tool based not only on the DEVS formalism but also on extended DEVS formalisms such as real-time DEVS, for supporting rapid prototyping and automatic code generation. DEVShop covers the construction, simulation, analysis, and execution of models by providing graphical model designers, a project manager, model checkers, an automatic code generator, and an interactive tracer. It enables a modeler to validate a complex design early in the design process by simulation and analysis, thereby avoiding costly remodeling process. Also, it shortens the development time of a system by automatically generating code that can be used to implement the design as concurrent real-time software. As a result, due to the framework, once verified implementation mechanisms have been put in place, high-level formal models can be brought to bear on actual implementation in a tractable way. We give an elevator control system as an example of our method.
이 논문에서, 우리는 병행 실시간 이산 사건 시스템을 위한, 정형적인 객체 지향 소프트웨어 개발 방법을 제안한다. 이 시스템은 실시간 제한들을 가진 동시에 실행되는 모듈들로 구성되어 있고, 시스템의 상태 전이는 비동기적으로 발생하는 이산 사건들에 의해 이루어진다. 이와 같은 시스템의 일반적인 예로서는 통신 네트워크, 생산 공정 시스템등이 있다. 병행 실시간 이산 사건 시스템 개발의 이론적인 기반을 세우기 위해서는, 각 추상화된 레벨에서의 정확성, 적시성, 신뢰도의 검증이 가능하고, 각 레벨의 결과를 결합하여 통합된 시스템을 개발할수 있도록 하는, 통합된 이론과 기술의 개발이 필요하다. 이를 위한 한가지 방법으로 여러 연구 그룹에서 정형적 방법에 대한 연구가 진행되어 왔다. 정형적 방법은 시스템의 요구 사항과 특성의 명세에 모호성이 생기지 않도록 하여, 보다 강건한 개발 과정이 이루어지게 한다.
DEVS (Discrete Event System Specification)는 이산 사건 시스템을 기술하기 위해 고안된 집합 이론에 기반한 형식론이다. 우리는 DEVS에 activity를 도입하고, 시간 기반을 시간 구간으로 확장하여, 정형적인 실시간 소프트웨어 개발에 적용할수 있는 real-time DEVS를 제안한다. 또한, 우리는 모델의 개발, 모의 실험, 실시간 실행 환경에서 수행 가능한 상위 레벨 코드의 생성등의 전 과정을 포함한, DEVS 기반 틀을 제안한다. 모의 실험 단계를 위해, 우리는 DEVS 형식론을 사용하며, DEVS++ Simulator 라는 모의 실험 엔진을 개발하였다. 실행 단계를 위해, 우리는 DEVS++ Executive를 개발하였고, 이 엔진의 개념적 기반인 추상 실행 알고리즘을 제안한다. 모의 실험 단계와 실행 단계의 중간 단계로서, 우리는 시스템이 불안정한 상태로 전이하는 것을 막기 위해, 최악의 시간과 상태 궤도를 검증하기 위한, 분석 단계를 제안한다. 모의 실험과 실행의 피할수 없는 불일치때문에, 최악의 경우, 모의 실험 모델과 실행 모델간의 상태 궤도와 시간은 다를수 있다. 그러므로, real-time DEVS 모델의 분석 단계는 시스템의 최대 최소의 실행 시간과 상태 궤도를 예측할수 있도록 한다. 우리는 시스템 자원을 절약하기 위해 도달성 그래프를 계층적으로 생성시키는 계층적 실시간 검증 방법을 제안한다. 실험 결과에 의하면, 우리의 방법은 일반적인 도달성 그래프 생성 방법이 사용하는 자원의 90% 정도를 절약할수 있다. 다른 단계에서와 같이, 우리는 real-time DEVS의 분석 엔진으로서, 제안된 방법을 구현한 DEVS++ Analyzer를 개발하였다. DEVS++는 이와 같이 세가지 엔진들 --- DEVS++ Simulator, DEVS++ Analyzer, 그리고 DEVS++ Executive --- 로 구성된 통합 엔진이다. DEVS++는 이 세가지 엔진들에 대해 일관적인 API를 제공함으로써, 개발자는 기존의 코드를 수정하지 않고, 새로운 함수를 추가하여, DEVS에 기반한 모델을 모의 실험, 분석, 실행할수 있다. 이 통합된 엔진은 빠른 프로토타입의 개발과 자동 코드 생성을 가능케 하는 정형적 시스템 개발 도구인 DEVShop과 밀결합되어 있다. DEVShop은 시각적인 모델 개발 도구, 프로젝트 관리 도구, 모델 검증 도구, 자동 코드 생성기, 그리고, 상호 작용하는 추적 도구등을 제공하여, 모델의 개발, 모의 실험, 분석, 실행이 가능케 한다. 이 도구는 개발자가 복잡한 설계 과정의 초반에 모의 실험과 분석에 의한 검증을 가능케 하여, 비용이 많이 드는 재개발 과정을 피하게 한다. 또한 이 도구는 병행 실시간 소프트웨어를 개발하는데에 사용될수 있는 코드를 자동으로 생성하여, 시스템 개발 시간을 단축시켜준다. 결과적으로, 제안된 틀의 검증된 구현 방법에 의해, 높은 레벨의 정형적인 모델이 추적가능한 방법에 따라 실제 구현으로 이어질수 있다. 우리는 이 방법의 예로써, 엘리베이터 제어 시스템을 보인다.
