Name
Abstract | ||
|---|---|---|
In collaboration with NASA's Langley Research Center, we are developing mechanically verified formal specifications for the fault-tolerant architecture, algorithms, and implementations of a reliable computing platform (RCP) for digital flight-control applications.
Several of the formal specifications and verifications performed in support of RCP are individually of considerable complexity and difficulty. But in order to contribute to the larger goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to build on, modify, or cannibalize an intricate verification.
Accordingly, we have been developing and honing our verification tools to better support these large, difficult, iterative, and collaborative verifications. Our goal is to reduce formal verifications as difficult as these to routine exercises, and to maximize the value obtained from formalization and verification. In this paper, we describe some of the challenges we have faced, lessons learned, design decisions taken, and results obtained.
|
Year | DOI | Venue |
|---|---|---|
1993 | 10.1007/BFb0024663 | FME |
Keywords | Field | DocType |
fault-tolerant architectures,formal verification,formal specification,fault tolerant | Functional verification,Computer architecture,Intelligent verification,Computer science,Verification,Formal specification,Fault tolerance,Refinement,Formal methods,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-56662-7 | 8 | 1.36 |
References | Authors | |
19 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sam Owre | 1 | 1323 | 104.39 |
| John Rushby | 2 | 2459 | 235.69 |
| Natarajan Shankar | 3 | 3050 | 309.55 |
| Friedrich W. Von Henke | 4 | 425 | 49.05 |