Name
Abstract | ||
|---|---|---|
This paper reports an approach for the specification and verification of the correctness of dependable system designs achieved by the application of fault tolerant techniques based on equivalence relations and model checking techniques. The behaviour of the system in absence of faults is formally specified and faults are assumed as random events which interfere with the system by modifying its behaviour: The fault tolerant technique is formalized by a context, which specifies how replicas of the system cooperate to deal with faults. The system design is proved to satisfy the correctness property under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behaviour can be applied to verify the correctness of the design. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1109/ISORC.1998.666809 | ISORC |
Keywords | Field | DocType |
dependable systems,fault tolerant,model checking,system design,formal specification,correctness,equivalence relations,satisfiability,logic,equivalence relation,specification,temporal logic,formal specifications | Model checking,Computer science,Observational equivalence,Correctness,Systems design,Formal specification,Real-time computing,Fault tolerance,Temporal logic,System requirements specification | Conference |
ISBN | Citations | PageRank |
0-8186-8430-5 | 1 | 0.35 |
References | Authors | |
12 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| C. Bernardeschi | 1 | 41 | 4.90 |
| Luca Simoncini | 2 | 184 | 24.69 |
| Alessandro Fantechi | 3 | 1199 | 103.40 |