Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Integrated formal verification of safety-critical software

  • FMICS-AVoCS
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

This work presents a formal verification process based on the Systerel Smart Solver (S3) toolset for the development of safety-critical embedded software. In order to guarantee the correctness of the implementation of a set of textual requirements, the process integrates different verification techniques (inductive proof, bounded model checking, test cases generation, and equivalence proof) to handle different types of properties at their best capacities. It is aimed at the verification of properties at system, design, and code levels. To handle the floating-point arithmetic (FPA) in both the design and the code, an FPA library is designed and implemented in S3. This work is illustrated on an Automatic Rover Protection system implemented onboard a robot. Focus is placed on the verification of safety and functional properties and on the equivalence proof between the design model and the generated code.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Notes

  1. S3 is maintained, developed, and distributed by Systerel (http://www.systerel.fr/).

  2. The diversified expanders are designed and implemented by different teams using different programming languages.

  3. Triplex sensor voter case study is provided by Rockwell Collins to make it publicly available to the research community.

  4. The lemma generation is not addressed in our benchmark.

  5. Double precision is quite rare in practice.

  6. The INGEQUIP project is conducted at the IRT-Saint Exupéry. Main partners include academic members from LAAS, IRIT, ONERA, and ISAE; and industrial members from Airbus, Thales, Continental, Airbus D & S, ACTIA, SAGEM, Systerel, etc.

  7. http://projects.laas.fr/tina/home.php.

  8. With respect to the DO178, the Lustre model is considered to express LLRs, since the source code is directly generated from the model with no other interpretation/refinement.

  9. Contact the authors for the specification document, design model, and formal properties.

  10. http://www.scicos.org/.

  11. It is the verification engineer’s duty to translate the natural language requirements to the HLL properties.

  12. Usually, the safety referred by requirements means the system is safe, while the safety referred by properties is related to the deterministic process. Here is the latter case.

  13. Lemma searching is not a must. It is possible that a property is k-inductive.

  14. As explained by the REQ-01-4 in Table 5, we use continuous (continuity) hereafter for the fact that each waypoint has a unique precedent waypoint in a mission or in a reserved area, except that it is the initial one.

  15. Indeterminate means neither valid nor violated, or unknown.

  16. The counterexample of liveness property is a path to a loop that does not contain the desired state. This implies that with an infinite loop path, the system never reaches the specified state.

  17. The translator lus2c is provided by Lustre v4 toolset.

  18. Qualification is a requirement in getting a system certified.

References

  1. Benveniste, A., Berry, G.: The synchronous approach to reactive and real-time systems. Proc. IEEE 79(9), 1270–1282 (1991)

    Article  Google Scholar 

  2. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking Without BDDs. Springer, Berlin (1999)

    Book  MATH  Google Scholar 

  3. Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)

    MATH  Google Scholar 

  4. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Computer Aided Verification, pp. 831–848. Springer, Berlin (2014)

  5. Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Formal Methods in Computer-Aided Design, pp. 409–426. Springer, Berlin (2000)

  6. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: ACM SIGPLAN Notices, vol. 38, pp. 196–207. ACM (2003)

  7. Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D.: Interpolation-based verification of floating-point programs with abstract CDCL. In: Static Analysis, pp. 412–432. Springer, Berlin (2013)

  8. Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Form. Methods Syst. Des. 45(2), 213–245 (2014)

    Article  MATH  Google Scholar 

  9. Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Formal Methods in Computer-Aided Design, 2009. FMCAD 2009, pp. 69–76. IEEE (2009)

  10. Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S., Niebert, P.: From Simulink to SCADE/Lustre to TTA: a layered approach for distributed embedded applications. In: ACM Sigplan Notices, vol. 38, pp. 153–162. ACM (2003)

  11. Champion, A., Delmas, R., Dierkes, M.: Generating property-directed potential invariants by quantifier elimination in a k-induction-based framework. Sci. Comput. Program. 103, 71–87 (2015)

    Article  Google Scholar 

  12. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 93–107. Springer, Berlin (2013)

  13. Clabaut, M., Ge, N., Breton, N., Jenn, E., Delmas, R., Fonteneau, Y.: Industrial grade model checking—use cases, constraints, tools and applications. In: International Conference on Embedded Real Time Software and Systems (2016)

  14. Cody, W.J., Waite, W.M.C.: Software Manual for the Elementary Functions. Prentice-Hall series in computational mathematics. Prentice-Hall, Englewood Cliffs (1980)

    MATH  Google Scholar 

  15. Cuenot, P., Jenn, E., Faure, E., Broueilh, N., Rouland, E.: An experiment on exploiting virtual platforms for the development of embedded equipments. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016)

  16. Cuenot, P., Jenn, E., Faure, E., Broueilh, N., Rouland, E.: An experiment on exploiting virtual platforms for the development of embedded equipments. In: International Conference on Embedded Real Time Software and Systems (2016)

  17. Dajani-Brown, S., Cofer, D., Hartmann, G., Pratt, S.: Formal modeling and analysis of an avionics triplex sensor voter. In: Model Checking Software, pp. 34–48. Springer, Berlin (2003)

  18. De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. Springer, Berlin (2008)

  19. Dierkes, M.: Formal analysis of a triplex sensor voter in an industrial context. In: Formal Methods for Industrial Critical Systems, pp. 102–116. Springer, Berlin (2011)

  20. Dieumegard, A., Ge, N., Jenn, E.: Event-B at work: some lessons learnt from an application to a robot anti-collision function. In: 9th NASA Formal Methods Symposium (NFM 2017) (2017)

  21. Fröhlich, A., Biere, A., Wintersteiger, C.M., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Twenty-Ninth AAAI Conference on Artificial Intelligence (2015)

  22. Ge, N., Dieumegard, A., Jenn, E., d’Ausbourg, B., Aït-Ameur, Y.: Formal development process of safety-critical embedded human machine interface systems. In: Eleventh International Symposium on Theoretical Aspects of Software Engineering (2017)

  23. Ge, N., Dieumegard, A., Jenn, E., Voisin, L.: From event-B to verified C via HLL. ArXiv preprint arXiv:1610.07410 (2016)

  24. Ge, N., Jenn, E., Breton, N., Fonteneau, Y.: Formal verification of a rover anti-collision system. In: International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS-AVoCS 2016), vol. 9933, pp. 171–188 (2016)

  25. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305–1320 (1991)

  26. Harrison, J.: Floating-point verification using theorem proving. In: Formal Methods for Hardware Verification, pp. 211–242. Springer, Berlin (2006)

  27. IEEE Standards Association. IEEE standard for floating-point arithmetic (2008)

  28. Lapschies, F., Peleska, J., Gorbachuk, E., Mangels, T.: Sonolar SMT-solver. In: Satisfiability Modulo Theories Competition; System Description (2012)

  29. Leeser, M., Mukherjee, S., Ramachandran, J., Wahl, T.: Make it real: effective floating-point reasoning via exact arithmetic. In: Design, Automation and Test in Europe Conference and Exhibition (DATE), 2014, pp. 1–4. IEEE (2014)

  30. McMillan, K.L.: Interpolation and SAT-based model checking. In: Computer Aided Verification, pp. 1–13. Springer, Berlin (2003)

  31. Meseguer, J., Ölveczky, P.C.: Formalization and correctness of the pals architectural pattern for distributed real-time systems. In: International Conference on Formal Engineering Methods, pp. 303–320. Springer, Berlin (2010)

  32. Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. (TOPLAS) 30(3), 12 (2008)

    Article  Google Scholar 

  33. Roux, P., Jobredeaux, R., Garoche, P.-L.: Closed loop analysis of control command software. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 108–117. ACM (2015)

  34. RTCA DO. 178c.: Software Considerations in Airborne Systems and Equipment Certification (2011)

  35. RTCA DO. 330.: Software Tool Qualification Considerations (2011)

  36. Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT), p. 151 (2010)

  37. Rushby, J.: Integrated formal verification: using model checking with automated abstraction, invariant generation, and theorem proving. In: Theoretical and Practical Aspects of SPIN Model Checking, pp. 1–11. Springer, Berlin (1999)

  38. Sha, L., Al-Nayeem, A., Sun, M., Meseguer, J., Olveczky, P.C.: PALS: physically asynchronous logically synchronous systems. Technical report, University of Illinois (2009)

  39. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Formal Methods in Computer-Aided Design, pp. 127–144. Springer, Berlin (2000)

  40. Zave, P., Jackson, M.: Four dark corners of requirements engineering. ACM Trans. Softw. Eng. Methodol. (TOSEM) 6(1), 1–30 (1997)

    Article  Google Scholar 

Download references

Acknowledgements

This work has been funded by the INGEQUIP project. The authors would like to thank the members in the project for their good cooperation. We are thankful to Rémi Delmas and Michael Dierkes for sharing the experimental results on the TSV use case and their expertise. The authors want to express appreciation to the anonymous reviewers for their constructive and helpful comments.

Author information

Authors and Affiliations

  1. School of Software, Beihang University, Beijing, China

    Ning Ge

  2. IRT-Saint Exupéry, Toulouse, France

    Ning Ge & Eric Jenn

  3. Systerel, Toulouse, France

    Ning Ge, Nicolas Breton & Yoann Fonteneau

  4. Thales Avionics, Toulouse, France

    Eric Jenn

Authors
  1. Ning Ge
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eric Jenn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nicolas Breton
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yoann Fonteneau
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ning Ge.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ge, N., Jenn, E., Breton, N. et al. Integrated formal verification of safety-critical software. Int J Softw Tools Technol Transfer 20, 423–440 (2018). https://doi.org/10.1007/s10009-017-0475-0

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-017-0475-0

Keywords

Search

Navigation