Name
Title | ||
|---|---|---|
Specification and validation of the SACI-1 on-board computer using timed-CSP-Z and Petri nets |
Abstract | ||
|---|---|---|
In this paper we focus on the application of integrated formal methods to the specification and validation of a fault tolerant real-time system (the on-board computer of a Brazilian micro-satellite). The work involves the application of a framework which covers from the formal specification to the analysis and use of tools to prove properties of the system. We used Timed-CSP-Z, a combination of Timed CSP and Z, to specify the system behavior, and then a strategy for converting the specification to TER Nets, a high level Petri Nets based formalism with time. The conversion enables us to use the CABERNET tool to analyse the behavior of the system. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/3-540-44919-1_13 | ICATPN |
Keywords | Field | DocType |
on-board computer,saci-1 on-board computer,fault tolerant real-time system,petri net,brazilian micro-satellite,formal specification,integrated formal method,system behavior,high level,cabernet tool,ter nets,timed csp,real time systems,fault tolerant,formal method | Specification language,Programming language,Petri net,Concurrency,Computer science,Real-time computing,Formal specification,Fault tolerance,Language Of Temporal Ordering Specification,Formal methods,Program analysis,Distributed computing | Conference |
Volume | ISSN | ISBN |
2679 | 0302-9743 | 3-540-40334-5 |
Citations | PageRank | References |
3 | 0.44 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Adnan Sherif | 1 | 83 | 5.26 |
| Augusto Sampaio | 2 | 96 | 13.42 |
| Sérgio Cavalcante | 3 | 3 | 0.44 |