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 them. In this work, we modelled in the HOL4 system such design patterns, which we call here fault tolerant patterns. We illustrate our approach by modelling three classical fault tolerant patterns: Homogeneous Redundancy, Heterogeneous Redundancy and Triple Modular Redundancy. Our model takes into account that the original system (without redundancy) computes a certain function with some delay and is amenable to random failures. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1016/j.scico.2013.07.009 | Science of Computer Programming |
Keywords | Field | DocType |
Redundancy management,Fault tolerance,Behavioural preservation,Theorem proving,HOL | HOL,Computer science,Automated theorem proving,Correctness,Triple modular redundancy,Software design pattern,Theoretical computer science,Redundancy (engineering),Fault tolerance,Interval arithmetic | Journal |
Volume | ISSN | Citations |
92 | 0167-6423 | 0 |
PageRank | References | Authors |
0.34 | 10 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Diego Machado Dias | 1 | 2 | 0.71 |
| Juliano Iyoda | 2 | 61 | 9.21 |