Skip to Main content Skip to Navigation

Using SMT engine to generate Symbolic Automata -Extended version

Xudong Qin 1 Simon Bliudze 2 Eric Madelaine 3 Min Zhang 1
2 SPIRALS - Self-adaptation for distributed services and large software systems
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
3 KAIROS - Logical Time for Formal Embedded System Design
Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Open pNets are used to model the behaviour of open systems, both synchronous or asynchronous, expressed in various calculi or languages. They are endowed with a symbolic operational semantics in terms of so-called “Open Automata”. This allows us to check properties of such systems in a compositional manner. We implement an algorithm computing these semantics, building predicates expressing the synchronization conditions between the events of the pNet subsystems. Checking such predicates requires symbolic reasoning over first order logics, but also over application-specific data. We use the Z3 SMT engine to check satisfiability of the predicates, and prune the open automaton of its unsatisfiable transitions. As an industrial oriented use-case, we use so-called "architectures" for BIP systems, that have been used in the framework of an ESA project and 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, and compute its open automaton semantics. This automaton may be used to prove behavioural properties; we give 2 examples, a safety and a liveness property.
Complete list of metadatas

Cited literature [52 references]  Display  Hide  Download
Contributor : Eric Madelaine <>
Submitted on : Tuesday, June 26, 2018 - 10:07:43 AM
Last modification on : Friday, November 27, 2020 - 2:20:10 PM
Long-term archiving on: : Wednesday, September 26, 2018 - 9:07:40 PM


Files produced by the author(s)


  • HAL Id : hal-01823507, version 1


Xudong Qin, Simon Bliudze, Eric Madelaine, Min Zhang. Using SMT engine to generate Symbolic Automata -Extended version. [Research Report] RR-9177, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France; inria. 2018. ⟨hal-01823507⟩



Record views


Files downloads