Skip to main content
SpringerLink
Log in

Proof-based system engineering and embedded systems

  • Development and Engineering
  • Chapter
  • First Online:
Lectures on Embedded Systems (EEF School 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1494))

Included in the following conference series:

Abstract

We introduce basic principles that underlie proof-based system engineering, an engineering discipline aimed at computer-based systems. This discipline serves to avoid system engineering faults. It is based upon fulfilling proof obligations, notably establishing proofs that decisions regarding system design and system dimensioning are correct, before embarking on the implementation or the fielding of a computer-based system. We also introduce a proof-based system engineering method which has been applied to diverse projects involving embedded systems. These projects are presented and lessons learned are reported. An analysis of the Ariane 5 Flight 501 failure serves to illustrate how proof-based system engineering also helps in diagnosing causes of failures.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bernstein, P. A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley Pub., ISBN 0-201-10715-5 (1987) 370 p.

    Google Scholar 

  2. Gaubert S., Max Plus: Methods and Applications of (max, +) Linear Algebra, INRIA Research Report 3088 (Jan. 1997) 24 p.

    Google Scholar 

  3. Hadzilacos, V., Toueg, S.: A Modular Approach to Fault-Tolerant Broadcasts and Related Problems, Technical Report, TR 94-1425, Cornell University (May 1994).

    Google Scholar 

  4. Hermant, J.F., Le Lann, G.: A Protocol and Correctness Proofs for Real-Time High-Performance Broadcast Networks, 18th IEEE Intl. Conference on Distributed Computing Systems, Amsterdam, NL (May 1998) 10 p.

    Google Scholar 

  5. Hermant, J.F., Leboucher, L., Rivierre, N.: Real-Time Fixed and Dynamic Priority Driven Scheduling Algorithms: Theory and Experience. INRIA Research Report 3081 (Dec. 1996) 139 p.

    Google Scholar 

  6. Inquiry Board Report: Ariane 5-Flight 501 Failure, Paris (19 July 1996) 18 p. [http://www.inria.fr/actualites-fra.html].

    Google Scholar 

  7. Joseph, M., et al.: Real-Time Systems-Specification, Verification and Analysis. Prentice Hall UK Pub., ISBN 0-13-455297-0 (1996) 278 p.

    Google Scholar 

  8. Knightly E.W., Zhang Hui: D-BIND: An Accurate Traffic Model for Providing QoS Guarantees to VBR Traffic. IEEE/ACM Transactions on Networking, vol. 5, n°2 (April 1997) 219–231.

    Google Scholar 

  9. Koren, G., Shasha, D.: D-Over: An Optimal On-Line Scheduling Algorithm for Overloaded Real-Time Systems, INRIA Technical Report 138 (Feb. 1992) 45 p.

    Google Scholar 

  10. Kuhn, DR.: Sources of Failure in the Public Switched Telephone Network, IEEE Computer (April 1997) 31–36.

    Google Scholar 

  11. Le Lann, G.: Certifiable Critical Complex Computing Systems. 13th IFIP World Computer Congress, Duncan K. and Krueger K. Eds, Elsevier Science Pub., vol. 3, Hamburg, D (Aug. 1994) 287–294.

    Google Scholar 

  12. Le Lann, G.: Proof-Based System Engineering for Computing Systems, ESA-INCOSE Conference on Systems Engineering, Noordwijk, NL (Nov. 1997) IEE/ESA Pub., vol. WPP-130, 5a.4.1–5a.4.8.

    Google Scholar 

  13. Le Lann, G.: An Analysis of the Ariane 5 Flight 501 Failure-A System Engineering Perspective. IEEE Intl. Conference on the Engineering of Computer-Based Systems, Monterey, USA (March 1997) 339–346.

    Google Scholar 

  14. Leveson, N.G., Turner, C.: An Investigation of the Therac-25 Accidents, IEEE Computer (July 1993) 18–41.

    Google Scholar 

  15. Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Pub., ISBN 1-55860-348-4 (1996) 872 p.

    Google Scholar 

  16. Neumann, P.G.: Computer Related Risks, Addison-Wesley Pub., ISBN 0-201-55805-X (1995) 367 p.

    Google Scholar 

  17. Powell, D.: Failure Mode Assumptions and Assumption Coverage, 22nd IEEE Intl. Symposium on Fault-Tolerant Computing, Boston, USA (July 1992) 386–395.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, Projet REFLECS, BP 105, F-78153, Le Chesnay Cedex, France

    Gerard Le Lann

Authors
  1. Gerard Le Lann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Grzegorz Rozenberg Frits W. Vaandrager

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Le Lann, G. (1998). Proof-based system engineering and embedded systems. In: Rozenberg, G., Vaandrager, F.W. (eds) Lectures on Embedded Systems. EEF School 1996. Lecture Notes in Computer Science, vol 1494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-65193-4_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-65193-4_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65193-2

  • Online ISBN: 978-3-540-49498-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation