Paper Info
Title
An experience in embedded control software verification
Abstract
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.
Year
DOI
Venue
2009
10.1109/ETFA.2009.5347235
Mallorca
Keywords
Field
DocType
concurrency control,control engineering computing,operating systems (computers),program verification,C++,CalRoc2003,SPIN model checker,automatic model extraction tool,concurrency problem,embedded control software verification,formal verification
Programming language,Concurrency control,Computer science,Concurrency,Real-time computing,Software,Software verification and validation,Software construction,Software verification,Formal verification,SPIN model checker
Conference
ISSN
ISBN
Citations 
1946-0759 E-ISBN : 978-1-4244-2728-4
978-1-4244-2728-4
0
PageRank 
References 
Authors
0.34
4
2
Name
Order
Citations
PageRank
Pierluigi Rolando100.34
Riccardo Sisto255656.79