Specifying and verifying systems with multiple clocks

被引：4

作者：

Clarke, EM ^{[1
]}

Kroening, D ^{[1
]}

Yorav, K ^{[1
]}

机构：

[1] Carnegie Mellon Univ, Dept Comp Sci, Pittsburgh, PA 15213 USA

来源：

21ST INTERNATIONAL CONFERENCE ON COMPUTER DESIGN, PROCEEDINGS | 2003年

关键词：

D O I：

10.1109/ICCD.2003.1240872

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Multiple clock domains are a challenge for hardware specification and verification. We present a method for specifying the relations between multiple clocks, and for modeling the possible behaviors. We can then verify a hardware design assuming that the clocks meet these constraints. We implement our ideas in the context of SAT based Bounded Model Checking (BMC), using ANSI-C programs to specify the functional behavior of the design.

引用

页码：48 / 55

页数：8

共 50 条

[41] Specifying and Verifying Business Processes Using PPML
Regis, German
Aguirre, Nazareno
Maibaum, Tom
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 737 - +
[42] Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
Yang, SJH
Chu, W
Lee, J
INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 1999, 9 (02) : 233 - 249
[43] Towards formally specifying and verifying transactional memory
Doherty, Simon
Groves, Lindsay
Luchangco, Victor
Moir, Mark
FORMAL ASPECTS OF COMPUTING, 2013, 25 (05) : 769 - 799
[44] Specifying and Verifying Concurrent C Programs with TLA
Methni, Amira
Lemerre, Matthieu
Ben Hedia, Belgacem
Haddad, Serge
Barkaoui, Kamel
FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2014, 2015, 476 : 206 - 222
[45] Specifying multiple time granularities in interactive systems
Kutar, M
Britton, C
Nehaniv, C
INTERACTIVE SYSTEMS: DESIGN, SPECIFICATION, AND VERIFICATION, 2001, 1946 : 51 - 63
[46] Layered Control Systems Operating on Multiple Clocks
Incer, Inigo
Csomay-Shanklin, Noel
Ames, Aaron D.
Murray, Richard M.
IEEE CONTROL SYSTEMS LETTERS, 2024, 8 : 1211 - 1216
[47] Specifying and Verifying CRDT Protocols Using TLA+
Ji Y.
Wei H.-F.
Huang Y.
Lü J.
Ruan Jian Xue Bao/Journal of Software, 2020, 31 (05): : 1332 - 1352
[48] Specifying and verifying interaction protocols in a temporal action logic
Dipartimento di Informatica, Università del Piemonte Orientale, Alessandria, Italy
不详
不详
J. Appl. Logic, 2007, 2 (214-234):
[49] Specifying and Verifying Information Flow Control in SELinux Configurations
Ceragioli, Lorenzo
Galletta, Letterio
Degano, Pierpaolo
Basin, David
ACM TRANSACTIONS ON PRIVACY AND SECURITY, 2024, 27 (04)
[50] Specifying and Verifying Sensor Networks: An Experiment of Formal Methods
Dong, Jin Song
Sun, Jing
Sun, Jun
Taguchi, Kenji
Zhang, Xian
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2008, 5256 : 318 - +

← 1 2 3 4 5 →