원문정보
초록
영어
Virtually all control systems nowadays perform various behavioral aspects such as discrete control mode transformation and continuous real time behavior. The interaction of these different types of dynamics and information leads to a lot of safety and control problems. In this paper, to verify these systems we propose a specification model combining interface automata, initialized multirate hybrid automata and Z language, named MZIA. This model can be used to describe temporal properties, hybrid properties, and data properties of hybrid software/hardware complements. And then, we propose a temporal logic for MZIA. Next, considering the measuring errors of real-numbered variables in practice, we study the approximated model checking method of MZIA. Finally, an example is given to indicate that this method is feasible and effective.
목차
1. Introduction
2. Multirate Hybrid Interface Automata with Z
3. Logic for MZIA
3.1. Syntax
3.2. Semantics
4. MZIA with Finite Domain
4.1. Multirate Zones
4.2. MZIA with Finite Domain
5. Model Checking Algorithm for MZIA with Finite Domain
5.1. Algorithm
5.2. Implementation
6. Example
6.1. Boiler Plant Description
6.2. DCM Respresentation
6.3. MZIA Modeling
6.4. Verification
7. Conclusion
References