Name
Abstract | ||
|---|---|---|
In the development of critical systems it is common practice to make use of redundancy in order to achieve higher levels of reliability. There are well established design patterns that introduce redundancy and that are widely documented and adopted by the industry. However there have been few attempts to formally verify some of them. In this work we modelled three fault tolerant patterns (homogeneous redundancy, heterogeneous redundancy and triple modular redundancy) using the HOL4 theorem prover in order to prove that the application of these patterns preserves the behaviour of the original system. Our model takes into account that the original system (without redundancy) computes a certain function with some delay and is amenable to random failure. We illustrate our approach with a case study that verifies in HOL4 that a fault tolerant design applied to a simplified avionic elevator system does not introduce functional errors. This work has been done in collaboration with the Brazilian aircraft manufacturer Embraer. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-25032-3_11 | SBMF |
Keywords | Field | DocType |
fault tolerant pattern,design pattern,hol4 theorem prover,homogeneous redundancy,heterogeneous redundancy,original system,critical system,triple modular redundancy,fault tolerant design,avionic elevator system,behavioural preservation,theorem proving,fault tolerance,hol | HOL,Computer science,Avionics,Automated theorem proving,Software design pattern,Triple modular redundancy,Real-time computing,Redundancy (engineering),Fault tolerance,Dual modular redundancy | Conference |
Volume | ISSN | Citations |
7021 | 0302-9743 | 2 |
PageRank | References | Authors |
0.37 | 9 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Diego Machado Dias | 1 | 2 | 0.71 |
| Juliano Manabu Iyoda | 2 | 5 | 0.74 |