Formal Verification of DEV&DESS Formalism Using Symbolic Model Checker HyTech

被引：0

作者：

Choi, Han ^{[1
]}

Cha, Sungdeok ^{[1
]}

Jo, Jae Yeon ^{[2
]}

Yoo, Junbeom ^{[2
]}

Lee, Hae Young ^{[3
]}

Kim, Won-Tae ^{[3
]}

机构：

[1] Korea Univ, Seoul, South Korea

[2] Konkuk Univ, Seoul, South Korea

[3] Elect & Telecommunicat Res Inst, Daejeon, South Korea

来源：

CONTROL AND AUTOMATION, AND ENERGY SYSTEM ENGINEERING | 2011年 / 256卷

关键词：

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：112 / +

页数：3

共 50 条

[1] Hybrid Co-simulation of FMUs using DEV&DESS in MECSYCO
Camus, Benjamin
Galtier, Virginie
Caujolle, Mathieu
[J]. 2016 SYMPOSIUM ON THEORY OF MODELING AND SIMULATION (TMS-DEVS), 2016,
[2] Formal verification of real-time software by symbolic model-checker
Nakamura, K
Yamane, S
[J]. 1998 INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 1998, : 99 - 108
[3] Formal verification of VHDL - The model checker CV
Deharbe, D
Shankar, S
Clarke, EM
[J]. XI BRAZILIAN SYMPOSIUM ON INTEGRATED CIRCUIT DESIGN, PROCEEDINGS, 1998, : 95 - 98
[4] Building a Symbolic Model Checker from Formal Language Description
Bobeda, Edmundo Lopez
Colange, Maximilien
Buchs, Didier
[J]. 2015 15TH INTERNATIONAL CONFERENCE ON APPLICATIONS OF CONCURRENCY TO SYSTEM DESIGN (ACSD), 2015, : 50 - 59
[5] Formal verification of digital circuits using symbolic model checking
Casar, A
Brezocnik, Z
Kapus, T
[J]. INFORMACIJE MIDEM-JOURNAL OF MICROELECTRONICS ELECTRONIC COMPONENTS AND MATERIALS, 2000, 30 (03): : 153 - 160
[6] NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification
Yuan, Yifei
Moon, Soo-Jin
Uppal, Sahil
Jia, Limin
Sekar, Vyas
[J]. PROCEEDINGS OF THE 17TH USENIX SYMPOSIUM ON NETWORKED SYSTEMS DESIGN AND IMPLEMENTATION, 2020, : 181 - 200
[7] FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals
Calinescu, Radu
Johnson, Kenneth
Paterson, Colin
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 : 540 - 546
[8] Formal Verification of 802.11 MAC Layer Handoff Process Using SPIN Model Checker
Zhao, Dan
Zhang, Dafang
Miao, Li
[J]. 2009 WRI WORLD CONGRESS ON SOFTWARE ENGINEERING, VOL 3, PROCEEDINGS, 2009, : 402 - +
[9] Formal verification of ad-hoc routing protocols using SPIN model checker
de Renesse, R
Aghvami, AH
[J]. MELECON 2004: PROCEEDINGS OF THE 12TH IEEE MEDITERRANEAN ELECTROTECHNICAL CONFERENCE, VOLS 1-3, 2004, : 1177 - 1182
[10] Formal verification of a pipelined processor with new memory hierarchy using a commercial model checker
Nakamura, H
Arai, T
Fujita, M
[J]. 2002 PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING, PROCEEDINGS, 2002, : 321 - 324

← 1 2 3 4 5 →