Component-Based Synthesis of Dependable Embedded Software

  • Arshad Jhumka
  • Martin Hiller
  • Neeraj Suri
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


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.


  1. 1.
    B. Alpern, F.B. Schneider, “Defining Liveness”, Information Processing Letters, 21(4):181–185, 1985 zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    A. Arora, S. Kulkarni, “Detectors and Correctors: A Theory of Fault-Tolerance Components”, Proc ICDCS, pp 436–443, May 1998.Google Scholar
  3. 3.
    P. Cousot, R. Cousot, “Static Determination of Dynamic Properties of Programs”, Int. Symposium on Programming, 1976Google Scholar
  4. 4.
    E.W. Dijkstra, “A Discipline of Programming”, Prentice Hall, 1976Google Scholar
  5. 5.
    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, 1999Google Scholar
  6. 6.
    H. Ehrig, B. Mahr, “Fundamentals of Algebraic Specification 2: Modules Specifications and Constraints”, EATCS Monographs on Theoretical Computer Science, Vol. 21, Springer Verlag, 1989Google Scholar
  7. 7.
    A. Ermedahl, J. Gustafsson, “Deriving Annotations For Tight Calculation of Execution Time”, Proc EuroPar’97, RT System Workshop Google Scholar
  8. 8.
    T. Fraser et al, “Hardening cots software with generic software wrappers”, IEEE Symposium on Security and Privacy, pp. 2–16, 1999Google Scholar
  9. 9.
    M. Hiller, A. Jhumka, N. Suri, “An Approach for Analysing the Propagation of Data Errors in Software”, Proc. DSN’01, pp. 161–170, 2001 Google Scholar
  10. 10.
    C. A. R. Hoare, “Communicating Sequential Processes”, Prentice Hall, 1985Google Scholar
  11. 11.
    T. Jensen et al, “Verification of Control Flow Based Security Properties”, Proc. IEEE Symp.on Security and Privacy, pp. 89–103, 1999 Google Scholar
  12. 12.
    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 Google Scholar
  13. 13.
    S. Kulkarni, A. Arora, “Automating the Addition of Fault Tolerance”, Proc. Formal Techniques in Real Time and Fault Tolerant Systems, pp. 82–93, 2000 Google Scholar
  14. 14.
    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 CrossRefGoogle Scholar
  15. 15.
    Z. Liu, M. Joseph, “Verification of Fault-Tolerance and Real-Time”, Proc. FTCS 1996, pp220–229.Google Scholar
  16. 16.
    F. Salles et al, “Metakernels and fault containment wrappers”, Proc. FTCS, pp. 22–29, 1998Google Scholar
  17. 17.
    G. Smith, “The Object-Z Specification Language. Advances in Formal Methods”, Kluwer Academic Publishers, 2000Google Scholar
  18. 18.
    F. Tip, “A Survey of Program Slicing Techniques,” Journal Prog. Languages Vol.3, No., 3, pp.121–189, Sept. 95Google Scholar
  19. 19.
    V. Wiels, “Modularite pour la conception et la validation formelles de systemes”, PhD thesis, ENSAE-ONERA/CERT/DERI, Oct 97Google Scholar
  20. 20.
    J. Woodcock, J. Davies, “Using Z: Specification, Refinement, and Proof”, Prentice Hall, 1996Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Arshad Jhumka
    • 1
  • Martin Hiller
    • 1
  • Neeraj Suri
    • 1
  1. 1.Department of Computer EngineeringChalmers Univ.Sweden

Personalised recommendations