On the formal verification of systems of synchronous software components

Abstract

Large asynchronous systems composed from synchronous components (so called GALS-globally asynchronous, locally synchronous-systems) pose a challenge to formal verification. We present an approach which abstracts components with contracts capturing the behavior by a mixture of temporal logic formulas and non-deterministic state machines. Formal verification of global system properties is then done transforming a network of contracts to model checking tools such as Promela/SPIN or UPPAAL. Synchronous components are implemented in Scade, and contract validation is done using the Scade Design Verifier for formal verification. We also discuss first experiences from an ongoing industrial case study applying our approach. © 2012 Springer-Verlag.