Supervision : Béatrice BÉRARD

Co-supervision : DUTHEILLET Claude & THIERRY-MIEG Yann

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.

2010-2022 Publications

• 2022
  • Ph. Basset, S. Beeby, Ch. Bowen, Zh. Chew, Ah. Delbani, R. Dharmasena, Bh. Dudem, F. Fan, D. Galayko, H. Guo, J. Hao, Y. Hou, Ch. Hu, Q. Jing, Y. Jung, S. Karan, S. Kar‑Narayan, M. Kim, S.‑W. Kim, Y. Kuang, K. Lee, J. Li, Zh. Li, Y. Long, Sh. Priya, X. Pu, T. Ruan, S. Ravi P. Silva, H. Wang, K. Wang, X. Wang, Zh. Wang, W. Wu, W. Xu, H. Zhang, Y. Zhang, M. Zhu : “Roadmap on nanogenerators and piezotronics”, APL Materials, vol. 10 (10), pp. 109201, (AIP Publishing) (2022)
• 2014
  • Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Controllability for Discrete Event Systems Modeled in VeriJ”, International Journal of Critical Computer-Based Systems, vol. 5 (3/4), pp. 218-240, (Inderscience) (2014)
• 2013
  • Y. Zhang : “Semi-Automatic Controller Design in a Java-like Language”, thesis, defence 07/05/2013, supervision Bérard, Béatrice, co-supervision : Dutheillet, Claude & THIERRY-MIEG Yann (2013)
  • Y. Zhang, B. Bérard, L. Hillah, Y. Thierry‑Mieg : “Semi-Automatic Controller Design of Java-like Models”, Workshop on Formal Techniques for Java-like Programs, FTfJP 2013, Montpellier, France, pp. 3:1-3:7, (ACM) (2013)
• 2011
  • Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Modeling complex systems with VeriJ”, 5^th Verification and Evaluation of Computer and Communication System (VECOS), Tunis, Tunisia, pp. 34-45, (British Informatics Society Ltd) (2011)
  • Y. Zhang, B. Matuszewski, A. Histace, F. Precioso : “Statistical Shape Model of Legendre Moments with Active Contour Evolution for Shape Detection and Segmentation”, Computer Analysis of Images and Patterns, vol. 6854 (1), LNCS, Sevilla, Spain, pp. 51-58 (2011)
• 2010
  • Y. Zhang, B. Bérard, F. Kordon, Y. Thierry‑Mieg : “Automated Controllability and Synthesis with Hierarchical Set Decision Diagrams”, 11^th International Workshop on Discrete Event Systems (WODES'10), Berlin, Germany, pp. 281-286, (IFAC/Elsevier) (2010)
  • Y. Zhang : “Modeling Automated Highway Systems with VeriJ”, MOdelling and VErifying parallel Processes (MOVEP), Aachen, Germany, pp. 138-143 (2010)