Semi-Automatic Controller Design in a Java-like Language
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.
Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Modeling complex systems with VeriJ”, 5th Verification and Evaluation of Computer and Communication System (VECOS), Tunis, Tunisia, pp. 34-45, (British Informatics Society Ltd) (2011)