Model-Checking Processes with States: An Industrial Case Study - Mota, Alexandre; Sampaio, Augusto (Anais do Simpósio Brasileiro de Engenharia de Software (SBES); 1998: Anais do XII Simpósio Brasileiro de Engenharia de SoftwareDO - 10.5753/sbes.1998.24017, 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.