Programme 2014

Le diagnostic consiste à détecter l’occurrence de fautes dans un système à événements discrets partiellement observable. Un tel système peut être diagnostiquable ou pas. Aussi le diagnostic actif vise à le contrôler afin de le rendre diagnostiquable. Aprés avoir formalisé le problème, nous décrirons d’abord des procédures de décision de complexité optimale et de synthèse de diagnostiqueur de taille optimale basées sur des techniques d’automates et de jeux. Puis nous étudierons ces mêmes problèmes dans un cadre probabiliste montrant que selon les exigences requises, le problème se situe d’un côté ou de l’autre de la frontière de la décidabilité. Lorsque les problèmes sont décidables, nous décrirons aussi des procédures optimales.

Ce travail repose sur des collaborations avec Nathalie Bertrand, Eric Fabre, Stefan Haar, Loïc Hélouët, Tarek Melliti et Stefan Schwoon.

Notre travail s’inscrit dans le contexte de l’étude conjointe de la correction et de la performance d’applications distribuées, sans nécessiter de réécriture entre les modèles, algorithmes et implémentations réelles. Pour cela, nous nous appuyons sur l’environnement SimGrid, qui permet initialement de simuler des systèmes distribués à large échelle tels que les grilles, le Cloud, les applications HPC ou bien encore les systèmes P2P. Au sein de cet outil de simulation, nous proposons l’outil de vérification SimGridMC qui permet de vérifier dynamiquement (en exécutant et en vérifiant l’application réelle) les applications étudiées à travers le simulateur.

L’informatique en nuage (ou  »Cloud Computing ») permet aux utilisateurs de louer à la demande des ressources numériques (processeur, mémoire, stockage, réseau, pile logicielle, application en ligne, etc.) et de les administrer à distance. L’Open Cloud Computing Interface (OCCI) est un ensemble de spécifications de l’Open Grid Forum (OGF) définissant une interface ouverte, simple, extensible et auto-descriptive pour la gestion de ces ressources en nuage (http://occi-wg.org/). Cependant ces spécifications écrites en anglais restent informelles et donc potentiellement inconsistantes, ambigües et incomplètes. Notre objectif est de proposer une spécification formelle d’OCCI qui soit mathématiquement consistante, non ambigüe et complète. Nous avons choisi Alloy, un langage de spécification léger basé sur la logique relationnelle du premier ordre pour écrire notre spécification formelle d’OCCI. L’intérêt d’Alloy est la simplicité de ce langage et l’utilisation facile de son analyseur (http://alloy.mit.edu), qui agit essentiellement comme un vérificateur de modèles et un générateur de contre-exemples. Cela permet de rapides itérations entre modélisation et analyse lors de l’écriture et la mise au point d’une spécification. Cet exposé présentera une spécification en Alloy de la sémantique statique et d’une partie de la sémantique dynamique du coeur d’OCCI. Ce modèle formel est ensuite outillé dans l’environnement Eclipse par une chaîne d’outils dirigée par le modèle OCCI. Cette chaîne propose un langage dédié de modélisation OCCI. La syntaxe abstraite de ce langage est capturée via un méta-modèle Ecore, la syntaxe concrète est un schéma XMI (XML Modeling Interchange), la sémantique statique est exprimée par des contraintes OCL (Object Constraint Language) et la sémantique dynamique est programmée en Kermeta (http://www.kermeta.org). Enfin, notre chaîne offre un modeleur graphique pour modéliser des extensions OCCI.

Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. The overwhelming majority of works so far considers handmade algorithm and correctness proofs. This paper is the first to propose a formal framework to automatically design distributed algorithms that are dedicated to autonomous mobile robots evolving in a discrete space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. Our contribution is threefold. First, we propose an encoding of the gathering problem as a reachability game. Then, we automatically generate an optimal distributed algorithm for three robots evolving on a fixed size uniform ring. Finally, we prove by induction that the generated algorithm is also correct for any ring size except when an impossibility result holds (that is, when the number of robots divides the ring rize).

Le langage TLA+ est destiné à la spécification de systèmes et particulièrement d’algorithmes répartis. Il est fondé sur la théorie des ensembles pour modéliser les aspects statiques et sur la logique temporelle pour décrire les exécutions d’un système. Les principaux outils de vérification associés à TLA+ sont le model checker TLC et la plate-forme interactive de preuves TLAPS. Cette dernière repose sur un langage hiérarchique de preuve et intègre différents outils de preuve automatisés. L’exposé donnera un aperçu des choix qui ont été faits dans la conception du langage de preuve et de TLAPS, des défis concernant l’intégration d’outils externes, de quelques exemples d’application pour la vérification d’algorithmes et présentera des travaux en cours et à venir.

Travail commun avec la participation de Kaustuv Chaudhuri, Denis Cousineau, Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Dan Ricketts et Hernán Vanzetto.

In a previous work, we showed that a kind of ω-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties.

In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Buchi Automata.

Verifying software systems automatically from their source code rather than manually modelling them in a dedicated language gives more confidence in establishing their properties. Here we propose a formal specification and verification approach for concurrent C programs directly based on the semantic of C. We define a set of translation rules and implement it in a tool (C2TLA+) that automatically translates C code into a TLA+ specification. The TLC model checker can use this specification to generate a model, allowing to check the absence of runtime errors and dead code in the C program in a given configuration. In addition, we present how to make the translated specification interact with manually written ones to: check the C code against safety or liveness properties; provide concurrency primitives or model hardware that cannot be expressed in C; and use abstract versions of translated C functions to address the state-explosion problem. We also show that we can verify refinement between this abstract version and the TLA+ specification obtained by translation. All these verifications have been conducted on an industrial case study, which is a part of the microkernel of the PharOS real-time system.

This paper defines a formal framework for the modular and hierarchical model-checking of μ-calculus against modular transitions systems. Given a formula φ, a module can be analysed alone, in such a way that the truth value of φ may be decided without the need to analyse other modules. If no conclusion can be drawn locally, the analysis provides information allowing to reduce the module to a smaller one that is equivalent with respect to the truth value of φ. This way, modules can be incrementally analysed, reduced and composed to other reduced modules until a conclusion is reached. On the one hand, modular analysis allows to avoid modules compositions and thus the corresponding combinatorial explosion; on the other hand, hierarchical analysis allows to reduce the modules that must be composed, which limits combi- natorial explosion. Moreover, by proposing three complementary formula-dependent reductions, we expect better reductions than general approaches like bisimulation or tau ∗ reductions. The current paper is focused on defining the theoretical tools for this approach; finding interesting strategies to apply them efficiently is left to future work.

Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.

Well-structured transition systems (WSTS) as a general class of infinite-state systems have spawned decidability results for important problems such as termination, boundedness, control-state maintainability and coverability. WSTS consist of a (usually infinite) well ordered set of states, together with a monotone transition relation. WSTS have found multiple uses: in settling the decidability status of reachability and coverability for graph transformation systems, in the forward analysis of depth-bounded processes, in the verification of parameterized protocols and the verification of multi-threaded asynchronous software. Most decidability results concerning WSTS apply to the finitely branching variant. Yet some models (inserting automata, ω-Petri nets, …) are naturally infinitely branching. Here we develop tools to handle infinitely branching WSTS by exploiting the crucial property that in the (ideal) completion of a well-quasi-ordered set, downward-closed sets are finite unions of ideals. Then, using these tools, we derive decidability results and we delineate the undecidability frontier in the case of the termination, the control-state maintainability and the coverability problems. A new forward algorithm for deciding coverability is obtained and boundedness is also shown decidable.

I will show that for any fixed i>0, the Sigma-(i+1)-fragment of Presburger arithmetic, i.e., its restriction to i+1 quantifier alternations beginning with an existential quantifier, is complete for the i-th level of the weak EXP hierarchy. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer & Rabin in 1974. Moreover, I will discuss bounds on sets of naturals definable in the existential fragment of Presburger arithmetic: given an existential formula p(x), I will show that the set of solutions is an ultimately periodic set whose period can be doubly-exponentially bounded from below and above. An online version of the paper is available from: http://arxiv-web3.library.cornell.edu/abs/1401.5266

In this talk, we investigate a sub-problem of the stratifiability of semilinear sets – namely the semilinear sets that are given as finite systems of linear inequalities – and show that stratifiability is coNP-complete in this case. We then apply this result to flat counter systems.

This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Even though it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to ZVASS while retaining NP-completness of both coverability and reachability.

Given a system modeled by a rational relation R, a channel is a pair (E,D) of rational relations that respectively encode and decode binary messages, and such that the composition E R D is the identity relation. This means that the message between E and D has been perfectly transmitted through R. Investigating the links between channels and the growth of rational sets of words, we give new characterizations for relations with channels. In the particular case where the relation is given as a union of functions, we obtain as a consequence the decidability of the synthesis problem with a linear complexity.

We use quantitative games with both energy and mean-payoff to model a network of wireless sensors where some nodes might be corrupted. (See file for extended abstract.)

Many systems have been proposed for electronic voting during the past few years and some of them are very complex, involving e.g. a lot of cryptographic primitives to ensure security and usability for the voters. A secure voting system should ensure properties such as privacy, individual and universal verifiability, correctness, etc. Verifying that these complex protocols satisfy such properties can be tedious and many of the existing approaches often involve a lot of handwork leading to error-prone proofs. Automatic tools dedicated to security protocols may sometimes simplify the work but they have some limits and e-voting protocols are, for most of them, a few steps away from their scope. One major difficulty for automatic tools is that most electronic voting systems involve associative and commutative properties. Even though such properties are quite simple, they often lead to issues such as non termination. On the other hand, this kind of properties is handled very well by SMT solvers, used by type-systems. From this idea, we propose a type system to prove privacy-like properties. More precisely, based on a recent work from C. Fournet and al. on rF*, we develop a type system that can be applied to verify some e-voting protocols like Helios and a Norwegian E-voting protocol. This involves the development of a cryptographic library that could also be used to model and verify other system, automatically.