Search

International audience; First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems. However,FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To addressthis, a possible track is to constrain specifications to a decidable fragment of FOLTL, but knownfragments are too restricted to be usable in practice. In this paper, we exhibit various fragments ofincreasing scope that provide a pertinent basis for abstract specification of infinite-state systems.We show that these fragments enjoy the Bounded Domain Property (any satisfiable FOLTL formulahas a model with a finite, bounded FO domain), which provides a basis for complete, automatedverification by reduction to LTL satisfiability. Finally, we present a simple case study illustratingthe applicability and limitations of our results.

International audience; In this paper, we present a specification in TLA+ of an AADL execution model. This formal specification is used forderiving a prototype verification tool for AADL the TOPCASED development environment.

International audience; In this paper, we study a mapping from AADL to Java-RTSJ. After reviewing the basic concepts of the AADL execution model, we present the basic notions of Java-RTSJ, we rely on, for our mapping. Then, we propose a mapping taking into account a given subset of AADL. A related works section reviews existing works and elaborates on some comparisons.

First-Order Linear Temporal Logic (FOLTL) is particularly convenient to specify distributed systems, in particular because of the unbounded aspect of their state space. We have recently exhibited novel decidable fragments of FOLTL which pave the way for tractable verification. However, these fragments are not expressive enough for realistic specifications. In this paper, we propose three transformations to translate a typical FOLTL specification into two of its decidable fragments. All three transformations are proved sound (the associated propositions are proved in Coq) and have a high degree of automation. To put these techniques into practice, we propose a specification language relying on FOLTL, as well as a prototype which performs the verification, relying on existing model checkers. This approach allows us to successfully verify safety and liveness properties for various specifications of distributed systems from the literature.

Cette étude concerne l’utilisation de la logique du premier ordre et la logique temporelle linéaire pour la spécification et la vérification des systèmes dynamiques ayant des structures riches. Elle concerne l’étude de la correction de fonctionnement du protocole de recherche distribuée Chord. L’objectif est d’une part d’améliorer la spécification et la vérification des systèmes dans le langage formel Electrum qui est une extension dynamique du langage formel Alloy basé sur la logique du premier ordre temporelle linéaire.Pour ce faire, nous avons développé une couche syntaxique au-dessus d’Electrum. L’objectif de cette couche est de faciliter la spécification du comportement dans Electrum, pour ce faire, nous avons défini une syntaxe permettant de générer automatiquement une partie de la spécification du comportement. Par ailleurs cette couche permet également de réduire les erreurs de spécification en déchargeant les utilisateurs de la spécification de certaines tâches comportementales ardues et sujettes aux erreurs.D’autre part, l’objectif est d’analyser formellement la correction de la propriété fondamentale de vivacité du protocole Chord. Pour ce faire nous avons spécifié et vérifié le protocole Chord avec l’extension d’Electrum que nous avons développée, puis nous avons prouvé sa correction et montré les avantages de notre méthode d’analyse. This study deals with the use of first-order logic and linear temporal logic for specificationand verification of dynamics system with rich structural properties. It also concerns the studyof the operating safety of the distributed lookup protocol Chord. The aim is on the one hand toimprove the specification and verification of systems whith the formal language Electrum a dynamicextension of the formal language Alloy based on first-order linear temporal logic. To do this, we havedeveloped an action layer above Electrum. The purpose of this layer is to make the specification ofthe behavior in Electrum easier, to do this, we have defined a syntax to automatically generate partof the specification of the behavior. Moreover, this layer also makes it possible to reduce specificationerrors by getting rid the users of the specification of certain laborious and error-prone behavioraltasks. On the other hand, the aim is the formal analyzing of the fundamental liveness property ofthe Chord protocol. To do this, we specified and verified the Chord protocol with the extension ofElectrum that we have developed, then we proved its correctness and showed the advantages of ouranalysis method.

International audience; Chord is a protocol that provides a scalable distributed hash table over an underlying peer-to-peer network. Since it combines data structures, asynchronous communications, concurrency, and fault tolerance, it features rich structural and temporal properties that make it an interesting target for formal specification and verification. Previous work has mainly focused on automatic proofs of safety properties or manual proofs of the full correctness of the protocol (a liveness property). In this paper, we report on analyzing automatically the correctness of Chord with the Electrum language (developed in former work) on small instance of networks. In particular, we were able to find various corner cases in previous work and showed that the protocol was not correct as described there. We fixed all these issues and provided a version of protocol for which we were not able to find any counterexample using our method.

National audience; Cet article propose des structures d'interprétation pour le langage Khi, un langage de modélisation pour l'ingénierie des exigences, qui formalise notamment les notions d'agents, de buts et d'opérations. Deux notions d'agents s'y confrontent : les acteurs, qui sont les agents présents et décrits par leurs capacités d'action sur le système, et les rôles, qui décrivent le comportement attendu des agents pour la réalisation des buts. Les rôles sont ensuite assignés à des acteurs ou des coalitions d'acteurs. La capacité effective des coalitions à jouer les rôles qui leur sont assignés fournit donc un critère de correction du modèle, on appelle le problème relatif problème de l'assignation. Khi a une sémantique formelle dans un fragment de la logique temporelle multi-agents ATL*, nommé ATL_Khi. Nous décrivons les modèles sémantiques qui permettent d'interpréter ATL_Khi et de réduire le problème de l'assignation à un problème de model-checking.

National audience; La vérification de propriétés de sûreté de fonctionnement (SdF) pour les systèmes critiques est un problème primordial. Les solutions existantes imposent généralement une connaissance de l'architecture complète du système. Dans cet article, nous proposons une approche permettant de vérifier efficacement la sûreté de fonctionnement d'architectures abstraites qui sont, éventuellement, partiellement décrites. Nous présentons une méthodologie qui s'appuie sur une vue SdF et une vue architecturale du système. Des propriétés de SdF sont vérifiées au niveau de la vue idoine, et sont postérieurement validées sur l'architecture. Cette approche permet donc de décomposer des vérifications complexes de SdF sur des architectures en deux vérifications plus simples, sur deux vues différentes. Les techniques présentées sont appliquées au système hydraulique d'un avion, utilisé comme cas d'étude.

This document presents the work realized for my final master project. I made this internship at the CNES. I was welcomed in the On-Board Software Team of the Ground & On Board System department by my tutor, David Chemouil. This intership lasted 6 months. My internship took place in the context of the CNES participation to the Topcased Project. The idea was to realize a framework for model transformation. From the point of view of the metamodels the models are instance of. Apart from the realization of this framework, the idea was also to evaluate the Scala language, using it to realize the application. First, I will present the context of my internship, the subject itself and the Scala language. Then I will analyze the problem and the different solutions I could bring for each part of the project. In a third part I will study in more details the chosen solution and the realized application. Finally, I will give conclusions about the Scala language and the work done.

International audience; Dans cet article, nous présentons un cadre de modélisation formelle pour l'ingénierie du besoin qui prenne simultanément en compte les buts comportementaux et les agents. Pour ce faire, nous introduisons un langage noyau, appelé KHI, ainsi que sa sémantique dans une logique de straté-gies appelée USL. Dans KHI, les agents sont décrits par leurs capacités et les buts sont définis par des formules de logique temporelle linéaire. Une « assignation » associe alors chacun des buts à un ensemble (une coalition) d'agents, qui sont responsables de sa satisfaction. Nous présentons et dis-cutons ensuite différents critères de correction pour cette relation d'assignation. Ceux-ci permettent d'évaluer la « pertinence » d'une assignation de buts à des coalitions. Ils différent selon les interactions qu'ils permettent entre les coalitions d'agents. Nous proposons alors une procédure décidable de vérification pour la satisfaction des critères de correction pour l'assignation. Elle consiste à réduire la satisfaction des critères à des instances du problème de model-checking pour des formules d'USL dans une structure dérivée des capacités des agents. 1 Contexte Si, en toute rigueur, la discipline de la modélisation du besoin ne se restreint pas à elles seules [17, 14], les approches dites par buts [18] ou par agents [2, 9] ont le vent en poupe dans la communauté idoine (cf. les citations précédentes mais aussi [12, 15]). En KAOS [18], la question première est de déterminer les besoins dont il faut tenir compte pour rendre compte d'un système au sein d'un environnement, le tout formant un système global à mettre au point. Celui-ci doit répondre à des buts et est constitué d'agents (entités actives). Un but est défini comme un énoncé prescriptif sous la responsabilité d'agents du système global. Les buts peuvent être de toutes sortes (on retrouve les traditionnelles taxonomies autour des buts non-fonctionnels [11]). Mais on distingue en particulier les buts comportementaux qui caractérisent des traces et peuvent donc faire l'objet d'une formalisation dans une logique temporelle telle que LTL. Bien que partageant superficiellement de nombreuses notions avec KAOS, TROPOS se concentre avant tout sur la notion d'acteur, défini comme un agent intentionnel. Un tel agent est muni de buts qu'il sou-haite voir remplis mais dont la satisfaction, partielle comme complète, n'est pas nécessairement de sa responsabilité. Celle-ci peut être déléguée à d'autres acteurs. TROPOS [2] pousse ainsi à l'explicitation des liens de dépendance et de collaboration entre acteurs. Ceci s'explique en particulier par le fait que les systèmes visés par la méthode sont susceptibles de comprendre des acteurs « humains » ou institu-tionnels. TROPOS a aussi fait l'objet d'une proposition formelle visant à étudier dans quelle mesure des acteurs peuvent contribuer à satisfaire des buts pour d'autres acteurs. L'approche en question [9, 10] introduit à cette fin les notions, dites « sociales », de rôle, d'engagement (commitment) et de protocole. Le rôle représente le comportement attendu des acteurs. Une assignation de rôles à des acteurs est alors évaluée au moyen d'un critère de correction. Celui-ci revient essentiellement à vérifier que les capacités d'un acteur entraînent les conséquents des engagements où le rôle assigné apparaît comme débiteur.