Invited talks - NII
Intervenant(s) : Dr. Fuyuki ICHIKAWA & Dr. Kenji TEI (NII, University of Tokyo)
- Fuyuki Ishikawa : Engineering Abstraction (or Refinement): towards Flexibility in Correct-by-Construction System Models
Software systems play an increasingly critical role in the society, as well as in the real world, as being further investigated in the emerging smart systems. The demand for dependability is very strong in such systems, while the difficulties in its assurance is increasing more than ever due to the unprecedented complexity of the systems and their environments. One of the key approaches to this challenge is abstraction (or refinement), specifically leveraging multiple steps of models with different levels of abstraction. Starting from the most abstract model, we can iteratively refine it and accumulate proofs on the correctness to finally reach the correct concrete model that we actually need. This "correctness-by-construction" approach has been investigated well to get a correct program code from a specification: e.g., by the B-Method well-known for its success in the Paris metro and the CDG airport shuttle. Such an approach is now moving to the system level given the increasing complexity even at the specification level: e.g., the Event-B method emerged after the success of the B-Method. However, the new approach faces with a large design space of abstraction: how we handle various elements in the system gradually in multi-step models by preserving the correctness. Our recent work provided a novel method to support engineering activities, such as refactoring, over the multi-step system models. This talk introduces the general background of the correctness-by-construction approaches and then our recent work, which tries to provide a complementary viewpoint for smart multi-agent systems.
- Kenji Tei : Assured and Correct Dynamic Update of Controllers
In many application domains, continuous operation is a desirable attribute for software-intensive systems. As the environment or system requirements change, so the system should change and adapt without stopping or unduly disturbing its operation. There is, therefore, a need for sound engineering techniques that can cope with dynamic change. In this keynote, I will address the problem of dynamic update of controllers in reactive systems when the specification (environment assumptions, requirements and interface) of the current system changes. I will present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur. Indeed, using controller synthesis I will show how to automatically build a controller that guarantees both progress towards update and safe update. Seven case studies have been implemented to validate the approach.
cedric.herpson (at) nulllip6.fr