BROWSE
Detail
Conference Paper
Case Study: Verification of ECML Models Using SpaceEx
Cited - time in 
Share 
Share
- Authors
- Jaeyeon Jo, Sanghyun Yoon, Junbeom Yoo, Hae Young Lee, Won-Tae Kim
- Issue Date
- 2012-09
- Citation
- Korea-Japan Joint Workshop on ICT 2012, pp.1-4
- Language
- English
- Type
- Conference Paper
- Abstract
- We present a formal verification of a hybrid system from an example of a barrel-filler system. Hybrid system composes continuous elements and discrete elements. ECML (ETRI CPS Modeling Language) is a modeling formalism for hybrid systems, recently proposed by a research institute -ETRI in Korea. It extends a basic formalism DEV& DESS (Discrete EVent & Differential Equation System Specification) with various conveniences in modeling and simulation. An ECML model checking tool has not been developed yet. SpaceEx is a verification tool for hybrid automata using reachability algorithms. It integrates various approaches of hybrid system verification. The case study illustrates how verification can be performed on an ECML model using a hybrid automata translation by hands.
- KSP Keywords
- Case studies, Differential equation system, Discrete Elements, Discrete Event(DE), Formal verification, Hybrid Automata, Hybrid system, Modeling and Simulation, Research institute, System Verification, System specification