Executable Formal Specification and Validation of NoC Communication Infrastructures

被引：0

作者：

Borrione, Dominique ^{[1
]}

Helmy, Amr ^{[1
]}

Pierre, Laurence ^{[1
]}

Schmaltz, Julien

机构：

[1] CNRS GrenobleINP UJF, TIMA Lab, Grenoble, France

来源：

SBCCI 2008: 21ST SYMPOSIUM ON INTEGRATED CIRCUITS AND SYSTEMS DESIGN, PROCEEDINGS | 2008年

关键词：

Verification; Theorem proving; Simulation;

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

We describe an enhanced generic model for Networks-on-Chip (NoCs), implemented in the executable logic of the ACL2 theorem prover. The model is meant for serving as a formal reference for the specification, validation, and simulation at the initial design phase. Instantiated on a specific NoC, the model may be used for formal proofs and for simulation. The methodology is illustrated on HERMES.

引用

页码：176 / 181

页数：6

共 50 条

[1] An executable specification of a formal argumentation protocol
Artikis, Alexander
Sergot, Marek
Pitt, Jeremy
[J]. ARTIFICIAL INTELLIGENCE, 2007, 171 (10-15) : 776 - 804
[2] Formal specification and validation of a vital communication protocol
Cimatti, A
Pieraccini, PL
Sebastiani, R
Traverso, P
Villafiorita, A
[J]. FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1584 - 1604
[3] A formal and executable specification of the Internet open trading protocol
Ouyang, C
Kristensen, LM
Billington, J
[J]. E-COMMERCE AND WEB TECHNOLOGIES, PROCEEDINGS, 2002, 2455 : 377 - 387
[4] Executable requirements specification: Formal semantics of Live Activity Diagrams
Knicke, Christoph
Huhn, Michaela
Lochau, Malte
[J]. TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 109 - 112
[5] Visualisation of executable formal specifications for user validation
Özcan, MB
Parry, PW
Morrey, IC
Siddiqi, JI
[J]. SERVICES AND VISUALIZATION: TOWARDS USER-FRIENDLY DESIGN, 1998, 1385 : 142 - 157
[6] Tobias-Z: An executable formal specification of a test generator
Ledru, Y.
du Bousquet, L.
[J]. ASE 2006: 21ST IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2006, : 353 - +
[7] Automated conversion from a requirements document to an executable formal specification
Lee, BS
[J]. 16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 437 - 437
[8] Use of executable formal specifications in user validation
Ozcan, MB
[J]. SOFTWARE-PRACTICE & EXPERIENCE, 1998, 28 (13): : 1359 - 1385
[9] A Formal Executable Specification of the GinMAC Protocol for Wireless Sensor Actuator Networks
Somappa, Admar Ajith Kumar
Kristensen, Lars Michael
Ovsthus, Knut
[J]. 2013 INTERNATIONAL SYMPOSIUM ON WIRELESS AND PERVASIVE COMPUTING (ISWPC), 2013,
[10] Animating a non-executable formal specification with a distributed symbolic language
Ciancarini, P
Cimato, S
[J]. DESIGN AND IMPLEMENTATION OF SYMBOLIC COMPUTATION SYSTEMS, 1996, 1128 : 200 - 201

← 1 2 3 4 5 →