Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 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 formal verification tool, HyTech. HyTech is a symbolic model checker for liner hybrid automata, and we transformed an atomic DEV&DESS model into linear hybrid automata. We are now developing translation rules from DEV&DESS models, including a coupled DEV&DESS, into linear hybrid automata, through various case studies.

Original languageEnglish
Title of host publicationControl and Automation, and Energy System Engineering - International Conferences, CA and CES3 2011, Held as Part of the FGIT 2011, in Conjunction with GDC 2011, Proceedings
Pages112-121
Number of pages10
DOIs
Publication statusPublished - 2011
Event2011 Int. Conf. on Control and Automation CA 2011 andCircuits Control Commun. Electric.Electronics EnergySyst.Signal and Simulation CES3 2011 Held as Part of the 3rd Int.Mega-Conf.on Future-Gener.Inf.Technol.FGIT 2011 in Conjunction with GDC 2011 - Jeju Island, Korea, Republic of
Duration: 2011 Dec 82011 Dec 10

Publication series

NameCommunications in Computer and Information Science
Volume256 CCIS
ISSN (Print)1865-0929

Other

Other2011 Int. Conf. on Control and Automation CA 2011 andCircuits Control Commun. Electric.Electronics EnergySyst.Signal and Simulation CES3 2011 Held as Part of the 3rd Int.Mega-Conf.on Future-Gener.Inf.Technol.FGIT 2011 in Conjunction with GDC 2011
CountryKorea, Republic of
CityJeju Island
Period11/12/811/12/10

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Fingerprint Dive into the research topics of 'Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech'. Together they form a unique fingerprint.

Cite this