Model-Checking Processes with States: An Industrial Case Study

• Alexandre Mota UFPE
• Augusto Sampaio UFPE

DOI: https://doi.org/10.5753/sbes.1998.24017

Resumo

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.

Palavras-chave: Model-Checking, Formal Methods, Industrial Case Study, Verification, Tools, Concurrent and Model-Based Specifications

Referências

A. Mota. Formalisation and Analysis of the SACI-1 Microsatellite in CSP-Z (in Portuguese). Master's thesis, Federal University of Pernambuco, 1997.

A. Mota and A. Sampaio. Model-Checking CSP-Z. In Fundamental Approaches to Software Engineering, volume 1382 of LNCS, pages 205-220. Springer-Verlag Berlin, 1998.

T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1):25-59, January 1987.

S. D. Brookes and A. W. Roscoe. An improved failures model for communication processes. In Lecture Notes on Computer Science, volume 197, pages 281-305, 1985.

A. R. de Paula Jr. Fault-Tolerance Aspects of the On-Board Computer of the First INPE Microsatellite for Scientific Applications. VI Brazilian Symposium on Fault-Tolerant Computers, August 1995.

E. Boiten, H. Bowman, J. Derrick and M. Steen. Viewpoint Consistency in Z and LOTOS: A Case Study. In FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, pages 644-664. Springer Verlag, 1997.

C. Fischer. Combining CSP and Z. Technical report, University of Oldenburg, 1996.

C. Fischer. CSP-OZ: A Combination of Object-Z and CSP. In 2nd IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMODDS'97). Chapman Hall, 1997.

Formal Systems (Europe) Ltd. FDR: User Manual and Tutorial, version 2.01, August 1996.

G. Smith. A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. In FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, number 1313 in Lecture Notes in Computer Science, pages 62-81. Springer Verlag, 1997.

C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

J. N. Reed, D. M. Jackson, B. Deianov and G. M. Reed. Automated Formal Analysis of Networks: FDR Models of Arbitrary Topologies and Flow-Control Mechanisms. In Fundamental Approaches to Software Engineering, volume 1382 of LNCS, pages 230-254. Springer-Verlag Berlin, 1998.

X. Jia. A Tutorial of ZANS - A Z Animation System, 1995.

J. L. Lions. Ariane 5 A Falha do Vôo 501. Technical report, http://www.estin.esa.it/htdocs/tidc/Press/Press6/ariane5rep.html, 1996.

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.

A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall International, 1998.

M. Saaltink. The Z/EVES System. In ZUM'97: The Z Formal Specification Notation, pages 72-85. Lecture Notes in Computer Science, 1212, Springer, 1997.

A. Sampaio. An Algebraic Approach to Compiler Design. World Scientific Publishing, 1997.

M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall International, 2nd edition, 1992.