Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Using Formal Verification Techniques to Reduce Simulation and Test Effort

  • Conference paper
  • First Online:
FME 2001: Formal Methods for Increasing Software Productivity (FME 2001)

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

Included in the following conference series:

Abstract

This paper describes an experiment in using formal methods in an industrial context. The goal is to use formal verification techniques in order to alleviate the simulation and test activities. The application is a flight control computer of the Airbus A340.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Caspi, N. Halbwachs, P. Pilaud, and P. Raymond. The synchronous dataflow programming language Lustre. Proceedings of IEEE, Another Look at Real-time programming, 79(9): 1305–1319, September 1991.

    Google Scholar 

  2. N. Halbwachs, Lagnier F., and Raymond P. Synchronous observer and the verification of reactive systems. In Third International Conference on Algebraic Methodology and Software Technology, AMAST’93, Twente, June 93.

    Google Scholar 

  3. N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real time systems by means of the synchronous data-flow language Lustre. IEEE Transactions on Software Engineering, special issue on the specification and analysis of real time systems, september 1992.

    Google Scholar 

  4. Magnus Ljung. Formal modelling and automatic verification of Lustre programs using np-tools. Master’s thesis, Royal Institute of Technology, Department of Tele-informatics, 1999.

    Google Scholar 

  5. Prover Technology AB. NP-Tools 2.4 Reference manual, 1999.

    Google Scholar 

  6. C. Ratel. Définition et réalisation d’un outil de vérification formelle de programmes Lustre: le système LESAR. PhD thesis, Institut National Polytechnique de Grenoble, Juillet 1992.

    Google Scholar 

  7. Mary Sheeran and Gunnar Stalmarck. A tutorial on Stalmarck’s proof procedure for propositional logic. In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), LNCS. Springer Verlag, 1998.

    Google Scholar 

  8. Verilog. SCADE Language-Reference Manual 2.1.

    Google Scholar 

  9. Verimag. Lustre/lesar home page. http://www-verimag.imag.fr/SYNCHRONE/lustre-english.html.

Download references

Author information

Authors and Affiliations

  1. EADS-Airbus SA, A/BTE/SY/MS, 316 route de Bayonne, 31000, Toulouse cedex 03, France

    O. Laurent

  2. ONERA-CERT/DTIM, BP 4025, 2 avenue E. Belin, 31055, Toulouse Cedex 4, France

    P. Michel & V. Wiels

Authors
  1. O. Laurent
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. Michel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. V. Wiels
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Minho, Campus de Gualtar, 4700-320, Braga, Portugal

    José Nuno Oliveira

  2. AT&T Laboratories — Research, 180 Park Avenue, Florham Park, New Jersey, 07932, USA

    Pamela Zave

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Laurent, O., Michel, P., Wiels, V. (2001). Using Formal Verification Techniques to Reduce Simulation and Test Effort. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_27

Download citation

  • DOI: https://doi.org/10.1007/3-540-45251-6_27

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41791-0

  • Online ISBN: 978-3-540-45251-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation