Model checking algorithms for analog verification

被引：0

作者：

Hartong, W ^{[1
]}

Hedrich, L ^{[1
]}

Barke, E ^{[1
]}

机构：

[1] Univ Hannover, Inst Microelect Circuits & Syst, D-30167 Hannover, Germany

来源：

39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002 | 2002年

关键词：

model checking; formal methods; nonlinear analog systems;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

In this contribution we present the first method for model checking on nonlinear analog systems. Based on digital CTL model checking algorithms and results in hybrid model checking, we have developed a concept to adapt these ideas to analog systems. Using an automatic state space subdivision method the continuous state space is transfered into a discrete model. In doing this, the most challenging task is to retain the essential nonlinear behavior of the analog system. To describe analog specification properties, an extension to the CTL language is needed. Two small examples show the properties and advantages of this new method and the capability of the implemented prototype tool.

引用

页码：542 / 547

页数：2

共 50 条

[21] Verification of clinical guidelines by model checking
Perez, Beatriz
Porres, Ivan
PROCEEDINGS OF THE 21ST IEEE INTERNATIONAL SYMPOSIUM ON COMPUTER-BASED MEDICAL SYSTEMS, 2008, : 114 - +
[22] Model Checking: Algorithmic Verification and Debugging
Clarke, Edmund M.
Emerson, E. Allen
Sifakis, Joseph
COMMUNICATIONS OF THE ACM, 2009, 52 (11) : 75 - 84
[23] Model Checking for Verification of Quantum Circuits
Ying, Mingsheng
FORMAL METHODS, FM 2021, 2021, 13047 : 23 - 39
[24] On Applying Model Checking in Formal Verification
Hjort, Hakan
2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 : 3 - 3
[25] Applying model checking to workflow verification
Pfeiffer, JH
Rossak, WR
Speck, A
11TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOP ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2004, : 144 - 151
[26] Model checking of analog systems using an Analog Specification Language
Steinhorst, Sebastian
Hedrich, Lars
2008 DESIGN, AUTOMATION AND TEST IN EUROPE, VOLS 1-3, 2008, : 282 - 287
[27] On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency
Voellinger, Kim
Akili, Samira
FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2018, 2018, 10854 : 161 - 180
[28] Equivalence Checking of Nonlinear Analog Circuits for Hierarchical AMS System Verification
Steinhorst, Sebastian
Hedrich, Lars
2012 IEEE/IFIP 20TH INTERNATIONAL CONFERENCE ON VLSI AND SYSTEM-ON-CHIP (VLSI-SOC), 2012, : 135 - 140
[29] Algorithms for Model Checking HyperLTL and HyperCTL
Finkbeiner, Bernd
Rabe, Markus N.
Sanchez, Cesar
COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 : 30 - 48
[30] Hardware Model Checking Algorithms and Techniques
Cabodi, Gianpiero
Camurati, Paolo Enrico
Palena, Marco
Pasini, Paolo
ALGORITHMS, 2024, 17 (06)

← 1 2 3 4 5 →