LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Tin tức » Nghiên cứu sinh
http://perso.celest.fr/yan

ZHANG Yan

Tiến sĩ
Nhóm nghiên cứu : MoVe
Ngày đi : 15-10-2013
http://perso.celest.fr/yan
Ban lãnh đạo nghiên cứu : Béatrice BÉRARD
Đồng hướng dẫn : 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.
Bảo vệ luận án : 05-07-2013 - 14h - Site Jussieu - Salle Jean-Louis Laurière - 25-26/101
Hội đồng giám khảo :
Stephan Merz - INRIA Nancy & LORIA [Rapporteur]
Franck Pommereau - IBISC, Université d'Évry [Rapporteur]
Stefan Schwoon - LSV, ENS Cachan
Fabrice Kordon - LIP6, UPMC
Béatrice Bérard - LIP6, UPMC
Yann Thierry-Mieg - LIP6, UPMC

Bài báo khoa học 2010-2014

 Mentions légales
Sơ đồ site |