SMT-based generation of symbolic automata

摘要

Open pNets are formal models that can express the behaviour of open systems, either synchronous, asynchronous, or heterogeneous. They are endowed with a symbolic operational semantics in terms of open automata, which allows us to check properties of such systems in a compositional manner. We present an algorithm computing these semantics, building predicates expressing the synchronisation conditions between the events of pNet sub-systems. Checking such predicates requires symbolic reasoning about first order logics and application-specific data. We use the Z3 SMT engine to check satisfiability of the predicates. We also propose and implement an optimised algorithm that performs part of the pruning on the fly, and show its correctness with respect to the original one. We illustrate the approach using two use-cases: the first one is a classical process-algebra operator for which we provide several encodings, and prove some basic properties. The second one is industry-oriented and based on the so-called "BIP architectures", which have been used to specify the control software of a nanosatellite at the EPFL Space Engineering Center. We use pNets to encode a BIP architecture extended with explicit data, compute its semantics and discuss its properties, and then show how our algorithms scale up, using a composition of two such architectures.