Sciweavers

HYBRID
1998
Springer

Formal Verification of Safety-Critical Hybrid Systems

14 years 2 months ago
Formal Verification of Safety-Critical Hybrid Systems
This paper investigates how formal techniques can be used for the analysis and verification of hybrid systems [1,5,7,16] -- systems involving both discrete and continuous behavior. The motivation behind such research lies in the inherent similarity of the hierarchical and decentralized control strategies of hybrid systems and the communication and operation protocols used for distributed systems in computer science. This paper focuses on the use of hybrid I/O automata [11,12] to model, analyze, and verify safety-critical hybrid systems that use emergency control subsystems to prevent the violation of their safety requirements. r is split into two parts. First, we develop an abstract model of a protector -- an emergency control component that guarantees that the physical plant at hand adheres to a particular safety requirement. The protector model specialized to a particular physical plant and a particular safety requirement constitutes the specification of a protector that enforces the...
Carolos Livadas, Nancy A. Lynch
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where HYBRID
Authors Carolos Livadas, Nancy A. Lynch
Comments (0)