Title :
Behavior verification of hybrid real-time requirements by qualitative formalism
Author :
Jang-Soo Lee ; Cha, Sung-Deok
Author_Institution :
MMIS Lab., Korea Atomic Energy Res. Inst., Taejon, South Korea
Abstract :
Although modern control theories have been successfully applied to solve a variety of problems, they are often mathematically and physically too specific to describe and analyze the qualitative properties of hybrid real-time systems. In this paper, we propose the use of qualitative formal methods, Compositional Modeling Language (CML) and Causal Functional Representation Language (CFRL) in particular, to specify continuous plant dynamics and the required behavior respectively. The system behavior has been simulated by a qualitative simulator known as the Device Modeling Environment (DME), and verified against the required behavior. Using the Electrical Power System (EPS) as an example, we demonstrate the effectiveness of our approach by illustrating here a simple SCR-style specification can be transformed and analyzed
Keywords :
formal specification; formal verification; process control; real-time systems; Causal Functional Representation Language; Compositional Modeling Language; behavior verification; causal reasoning; continuous plant dynamics; formal methods; hybrid real-time requirements; qualitative formalism; real-time process control; real-time systems; Actuators; Control systems; Control theory; Embedded software; Error correction; Power system dynamics; Power system modeling; Power system simulation; Real time systems; Sensor systems;
Conference_Titel :
Real-Time Computing Systems and Applications, 1997. Proceedings., Fourth International Workshop on
Conference_Location :
Taipei
Print_ISBN :
0-8186-8073-3
DOI :
10.1109/RTCSA.1997.629184