Using SMT engine to generate Symbolic Automata -Extended version

Description

Open pNets are used to model the behaviour of open systems, both synchronousor asynchronous, expressed in various calculi or languages. They are endowed with a symbolicoperational semantics in terms of so-called "Open Automata". This allows us to check properties ofsuch 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 alsoover 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 anESA project and to specify the control software of a nanosatellite at the EPFL Space EngineeringCenter. We use pNets to encode a BIP architecture extended with explicit data, and compute itsopen automaton semantics. This automaton may be used to prove behavioural properties; we give2 examples, a safety and a liveness property.

Abstract (French)

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 sontdotés d'une sémantique opérationnelle symbolique en termes d'«Automata Ouverts». Cela nouspermet de vérifier les propriétés de ces systèmes d'une manière compositionnelle. Nous avonsimplémenté un algorithme calculant ces sémantiques, en construisant des prédicats exprimant lesconditions de synchronisation entre les actions des composants du pNet. La vérification de telsprédicats nécessite un raisonnement symbolique sur les logiques de premier ordre, mais égalementsur des données spécifiques à l'application. Nous utilisons le moteur SMT Z3 pour vérifier lasatisfiabilité 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 nouspartons d'«architectures» de systèmes BIP, qui ont été utilisés dans le cadre d'un projet del'Agence Spatiale Européenne pour spécifier le logiciel de contrôle d'un nanosatellite au Centred'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 2exemples, une propriete de sureté et une de vivacité.

Additional details