Earticle

초록

영어

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.

목차

Abstract
 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

키워드

저자

• Guozheng Li [ Computer Science Department Nanjing University of Aeronautics & Astronautics, Nanjing, China ]
• Zining Cao [ Computer Science Department Nanjing University of Aeronautics & Astronautics, Nanjing, China ]
• Zheng Gao [ Computer Science Department Nanjing University of Aeronautics & Astronautics, Nanjing, China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Control and Automation

• 간기

  월간

• pISSN

  2005-4297

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605