In: Proc. 30th Annual Hawaii Int. Conf. on System Sciences; Vol. 1: Software Technology and Architecture, 7-10 January 1997, Wailea, HI, pages 443-451. January 1997.
Abstract: This paper presents an experience in formal methods integration for the specification and validation of distributed, fault-tolerant systems. Trace logic, based on the CSP theory and stochastic Petri nets are used for the specification formalism. Their integration allows to combine the power of event traces to specify the behavior of a system in an intuitive and modular way and 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.
Keywords: distributed systems; stochastic Petri nets; system specifications; trace logic; CSP; Fault tolerance; Formalism integration; Trace based specifications.