| Paper |
Title |
Page |
| MOPD037 |
Safety Testing for LHC Access System
|
532 |
| |
- F. Valentini, T. Ladzinski, P. Ninin, L. Scibile
CERN, Geneva
|
|
| |
This paper presents the validation and verification activities carried out for the LHC Access Control and Safety System. It also presents a new strategy for the future that includes the application of formal methods based on model checking techniques, commonly used to prove the correctness of software algorithms or system functional specifications through automatic exploration of the system state space. We will show how to apply these techniques in order to automate the testing process. The paper also presents the results of the performances and the applicability of a series of tools that have been tested in order to carry out a formal correctness proof for the LHC Access System.
|
|