Advertisement

A Formal Basis for Some Dependability Notions

  • Cliff B. Jones
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2757)

Abstract

This paper shows how formal methods ideas can be used to clarify basic notions used in the field of dependability. Central to this endeavour is fixing a notion of system. Relationships between systems are also considered: in particular, the importance of the situation where one system is generated by another (possibly human) system is explored. The formalisation is used as a basis for definitions of the notions of fault, error and failure. Some applications to examples from the dependability literature and extensions of the basic model of system are also sketched.

Keywords

Formal Basis Process Algebra Proof Obligation Error Recovery Concurrent System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abr96.
    Abrial, J.-R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)MATHCrossRefGoogle Scholar
  2. AKKB99.
    Astesiano, E., Kreowski, H.-J., Krieg-Bruckner, B. (eds.): Algebraic Foundations of Systems Specification. Springer, Heidelberg (1999)Google Scholar
  3. Ame89.
    America, P.: Issues in the design of a parallel object-oriented language. Formal Aspects of Computing 1(4) (1989)Google Scholar
  4. Col94.
    Collette, P.: Design of Compositional Proof Systems Based on Assumption-Commitment Specifications – Application to UNITY. PhD thesis, Louvain-la-Neuve (June 1994)Google Scholar
  5. dR01.
    de Roever, W.P.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)MATHGoogle Scholar
  6. Hay93.
    Hayes, I. (ed.): Specification Case Studies, 2nd edn. Prentice Hall International, Englewood Cliffs (1993)MATHGoogle Scholar
  7. Jon83.
    Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321–332. North-Holland, Amsterdam (1983)Google Scholar
  8. Jon87.
    Jones, C.B.: Program specification and verification in VDM. In: Broy, M. (ed.) Theory of Program Structures. NATO ASI Series F: Computer and Systems Sciences, vol. 36, pp. 149–184. Springer, Heidelberg (1987)Google Scholar
  9. Jon89.
    Jones, C.B.: Data reification. In: McDermid, J.A. (ed.) The Theory and Practice of Refinement, Butterworths, pp. 79–89 (1989)Google Scholar
  10. Jon90.
    Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall International, Englewood Cliffs (1990) ISBN 0-13-880733-7MATHGoogle Scholar
  11. Jon94.
    Jones, C.B.: Process algebra arguments about an object-based design notation. In: Roscoe, A.W. (ed.) A Classical Mind. ch. 14, pp. 231–246. Prentice-Hall, Englewood Cliffs (1994)Google Scholar
  12. Jon99.
    Jones, C.B.: Scientific decisions which characterise VDM. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 28–47. Springer, Heidelberg (1999)Google Scholar
  13. Jon00.
    Jones, C.B.: Compositionality, interference and concurrency. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Milennial Perspectives in Computer Science, pp. 175–186. Macmillian Press (2000)Google Scholar
  14. JRW02.
    Jones, C., Romanovsky, A., Welch, I.: A structured approach to handling on-line interface upgrades. In: Proceedings of COMPSAC (2002) (to appear in)Google Scholar
  15. Kop02a.
    Kopetz, H.: On the specification of linking interfaces in distributed real-time systems. Technical Report 2002/8, Institut fuer Technische Informatik, TU Vienna (2002)Google Scholar
  16. Kop02b.
    Kopetz, H.: Real-Time Systems. Kluwer, Dordrecht (2002)Google Scholar
  17. Lap92.
    Laprie, J.-C.: Dependability: basic concepts and terminology—in English, French, German, Italian and Japanese. Springer, Heidelberg (1992)MATHGoogle Scholar
  18. LT93.
    Levenson, N.G., Turner, C.S.: An investigation of the Therac-25 accidents. Computer, 18–41 (July 1993)Google Scholar
  19. Mar86.
    Marshall, L.S.: A Formal Description Method for User Interfaces. PhD thesis, University of Manchester (1986)Google Scholar
  20. MH91.
    Mahony, B., Hayes, I.: Using continuous real functions to model timed histories. In: Bailes, P. (ed.) Engineering Safe Software, pp. 257–270. Australian Computer Society (1991)Google Scholar
  21. MPW92.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100, 1–77 (1992)MATHCrossRefMathSciNetGoogle Scholar
  22. Nip86.
    Nipkow, T.: Non-deterministic data types: Models and implementations. Acta Informatica 22, 629–661 (1986)MATHCrossRefMathSciNetGoogle Scholar
  23. Nip87.
    Nipkow, T.: Behavioural Implementation Concepts for Nondeterministic Data Types. PhD thesis, University of Manchester (May 1987)Google Scholar
  24. Per99.
    Perrow, C.: Normal Accidents. Princeton University Press, Princeton (1999)Google Scholar
  25. Ran00.
    Randell, B.: Facing up to faults. The Computer Journal 43(2), 95–106 (2000)CrossRefGoogle Scholar
  26. Rea90.
    Reason, J.: Human Error. Cambridge University Press, Cambridge (1990)Google Scholar
  27. Rea97.
    Reason, J.: Managing the Risks of Organisational Accidents. Ashgate Publishing Limited (1997)Google Scholar
  28. Rus99.
    Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. In: Proceedings of 3rd Workshop on Human Error, HESSD 1999, pp. 1–18 (1999)Google Scholar
  29. San99.
    Sangiorgi, D.: Typed π-calculus at work: a correctness proof of Jones’s parallelisation transformation on concurrent objects. Theory and Practice of Object Systems 5(1), 25–34 (1999)CrossRefMathSciNetGoogle Scholar
  30. SO02.
    Sala-Oliveras, C.: Systems, advisory systems and safety (2002) Private communicationGoogle Scholar
  31. Sti88.
    Stirling, C.: A generalisation of Owicki-Gries’s Hoare logic for a concurrent while language. TCS 58, 347–359 (1988)MATHCrossRefMathSciNetGoogle Scholar
  32. Stø90.
    Stølen, K.: Development of Parallel Programs on Shared Data-Structures. PhD thesis, Manchester University, available as UMCS-91-1-1 (1990)Google Scholar
  33. SW01.
    Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambrisge University Press, Cambridge (2001)Google Scholar
  34. Wal91.
    Walker, D.: π-calculus semantics for object-oriented programming languages. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 532–547. Springer, Heidelberg (1991)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Cliff B. Jones
    • 1
  1. 1.School of Computing Science University of NewcastleUK

Personalised recommendations