Safety testing for LHC access system
Francesco Valentini, P. Ninin, S Scibile, Tomasz Ladzinski · International Linear Collider · 2008
In the domain of Safety Real-Time Systems the problem of testing represents always a big effort in terms of time, costs and efficiency to guarantee an adequate coverage degree. Exhaustive tests may, in fact, not be practicable for large and distributed systems. This paper describes the testing process followed during the validation of the CERN's LHC Access System [1], responsible for monitoring and preventing physical risks for the personnel accessing the underground areas. In the paper we also present a novel strategy for the testing problem, intended to drastically reduce the time for the test patterns generation and execution. In particular, we propose a methodology for blackbox testing that relies on the application of Model Checking techniques. Model Checking is a formal method from computer science, commonly adopted to prove correctness of system’s models through an automatic system’s state space exploration against some property formulas.