Using SMT engine to generate Symbolic Automata

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 be-havioural properties; we give 2 examples, a safety and a liveness property.
Type de document :
Communication dans un congrès
18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018), Jul 2018, Oxford, United Kingdom. Electronic Communications of the EASST Open Access Journal, Jul 2018, Oxford, United Kingdom
Liste complète des métadonnées

https://hal.inria.fr/hal-01962971
Contributeur : Eric Madelaine <>
Soumis le : vendredi 21 décembre 2018 - 08:33:33
Dernière modification le : dimanche 23 décembre 2018 - 01:22:46

Fichier

2018-Avocs-paper 16.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01962971, version 1

Collections

Citation

Xudong Qin, Simon Bliudze, Eric Madelaine, Min Zhang. Using SMT engine to generate Symbolic Automata. 18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018), Jul 2018, Oxford, United Kingdom. Electronic Communications of the EASST Open Access Journal, Jul 2018, Oxford, United Kingdom. 〈hal-01962971〉

Partager

Métriques

Consultations de la notice

52

Téléchargements de fichiers

86