An experience in embedded control software verification

We report on our experience with the formal verification of CalRoc2003, the software that controls the scientific payload for the SCORE coronographic experiment. Our target was using the state-of-the-art SPIN model checker for spotting concurrency problems that could have gone undetected in the traditional testing phase. Some challenges had to be faced in this task. Since the software interacts heavily with the operating system for inter-process communication and process management, the relevant OS primitives had to be modelled. Moreover, since CalRoc2003 is written in C++, the automatic model extraction tools coming with SPIN are inapplicable because they only target C programs, and models had to be extracted manually. Even with these difficulties, the verification proved useful in detecting some subtle problems in the software.