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 journalArticlepeer-review

    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