Formal Methods for the International Space Station ISS

  • Jan Peleska
  • Bettina Buth
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)


This article summarises and evaluates the results and experiences obtained from a verification, simulation and test suite for a faulttolerant computer system designed and developed by DaimlerChrysler Aerospace for the International Space Station ISS. Verification and testing focused on various aspects of system correctness which together ensure a high degree of trustworthiness for the system. The verification and test approach is based on CSP specifications, the model-checking tool FDR and the test automation tool RT-Tester. Furthermore, Generalised Stochastic Petri Nets (GSPN) have been used with the tools DSPN-Express and TimeNet to perform a statistical throughput analysis by means of simulation. The objective of this article is to present, motivate and evaluate our approach that strongly relied on the combination of different methods, techniques and tools in order to increase the overall efficiency of the verification, simulation and test suite. The isolated techniques applied are illustrated by small examples; for details, references to other publications are given.


Fault-Tolerant Systems Byzantine Agreement Protocol Formal Verification CSP Test Automation Model Checking Generalised Stochastic Petri Nets Hardware-in-the-loop Test International Space Station 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Booch, G., Rumbaugh, J. and Jacobsen, I.: The Unified Modeling Language User Guide. Addison-Wesley (1998).Google Scholar
  2. 2.
    Booch, G., Rumbaugh, J. and Jacobsen, I.: The Unified Modeling Language Reference Manual. Addison-Wesley (1999).Google Scholar
  3. 3.
    Buth, B., Cardell-Oliver, R., Peleska, J.: Combining tools for the verification of fault-tolerant systems. In Berghammer, R., Buth, B., Peleska, J. (eds.), Tools for Software Development and Verification, Monographs of the Bremen Institute of Safe Systems 1, Shaker Verlag, (1998), ISBN 3-8265-3806-4.Google Scholar
  4. 4.
    Bettina Buth: PAMELAtPVS (Abstract for Tool Demo) InMichael Johnson (Ed.): Algebraic Methodology and Software Technology. Proceedings of the AMAST‘97, Sidney, Australia, December 1997, Springer LNCS 1349 (1997), 560–562.CrossRefGoogle Scholar
  5. 5.
    Buth, B., Kouvaras, M., Peleska, J., Shi, H.: Deadlock analysis for a fault-tolerant system. In Johnson, M. (ed.), Algebraic Methodology and Software Technology. Proceedings of the AMAST‘97, number 1349 in LNCS, pages 60–75. Springer, December 1997.CrossRefGoogle Scholar
  6. 6.
    Buth, B., Peleska, J., Shi, H.: Combining Methods for the Livelock Analysis of a Fault-Tolerant System. In A. M. Haeberer (Ed.): Algebraic Methodology and Software Technology. Proceedings of the 7th International Conference, AMAST 98, Amazonia, Brazil, January 1999. Springer LNCS 1548, pp. 124–139, 1998.CrossRefGoogle Scholar
  7. 7.
    Buth, B., Peleska, J., Shi, H.: Combining Methods for the Analysis of a Fault-Tolerant System. CD-ROM Proceedings of the 12th International Software Quality Week, May 24-28, 1999, Software Research Institute.Google Scholar
  8. 8.
    Dierks, H.: PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, Transformation-Based Reactive Systems Development (ARTS‘97), volume 1231 of Lecture Notes in Computer Science, pages 111–125. Springer-Verlag, 1997.Google Scholar
  9. 9.
    Formal Systems: FDR2 User Manual Formal Systems (Europe) Lts (1997). Available under
  10. 10.
    Gamma, E., Helm, R., Johnson, R. and Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software Addison-Wesley (1995)Google Scholar
  11. 11.
    D. Harel, A. Pnueli, J. Pruzan-Schmidt and R. Sherman. On the formal semantics of Statecharts. In Proceedings Symposium on Logic in Computer Science, (1987) 54–64.Google Scholar
  12. 12.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985).Google Scholar
  13. 13.
    Lamport, L., Shostak, R., Pease, M.: The Byzantine Generals Problem, In: ACM Transactions on Programming Languages and Systems, Vol.4, Nr. 3, (1982)Google Scholar
  14. 14.
    Lankenau, A., Meyer, O. and Krieg-Brückner, B.: Safety in Robotics: The Bremen Autonomous Wheelchair. In: Proceedings of AMC‘98-Coimbra, 5th Int.Workshop on Advanced Motion Control, Coimbra, Portugal 1998. ISBN 0-7803-4484-7. pp. 524-529.Google Scholar
  15. 15.
    Lankenau, A., Meyer, O.: Formal Methods in Robotics: Fault Tree Based Verification. Submitted to Quality Week Europe 99.Google Scholar
  16. 16.
    R.S. Lazićc: Theories for mechanical verification of data-independent CSP, Oxford University Computing Laboratory technical report, 1997.Google Scholar
  17. 17.
    Lyu, M. R. (ed.): Handbook of Software Reliability Engineering, IEEE Computer Society Press, Computing McGraw-Hill (1995).Google Scholar
  18. 18.
    Milner, R.:Communication and Concurrency. Prentice-Hall International (1989).Google Scholar
  19. 19.
    J. Peleska: Test Automation for Safety-Critical Systems: Industrial Application and Future Developments. In M.-C. Gaudel and J. Woodcock (Eds.): FME ‘96: Industrial Benefit and Advances in Formal Methods. LNCS 1051, Springer-Verlag, Berlin Heidelberg New York (1996) 39–59.Google Scholar
  20. 20.
    J. Peleska: Formal Methods and the Development of Dependable Systems. Habilitationsschrift, Bericht Nr. 9612, Dezember 1996, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel (1997).Google Scholar
  21. 21.
    J. Peleska and M. Siegel: Test Automation of Safety-Critical Reactive Systems. South African Computer Jounal (1997)19:53–77.Google Scholar
  22. 22.
    Peleska, J.: Testing Reactive Real-Time Systems. Tutorial, held at the FTRTFT ‘98. Denmark Technical University, Lyngby (1998).Google Scholar
  23. 23.
    J. Peleska and C. Zahlten: Test Automation for Avionic Systems and Space Technology (Extended Abstract). Softwaretechnik-Trends (1999)19:34–36.Google Scholar
  24. 24.
    Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice-Hall International (1998).Google Scholar
  25. 25.
    Shi, H., Peleska, J.: Daimler-Benz Aerospace-Project DMS-R, FTC Development-Fault Management Layer (FML): Verification of Byzantine Agreement Protocol Implementation. Technical Report, JP Software-Consulting, (1998).Google Scholar
  26. 26.
    Schneider, S.: An Operational Semantics for Timed CSP. Information and Computation, 116:193–213, 1995.zbMATHGoogle Scholar
  27. 27.
    Shi, H., Peleska, J. and Kouvaras, M: Combining Methods for the Analysis of a Fault-Tolerant System. Submitted to 1999 Pacific Rim International Symposium on Dependable Computing (PRDC 1999).Google Scholar
  28. 28.
    M. J. Spivey. The Z Notation. Prentice-Hall International, Englewood Cliffs NJ (1992).Google Scholar
  29. 29.
    Storey, N.: Safety-Critical Computer Systems. Addison-Wesley (1996).Google Scholar
  30. 30.
    L. Twele, H. Schlinglo, H. Szczerbicka: Performability Analysis of an Avionics-Interface; Proc. IEEE Conf. on Systems, Man and Cybernetics; San Diego, N.J., pp. 499–504, (Oct. 1998)Google Scholar
  31. 31.
    Gerd Urban, Hans-Joachim Kolinowitz and Jan Peleska: A Survivable Avionics System for Space Applications. Published in Proceedings of the FTCS-28, 28th Annual Symposium on Fault-Tolerant Computing, Munich, June 23-25, 1998, 372–381.Google Scholar
  32. 32.
    Zhiming Liu, E. V. Sørensen, A. P. Ravn and Chaochen Zhou: Towards a Calculus of System Dependability. Journal of high integrity systems (1994) 1: 49–65.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Jan Peleska
    • 1
    • 2
  • Bettina Buth
    • 1
  1. 1.TZI-BISSUniversity of BremenBremen
  2. 2.Verified Systems International GmbHBremen

Personalised recommendations