Formal Verification of Hybrid System

1. Formal Verification of ECML(ETRI CPS Modeling Language) using HyTech

2. ECMLtoHyTech

• 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 GUI.
  • 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

• 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.