VHS Deliverable MG.1.2:
Management Report on Year 2)

Administration

1. The initiative to add the University of Uppsala as an official sub-contractor to Aalborg has been withdrawn.
2. The process of adding ETH-Zurich (M. Morari) as a partner to the project has been completed
3. Yassine Lakhnech, the site leader of Kiel, has been appointed as a professor at UJF-Verimag. Although he continues to supervise his students at Kiel which work for VHS, Willem-Paul de Roever has the the formal responsability for Kiel's part in the project.

Meetings and Visits.

Progress on Work-Packages

General

1. Timed models constitute a very useful level of abstraction for many of the case-studies and they can serve as a unifying framework for problems such as verification and scheduling, currently treated by different communities.
2. There is a serious gap between the complexity of real physical models of plants and the state-of-the-art in verification tools for continuous and hybrid systems.
3. There is a lot to be done in order to improve the software engineering of embedded systems in general and industrial computers in particular.

1. Comparison of different approaches to timing analysis (timed automata and Petri nets, mathematical programming, constraint solving, etc.) and development of methodologies, algorithms and data-structures to treat timing problems, inspired by the case-studies.
2. Contribution to the state-of-the-art in verification and controller synthesis for continuous and hybrid systems.
3. Research in methodologies and tools for design and verification of PLC programs.

MF: The work on this package which underlies the packages PA and TL made some significant contribution among which we mention here the compositional modeling of hydrodynamic networks, works on the semantics of PLC programming languages, connection between Simulink modules and synchronous languages, compositional modeling of discrete timed systems using Petri nets, the use of timed automata to express scheduling problems and the comparison between discrete and continuous time models.

PA: A lot of impressive work has been done on this work-package. For timed systems, new data-structures and algorithms for verification and for time-optimal synthesis of controllers have been devised. For hybrid systems new decidability and reducibility results have been proved and approximation algorithms for reachability and synthesis have been developed. It is fair to say that the results obtained by the partners represent the international state-of-the-art in the domain. Several efforts aimed on compositional modeling of hybrid systems for simulation. For PLC programs, first efforts in lightweight verification (verification of certain properties of the programs themselves which do not depend on the environment) have been made.

TL: A lot of work has been invested in the improvement of the two existing timing analysis tools Uppaal and Kronos. In addition to that some new prototype tools have been developed and tested. Among them one can find d/dt for verification and synthesis of hybrid systems with linear differential inclusions, PDG for probabilistic verification, YAHMST for hybrid systems simulation, VERDICT for translating logic-controlled plant to timed automata and a real-time animator for Uppaal. In the area of PLC programming, a prototype of a static analyzer for the language IL has been implemented.

CS1: Although this case-study terminated, the partners continued to improve their related results, partly due to the forthcoming special issue of the European Journal of Control and partly due to the challenging research opportunities it created.

CS3: The part of the case-study to be treated by the consortium has been extracted from Merck and presented to the partners.

CS4: The plant description and its operation schedules have been studied by the partners and a model of the juice processing plant in the form of a piecewise-linear hybrid system has been suggested. The coordination control problem is formulated and an approach to its solution was sketched.

CS5: Feasible schedules have been extracted for this steel plant as a first application of timed automata technology to such problems. Techniques for generating efficient schedules, based on constraint logic programming and on UPPAAL modelling, have been compared. Algorithms for recursively generating optimal schedules based on modular plant models have been developed.

CS6: The plant information has been extracted from Nylstar and presented to the consortium. A hybrid analysis problem has been defined and experiments with the new verification tools developed by the consortium have started.

CS7: The plant information, both as a scheduling and programming problem have been presented. This additional case study is interesting to the project, because it is accessible and contains aspects ultimatively requiring online scheduling and closed loop control. A second report analyses this problem in depth so that the project partners can work on it in the third year.

Conclusions

Appendix: Tables