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

doi:10.1007/978-3-642-26010-0_13

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

Department of Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Control 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
Pages	112-121
Number of pages	10
DOIs	https://doi.org/10.1007/978-3-642-26010-0_13
Publication status	Published - 2011
Event	2011 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 8 → 2011 Dec 10

Publication series

Name	Communications in Computer and Information Science
Volume	256 CCIS
ISSN (Print)	1865-0929

Other

Other	2011 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
Country/Territory	Korea, Republic of
City	Jeju Island
Period	11/12/8 → 11/12/10

ASJC Scopus subject areas

Computer Science(all)
Mathematics(all)

Access to Document

10.1007/978-3-642-26010-0_13

Cite this

Choi, H., Cha, S., Jo, J. Y., Yoo, J., Lee, H. Y., & Kim, W. T. (2011). Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech. In Control 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 (pp. 112-121). (Communications in Computer and Information Science; Vol. 256 CCIS). https://doi.org/10.1007/978-3-642-26010-0_13

Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech. / Choi, Han; Cha, Sungdeok; Jo, Jae Yeon et al.

Control 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. 2011. p. 112-121 (Communications in Computer and Information Science; Vol. 256 CCIS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Choi, H, Cha, S, Jo, JY, Yoo, J, Lee, HY & Kim, WT 2011, Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech. in Control 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. Communications in Computer and Information Science, vol. 256 CCIS, pp. 112-121, 2011 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, 11/12/8. https://doi.org/10.1007/978-3-642-26010-0_13

Choi H, Cha S, Jo JY, Yoo J, Lee HY, Kim WT. Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech. In Control 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. 2011. p. 112-121. (Communications in Computer and Information Science). doi: 10.1007/978-3-642-26010-0_13

Choi, Han ; Cha, Sungdeok ; Jo, Jae Yeon et al. / Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech. Control 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. 2011. pp. 112-121 (Communications in Computer and Information Science).

@inproceedings{3153071d92274bb392cc69ac9d118ead,

title = "Formal verification of DEV and DESS formalism using symbolic model checker Hy Tech",

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.",

author = "Han Choi and Sungdeok Cha and Jo, {Jae Yeon} and Junbeom Yoo and Lee, {Hae Young} and Kim, {Won Tae}",

year = "2011",

doi = "10.1007/978-3-642-26010-0_13",

language = "English",

isbn = "9783642260094",

series = "Communications in Computer and Information Science",

pages = "112--121",

booktitle = "Control 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",

note = "2011 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 ; Conference date: 08-12-2011 Through 10-12-2011",

}

TY - GEN

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

AU - Choi, Han

AU - Cha, Sungdeok

AU - Jo, Jae Yeon

AU - Yoo, Junbeom

AU - Lee, Hae Young

AU - Kim, Won Tae

PY - 2011

Y1 - 2011

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

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

UR - http://www.scopus.com/inward/record.url?scp=82955210380&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-26010-0_13

DO - 10.1007/978-3-642-26010-0_13

M3 - Conference contribution

AN - SCOPUS:82955210380

SN - 9783642260094

T3 - Communications in Computer and Information Science

SP - 112

EP - 121

BT - Control 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

T2 - 2011 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

Y2 - 8 December 2011 through 10 December 2011

ER -

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

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this