Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software

  • Richard Bonichon
  • Géraud Canet
  • Loïc Correnson
  • Eric Goubault
  • Emmanuel Haucourt
  • Michel Hirschowitz
  • Sébastien Labbé
  • Samuel Mimram
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6894)


In the power generation industry, digital control systems may play an important role in plant safety. Thus, these systems are the object of rigorous analyzes and safety assessments. In particular, the quality, correctness and dependability of control systems software need to be justified. This paper reports on the development of a tool-based methodology to address the demonstration of freedom from intrinsic software faults related to concurrency and synchronization, and its practical application to an industrial control software case study. We describe the underlying theoretical foundations, the main mechanisms involved in the tools and the main results and lessons learned from this work. An important conclusion of the paper is that the used verification techniques and tools scale efficiently and accurately to industrial control system software, which is a major requirement for real-life safety assessments.


Digital control systems software dependability formal verification concurrency deadlock 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: PLDI, pp. 128–140 (2003)Google Scholar
  2. 2.
    Baier, C., Katoen, J.P.: Principles of Model-Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  3. 3.
    Balabonski, T., Haucourt, E.: A geometric approach to the problem of unique decomposition of processes. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 132–146. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. 4.
    Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: POPL, pp. 1–3 (2002)Google Scholar
  5. 5.
    Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. STTT 10(5), 401–424 (2008)CrossRefGoogle Scholar
  6. 6.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT 9(5-6), 505–525 (2007)CrossRefGoogle Scholar
  8. 8.
    Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model checker. STTT 2(4), 410–425 (2000)CrossRefzbMATHGoogle Scholar
  9. 9.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  10. 10.
    Cuoq, P., Prevosto, V.: Frama-c’s value analysis plug-in. CEA LIST Technical Report (2010),
  11. 11.
    Cuoq, P., Signoles, J., Baudin, P., Bonichon, R., Canet, G., Correnson, L., Monate, B., Prevosto, V., Puccetti, A.: Experience report: OCaml for an industrial-strength static analysis framework. In: ICFP, pp. 281–286 (2009)Google Scholar
  12. 12.
    CWE Common Weakness Enumeration —,
  13. 13.
    Dijkstra, E.W.: Cooperating sequential processes. In: Programming Languages: NATO Advanced Study Institute, pp. 43–112. Academic Press, London (1968)Google Scholar
  14. 14.
    Dräger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: Slab: A certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 271–274. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Emanuelsson, P., Nilsson, U.: A Comparative Study of Industrial Static Analysis Tools. Linköpink University Technical Report (2008)Google Scholar
  16. 16.
    Fajstrup, L., Goubault, E., Raußen, M.: Algebraic topology and concurrency. Theoretical Computer Science 357, 241–278 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Frama-c Software Analyzers —,
  18. 18.
    Goubault, E.: Geometry and concurrency: a user’s guide. Mathematical Structures in Computer Science 10(4), 411–425 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Goubault, E., Haucourt, E.: A practical application of geometric semantics to static analysis of concurrent programs. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 503–517. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    Grandis, M.: Directed Algebraic Topology. New Mathematical Monographs. Cambridge University Press, Cambridge (2009)CrossRefzbMATHGoogle Scholar
  21. 21.
    Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)Google Scholar
  22. 22.
    Holzmann, G.J., Ruys, T.C.: Effective bug hunting with spin and modex. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, p. 24. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    Labbé, S., Sangnier, A.: Formal verification of industrial software with dynamic memory management. In: IEEE PRDC. pp. 77–84 (2010)Google Scholar
  24. 24.
    Labbé, S., Thuy, N.: Formal verification of freedom from intrinsic software faults in digital control systems. In: ANS NPIC&HMIT, pp. 2191–2201 (2010)Google Scholar
  25. 25.
    Larochelle, D., Evans, D.: Statically detecting likely buffer overflow vulnerabilities. In: USENIX Security Symposium, pp. 177–190 (2001)Google Scholar
  26. 26.
    Nachbin, L.: Topology and Order. Mathematical Studies, vol. 4. Van Nostrand, Princeton (1965)zbMATHGoogle Scholar
  27. 27.
    Podelski, A., Rybalchenko, A.: Armc: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  28. 28.
    Thuy, N., Ourghanlian, A.: Dependability assessment of safety-critical system software by static analysis methods. In: DSN, pp. 75–79 (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Richard Bonichon
    • 1
  • Géraud Canet
    • 1
  • Loïc Correnson
    • 1
  • Eric Goubault
    • 1
  • Emmanuel Haucourt
    • 1
  • Michel Hirschowitz
    • 1
  • Sébastien Labbé
    • 2
  • Samuel Mimram
    • 1
  1. 1.CEA, LISTGif-sur-YvetteFrance
  2. 2.EDF Research & DevelopmentChatouFrance

Personalised recommendations