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 条

[21] Extended state identification and verification using a model checker
Robinson-Mallett, Christopher
Liggesmeyer, Peter
Muecke, Tilo
Goltz, Ursula
[J]. INFORMATION AND SOFTWARE TECHNOLOGY, 2006, 48 (10) : 981 - 992
[22] Formal verification of memory arrays using symbolic trajectory evaluation
Pandey, M
Bryant, RE
[J]. INTERNATIONAL WORKSHOP ON MEMORY TECHNOLOGY, DESIGN AND TESTING, PROCEEDINGS, 1997, : 42 - 49
[23] Formal verification of a snoop-based cache coherence protocol using symbolic model checking
Srinivasan, S
Chhabra, PS
Jaini, PK
Aziz, A
John, L
[J]. TWELFTH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 1999, : 288 - 293
[24] Using a formal specification and a model checker to monitor and direct simulation
Tasiran, S
Yu, Y
Batson, B
[J]. 40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 356 - 361
[25] An ACL2 model of VHDL for symbolic simulation and formal verification
Rodrigues, VM
Borrione, D
Georgelin, P
[J]. 13TH SYMPOSIUM ON INTEGRATED CIRCUITS AND SYSTEMS DESIGN, PROCEEDINGS, 2000, : 269 - 274
[26] Modeling, Verification and Testing of Web Applications Using Model Checker
Homma, Kei
Izumi, Satoru
Takahashi, Kaoru
Togashi, Atsushi
[J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2011, E94D (05): : 989 - 999
[27] Using CTL Model Checker for Verification of Domain Application Systems
Cacovean, Laura Florentina
[J]. RECENT ADVANCES IN NEURAL NETWORKS, FUZZY SYSTEMS & EVOLUTIONARY COMPUTING, 2010, : 262 - 267
[28] Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation
Kalla, Priyank
[J]. PROCEEDINGS OF THE 15TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2015), 2015, : 2 - 2
[29] Formal verification of PowerPC(TM) arrays using symbolic trajectory evaluation
Pandey, M
Raimi, R
Beatty, DL
Bryant, RE
[J]. 33RD DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 1996, 1996, : 649 - 654
[30] Formal verification of content addressable memories using symbolic trajectory evaluation
Pandey, M
Raimi, R
Bryant, RE
Abadir, MS
[J]. DESIGN AUTOMATION CONFERENCE - PROCEEDINGS 1997, 1997, : 167 - 172

← 1 2 3 4 5 →