Integrating trace logic and Petri nets specifications

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.