International Conference on Service Oriented Computing

Keynote 1 - Rigorous System Design

Speaker: Joseph Sifakis, RiSD Laboratory EPFL
Date: November 4, 2014


We advocate rigorous system design as a coherent and accountable model-based process leading from requirements to implementations. We present the state of the art in system design, discuss its current limitations, and identify possible avenues for overcoming them.

A rigorous system design flow is defined as a formal accountable and iterative process composed of steps, and based on four principles: (1) separation of concerns; (2) component-based construction; (3) semantic coherency; and (4) correctness-by-construction. We show that the combined application of these principles allows the definition of rigorous design flows clearly identifying where human intervention and ingenuity are needed to resolve design choices, as well as activities that can be supported by tools to automate tedious and error-prone tasks. An implementable system model is progressively derived by source-to-source automated transformations in a single host component-based language rooted in well-defined semantics. Using a single modeling language throughout the design flow enforces semantic coherency. Correct-by-construction techniques allow well-known limitations of a posteriori verification to be overcome and ensure accountability. It is possible to explain, at each design step, which among the requirements are satisfied and which may not be satisfied.

The presented view has been amply implemented in the BIP (Behavior, Interaction, Priority) component framework and substantiated by numerous experimental results showing both its relevance and feasibility. We show in particular, how distributed implementations can be generated from BIP models with multiparty interactions by application of correct-by-construction transformations.


Bio from Wikipedia
Mentions légales