Abstract
A hybrid system is a dynamical system reacting to continuous and discrete changes simultaneously. Many researchers have proposed modeling and verification formalisms for hybrid systems, but algorithmic verification of important properties such as safety and reachability is still an on-going research area. This paper demonstrates that a basic modeling formalism for hybrid systems, DEV&DESS, is an easy-to-use input front-end of a widely-used formal verification tool, HyTech. This paper transforms basic DEV&DESS models into linear hybrid automata and performs the HyTech model checking. We are now developing translation rules from DEV&DESS models into linear hybrid automata through various case studies.
Original language | English |
---|---|
Pages (from-to) | 821-826 |
Number of pages | 6 |
Journal | Information (Japan) |
Volume | 16 |
Issue number | 1 B |
Publication status | Published - 2013 Jan |
Keywords
- DEV&DESS
- HyTech
- Hybrid system
- Linear hybrid automata
- Model checking
- Parametric analysis
ASJC Scopus subject areas
- Information Systems