CERN Accelerating science

Article
Report number	CERN-TS-2008-010
Title	Safety testing for LHC access system
Author(s)	Valentini, F (CERN) ; Ladzinski, T (CERN) ; Ninin, P (CERN) ; Scibile, S (CERN)
Publication	2008
Imprint	22 Jun 2008
Number of pages	5
In:	11th European Particle Accelerator Conference, Genoa, Italy, 23 - 27 Jun 2008, pp.MOPD037
Subject category	Engineering ; Accelerators and Storage Rings
Accelerator/Facility, Experiment	CERN LHC
Abstract	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.
Copyright/License	publication: (License: CC-BY)

Corresponding record in: EDMS ; Inspire
Email contact: evelyne.cochet@cern.ch