Conception semi-automatique de contrôleurs avec VeriJ
Institution:
Paris 6Disciplines:
Directors:
Abstract EN:
Lorsqu'un système ouvert ne respecte pas une spécification, notamment concernant la sûreté de fonctionnement, une solution possible consiste à restreindre le système avec un contrôleur pour atteindre l'objectif, lorsque cela est possible. Deux approches sont utilisées pour construire un tel contrôleur. La première, qui consiste en un processus manuel où un expert définit un contrôleur, est sujette à erreurs. La seconde repose sur des méthodes formelles et synthétise automatiquement un contrôleur correct, s'il en existe un. Cependant, les outils de synthèse existants résolvent principalement le problème pour des systèmes décrits dans des formalismes de bas niveau, qui présentent un investissement conséquent en apprentissage pour les ingénieurs du logiciel. De plus, la synthèse automatique ne passe pas bien à l'échelle pour des grands systèmes. Enfin, le contrôleur généré automatiquement est généralement très grand, ce qui rend son interprétation difficile, et il ne peut pas être adapté aisément lorsque des paramètres du système sont modifiés. Afin de favoriser l'adoption de la théorie du contrôle dans les processus industriels, nous définissons un nouveau langage de programmation appelé VeriJ, sous la forme d'un sous-ensemble de Java auquel sont ajoutées des constructions supplémentaires dédiées à la supervision. Nous fournissons avec VeriJ un outil, basé sur la transformation de modèles, qui prend en entrée un programme VeriJ et produit un système de transitions étiqueté (LTS), représentant la sémantique du programme. Un moteur pour ce système de transitions est intégré dans l'outil afin de permettre le test de contrôlabilité et la synthèse de contrôleur pour des programmes VeriJ. Ceci réduit donc le fossé entre les programmes de type Java et la synthèse formelle de contrôleurs. Nous proposons de combiner la synthèse automatique avec une conception centrée sur l'utilisateur en définissant une approche itérative, incrémentale et semi-automatique pour la conception de contrôleur. Dans ce processus, les utilisateurs peuvent modéliser, simuler et exécuter un système (incluant éventuellement un contrôle partiel), dans un environnement de développement Java. L'outil de synthèse fournit aux utilisateurs des diagnostiques sur le programme courant et peut générer des contrôleurs en VeriJ, lorsque cela est possible. Cette approche évite partiellement les problèmes de passage à l'échelle et de lisibilité des contrôleurs générés. L'illustration d'un tel processus sur un exemple significatif, provenant des systèmes de transport automatisés, montre qu'il est possible de combiner: i) les bénéfices résultant des environnements de développement évolués pour Java, avec ii) des performances comparables à celles des outils existants.
Abstract FR:
When an open system does not satisfy a specification, for instance safety requirements, a solution consists in restricting the system with a controller to enforce the specification. There are two approaches to build such a controller. The first one, consisting in a manual process where an expert produces a controller, is error-prone. The second one, relying on formal methods, is to automatically synthesize a correct controller if it exists. However, existing synthesis tools mainly solve the problem for systems described in low-level formalisms, which presents a costly learning investment for software engineers. Another problem is that automatic synthesis cannot scale up well on large systems. Besides, the automatically generated controller is usually very large, difficult to understand, and cannot be adapted when system parameters must be changed. To help industrial adoption of control theory, we define a programming language called VeriJ, a subset of Java with additional constructs dedicated to supervisory control. We provide a tool, based on model transformation, to automatically express an input VeriJ program as a labeled transition system (LTS). An engine for this LTS is then integrated into the tool to proceed with controller synthesis of the VeriJ program, which bridges the gap between Java-like programs and automatic controller synthesis. We propose to combine the fully automatic synthesis with a user-centric design by defining an iterative, incremental and semi-automatic approach for controller design. In this process, users can model, simulate, and execute a system that may include a controller in Java development environments. The synthesis tool will provide users diagnosis of the input and generate controllers in VeriJ if possible. This approach partly avoids the issues of scalability and readability of generated controllers. The illustration of such a process on a significant example taken from automated transport systems, shows that it is possible to combine: i) the benefits resulting from using mature Java development environments, with ii) performances comparable to those of existing tools. To mitigate the combinatorial explosion problem, we also integrate a control module to an efficient symbolic engine (ITS/SDD) based on SDD (Set decision Diagram), a variant of decision diagrams. With this module, we experiment controllability checking for (time) Petri net models. One of our important perspectives is to integrate this approach within the VeriJ framework.