Abstract
Standardized and reusable software (SW) objects (or SW components - in-house or pre-fabricated) are increasingly being used to reduce the cost of software (SW) development. Given that the basic components may not have been developed with dependability as primary driver, these components need to be adapted to deal with errors from their environment. To achieve this, error containment wrappers are added to increase the reliability of the components. In this paper, we first present a modular specification approach using fault intolerant components, based on the concepts of category theory. We further introduce the concept of wrapper consistency, based upon which, we present an algorithm that systematically generates globally consistent fault containment wrappers for each component, to make them fault tolerant. Subsequently, we enhance the initial modular specification to deal with the wrapped components, and show that safety properties of the system are preserved under composition only if the wrappers are globally consistent.
Supported in part by Saab endowment, TFR Grants
Chapter PDF
Similar content being viewed by others
References
B. Alpern, F.B. Schneider, “Defining Liveness”, Information Processing Letters, 21(4):181–185, 1985
A. Arora, S. Kulkarni, “Detectors and Correctors: A Theory of Fault-Tolerance Components”, Proc ICDCS, pp 436–443, May 1998.
P. Cousot, R. Cousot, “Static Determination of Dynamic Properties of Programs”, Int. Symposium on Programming, 1976
E.W. Dijkstra, “A Discipline of Programming”, Prentice Hall, 1976
M. Doche et al, “A Modular Approach to Specify and Test an Electrical Flight Control System”, 4th Intl. Workshop on Formal Methods for Industrial Critical Systems, 1999
H. Ehrig, B. Mahr, “Fundamentals of Algebraic Specification 2: Modules Specifications and Constraints”, EATCS Monographs on Theoretical Computer Science, Vol. 21, Springer Verlag, 1989
A. Ermedahl, J. Gustafsson, “Deriving Annotations For Tight Calculation of Execution Time”, Proc EuroPar’97, RT System Workshop
T. Fraser et al, “Hardening cots software with generic software wrappers”, IEEE Symposium on Security and Privacy, pp. 2–16, 1999
M. Hiller, A. Jhumka, N. Suri, “An Approach for Analysing the Propagation of Data Errors in Software”, Proc. DSN’01, pp. 161–170, 2001
C. A. R. Hoare, “Communicating Sequential Processes”, Prentice Hall, 1985
T. Jensen et al, “Verification of Control Flow Based Security Properties”, Proc. IEEE Symp.on Security and Privacy, pp. 89–103, 1999
A. Jhumka, M. Hiller, V. Claesson, N. Suri, “On Systematic Design of Consistent Executable Assertions For Distributed Embedded Software”, to Appear ACM LCTES/SCOPES, 2002
S. Kulkarni, A. Arora, “Automating the Addition of Fault Tolerance”, Proc. Formal Techniques in Real Time and Fault Tolerant Systems, pp. 82–93, 2000
N.G. Leveson et al, “The use of self checks and voting in software error detection: An empirical study.”, IEEE Trans. on Soft. Eng., 16:432–443, 1990
Z. Liu, M. Joseph, “Verification of Fault-Tolerance and Real-Time”, Proc. FTCS 1996, pp220–229.
F. Salles et al, “Metakernels and fault containment wrappers”, Proc. FTCS, pp. 22–29, 1998
G. Smith, “The Object-Z Specification Language. Advances in Formal Methods”, Kluwer Academic Publishers, 2000
F. Tip, “A Survey of Program Slicing Techniques,” Journal Prog. Languages Vol.3, No., 3, pp.121–189, Sept. 95
V. Wiels, “Modularite pour la conception et la validation formelles de systemes”, PhD thesis, ENSAE-ONERA/CERT/DERI, Oct 97
J. Woodcock, J. Davies, “Using Z: Specification, Refinement, and Proof”, Prentice Hall, 1996
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jhumka, A., Hiller, M., Suri, N. (2002). Component-Based Synthesis of Dependable Embedded Software. In: Damm, W., Olderog, E.R. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2002. Lecture Notes in Computer Science, vol 2469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45739-9_9
Download citation
DOI: https://doi.org/10.1007/3-540-45739-9_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44165-6
Online ISBN: 978-3-540-45739-8
eBook Packages: Springer Book Archive