Formal Verification of Hybrid System
1. Formal Verification of ECML(ETRI
CPS Modeling Language) using HyTech
- An automatic translator from ECML to linear hybrid automata in HyTech
- ECMLtoHyTech [download]
developed by Jaeyeon Jo(MS, currently working for ETRI, 2013.12.01)
- Semi-formally defined translation rules
3. HyTech Analyzer
- An automatic assistant for HyTech
- The HyTech model checker provides no
- Provides graphical interfaces for HyTech
and in-depth analysis on verification results
Developed by Jaeyeon Jo (MS, currently working for ETRI, 2013.12.01)
4. Formal Verification of ECML using SpaceEx
5. Formal Verification in EcoPOD
- Modeling & simulation Environment for ECML
- Translation tool set
- ECML checker: An automatic assistant for ECML language rule & translation restriction checking
- Makes checking result report file (.xml format)
- Included in EcoPOD
- ECMLtoSpaceEx: An automatic translator from ECML to SpaceEx Model
- ECMLtoSpaceEx[download] developed by Sanghyun Yoon.
- The tool translates ECML model into behaviorally equivalent SpaceEx model.
- CPVtoCFG: An automatic translator
- Users could specify verification property in EcoPOD.
- Translate verification properties specified in EcoPOD (CPV file), and set initial values & locations
- CPV file: Verification property file format in EcoPOD
- CFG file: Configuration file format for SpaceEx; it includes verification properties
- Included in ECMLtoSpaceEx.
- GenUnifier & INTVtoCSV
- Visualization tools from SpaceEx verification result
- INTVtoCSV shows ranges of values for variables in each location.
- GenUnfier shows change of values for variables.