TY - GEN
T1 - Rigorous evidence of freedom from concurrency faults in industrial control software
AU - Bonichon, Richard
AU - Canet, Géraud
AU - Correnson, Loïc
AU - Goubault, Eric
AU - Haucourt, Emmanuel
AU - Hirschowitz, Michel
AU - Labbé, Sébastien
AU - Mimram, Samuel
PY - 2011/9/26
Y1 - 2011/9/26
N2 - 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.
AB - 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.
KW - Digital control systems
KW - concurrency
KW - deadlock
KW - formal verification
KW - software dependability
U2 - 10.1007/978-3-642-24270-0_7
DO - 10.1007/978-3-642-24270-0_7
M3 - Conference contribution
AN - SCOPUS:80053031596
SN - 9783642242694
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 85
EP - 98
BT - Computer Safety, Reliability, and Security - 30th International Conference, SAFECOMP 2011, Proceedings
T2 - 30th International Conference on Computer Safety, Reliability and Security, SAFECOMP 2011
Y2 - 19 September 2011 through 22 September 2011
ER -