This paper presents an experience in formal method integration for the specification and validation of distributed fault-tolerant systems. The specification formalisms we deal with are trace logic, based on CSP (communicating sequential processes) theory, and stochastic Petri nets. Their integration allows us to combine the power of event traces (to specify the behaviour of a system in an intuitive and modular way) with the power of Petri nets (for the analysis of concurrent systems). The integrated specification technique is discussed by applying it to a real industrial control system, which uses redundant modules to guarantee given operational conditions, despite failures, and incorporates a voting algorithm for arbitration over the replicated units.

Integrating trace logic and Petri nets specifications

MAZZOCCA, NICOLA;RUSSO, STEFANO;VITTORINI, VALERIA
1997

Abstract

This paper presents an experience in formal method integration for the specification and validation of distributed fault-tolerant systems. The specification formalisms we deal with are trace logic, based on CSP (communicating sequential processes) theory, and stochastic Petri nets. Their integration allows us to combine the power of event traces (to specify the behaviour of a system in an intuitive and modular way) with the power of Petri nets (for the analysis of concurrent systems). The integrated specification technique is discussed by applying it to a real industrial control system, which uses redundant modules to guarantee given operational conditions, despite failures, and incorporates a voting algorithm for arbitration over the replicated units.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11588/192470
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact