Using SMT engine to generate Symbolic Automata -Extended version - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2018

Using SMT engine to generate Symbolic Automata -Extended version

Utilisation d'un Moteur SMT pour générer des Automates Symboliques - Version étendue

(1) , (2) , (3) , (1)
1
2
3

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.
Les pNets ouverts sont utilisés pour modéliser le comportement des systèmes ouverts, synchrones ou asynchrones, exprimée dans divers calculs ou langages de programmation. Ils sont dotés d’une sémantique opérationnelle symbolique en termes d’«Automata Ouverts». Cela nous permet de vérifier les propriétés de ces systèmes d’une manière compositionnelle. Nous avons implémenté un algorithme calculant ces sémantiques, en construisant des prédicats exprimant les conditions de synchronisation entre les actions des composants du pNet. La vérification de tels prédicats nécessite un raisonnement symbolique sur les logiques de premier ordre, mais également sur des données spécifiques à l’application. Nous utilisons le moteur SMT Z3 pour vérifier la satisfiabilité des prédicats, et ne conserver dans l’automate ouvert que les transitions satisfiables. Nous illustrons notre approche par un exemple d’inspiration industrielle. Pour cela nous partons d’«architectures» de systèmes BIP, qui ont été utilisés dans le cadre d’un projet de l’Agence Spatiale Européenne pour spécifier le logiciel de contrôle d’un nanosatellite au Centre d’ingénierie spatiale de l’EPFL. Nous utilisons les pNets pour encoder une architecture BIP étendu avec des données explicites, et calculer sa sémantique en termes d’automates ouverts. Cet automate peut être utilisé pour prouver des propriétés comportementales; nous donnons 2 exemples, une propriete de sureté et une de vivacité.
Fichier principal
Vignette du fichier
RR-9177.pdf (1.6 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01823507 , version 1 (26-06-2018)

Identifiers

  • HAL Id : hal-01823507 , version 1

Cite

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⟩
329 View
330 Download

Share

Gmail Facebook Twitter LinkedIn More