Model-Checking Processes with States: An Industrial Case Study
Alexandre Mota, Augusto C. A. Sampaio · 1998
ln this paper we present a formal specification of part of the SACI-1 microsatellite on-board computer whose development is led by the Brazilian Space Research Institute (INPE). The specification is written in CSP-Z, a specification language that integrates CSP (which allows one to focus on the concurrent aspects of the application) and Z (for modeling the relevant data structures). We also describe a strategy for model-checking processes with states (developed by the authors) and its implementation using the FOR model-checker. Finally, using this tool, we carry out an automatic proof that the SACI-1 specification is deadlock-free.