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

Abstract

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é.