For the most recent entries see the Petri Nets Newsletter.

Specification and Validation of the SACI-1 On-Board Computer Using Timed-CSP-Z and Petri Nets.

Sherif, Adnan; Sampaio, Augusto; Cavalcante, Sérgio

In: Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (ICATPN 2003), Eindhoven, The Netherlands, June 23-27, 2003, pages 161-180. Volume 2679 of Lecture Notes in Computer Science / Wil M. P. van der Aalst and Eike Best (Eds.) --- Springer-Verlag, June 2003.

Abstract: In this paper we focus on the application of integrated formal methods to the specification and validation of a fault tolerant real-time system (the on-board computer of a Brazilian micro-satellite). The work involves the application of a framework which covers from the formal specification to the analysis and use of tools to prove properties of the system. We used Timed-CSP-Z, a combination of Timed CSP and Z, to specify the system behavior, and then a strategy for converting the specification to TER Nets, a high level Petri Nets based formalism with time. The conversion enables us to use the CABERNET tool to analyse the behavior of the system.

Keywords: Real-time Systems; Case Studies; Time CSP; Z.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography