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
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Résumé : 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é.
Type de document :
Rapport
[Research Report] RR-9177, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France; inria. 2018
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01823507
Contributeur : Eric Madelaine <>
Soumis le : mardi 26 juin 2018 - 10:07:43
Dernière modification le : mardi 17 juillet 2018 - 11:37:12

Fichier

RR-9177.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01823507, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

201

Téléchargements de fichiers

103