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 条

[41] Modelling and Verification of CoAP over Routing Layer using SPIN Model Checker
Vattakunnel, Anchal J.
Kumar, Suresh N.
Kumar, G. Santhosh
[J]. PROCEEDINGS OF THE 6TH INTERNATIONAL CONFERENCE ON ADVANCES IN COMPUTING AND COMMUNICATIONS, 2016, 93 : 299 - 308
[42] Quantitative Verification of Beta Reputation System Using PRISM Probabilistic Model Checker
Bidgoly, Amir Jalaly
Ladani, Behrouz Tork
[J]. 2013 10TH INTERNATIONAL ISC CONFERENCE ON INFORMATION SECURITY AND CRYPTOLOGY (ISCISC), 2013,
[43] Verification of a Rule-Based Expert System by Using SAL Model Checker
Siregar, Maria Ulfah
Abriani, Sayekti
[J]. 2019 3RD INTERNATIONAL CONFERENCE ON INFORMATICS AND COMPUTATIONAL SCIENCES (ICICOS 2019), 2019,
[44] Formal Verification of Business Processes using Model Checking
Stoica, Florin
[J]. INNOVATION MANAGEMENT AND EDUCATION EXCELLENCE VISION 2020: FROM REGIONAL DEVELOPMENT SUSTAINABILITY TO GLOBAL ECONOMIC GROWTH, VOLS I - VI, 2016, : 2563 - 2575
[45] Formal verification of security model using SPR tool
Kim, Il-Gon
Kang, Miyoung
Choi, Jin-Young
Zegzhda, Peter D.
Kalinin, Maxim O.
Zegzhda, Dmitry P.
Kang, Inhye
[J]. COMPUTING AND INFORMATICS, 2006, 25 (05) : 353 - 368
[46] Design verification of Web Applications using symbolic model checking
Di Sciascio, E
Donini, FM
Mongiello, M
Totaro, R
Castelluccia, D
[J]. WEB ENGINEERING, PROCEEDINGS, 2005, 3579 : 69 - 74
[47] FORMAL VERIFICATION OF SPEED-DEPENDENT ASYNCHRONOUS CIRCUITS USING SYMBOLIC MODEL CHECKING OF BRANCHING TIME REGULAR TEMPORAL LOGIC
HAMAGUCHI, K
HIRAISHI, H
YAJIMA, S
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 410 - 420
[48] Modeling and Verification of Timed Automaton Based Hybrid Systems Using Spin Model Checker
Kumar, Suresh N.
Kumar, G. Santhosh
[J]. 2016 IEEE ANNUAL INDIA CONFERENCE (INDICON), 2016,
[49] Automatic generation of assertions for formal verification of PowerPC™ microprocessor arrays using symbolic trajectory evaluation
Wang, LC
Abadir, MS
Krishnamurthy, N
[J]. 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS, 1998, : 534 - 537
[50] Formal Analysis of QUIC Handshake Protocol Using Symbolic Model Checking
Zhang, Jingjing
Yang, Lin
Gao, Xianming
Tang, Gaigai
Zhang, Jiyong
Wang, Qiang
[J]. IEEE ACCESS, 2021, 9 : 14836 - 14848

← 1 2 3 4 5 →