SMT-Based Generation of Symbolic Automata
Xudong Qin, Simon Bliudze, Eric Madelaine, Zechen Hou, Yuxin Deng, Min Zhang
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.