Formal verification of basic DEV&DESS formalism using hytech

Han Choi, Sungdeok Cha, Jae Yeon Jo, Junbeom Yoo, Hae Young Lee, Won Tae Kim

Research output: Contribution to journalArticle

2 Citations (Scopus)

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 languageEnglish
Pages (from-to)821-826
Number of pages6
JournalInformation (Japan)
Volume16
Issue number1 B
Publication statusPublished - 2013 Jan

Keywords

  • DEV&DESS
  • HyTech
  • Hybrid system
  • Linear hybrid automata
  • Model checking
  • Parametric analysis

ASJC Scopus subject areas

  • Information Systems

Fingerprint Dive into the research topics of 'Formal verification of basic DEV&DESS formalism using hytech'. Together they form a unique fingerprint.

  • Cite this

    Choi, H., Cha, S., Jo, J. Y., Yoo, J., Lee, H. Y., & Kim, W. T. (2013). Formal verification of basic DEV&DESS formalism using hytech. Information (Japan), 16(1 B), 821-826.