The symposium consists of the following lectures by eminent scientists (see also the schedule below):
+++ JOSEPH SIFAKIS - RIGOROUS SYSTEM DESIGN +++
Professor at École Polytechnique Federale de Lausanne EPFL, Director of the RiSD Laboratory, Director of the Center of Integrative Research, Honorary CNRS Research Director, Founder of VERIMAG Laboratory, Turing Award 2007.
(
http://www-verimag.imag.fr/~sifakis/)
ABSTRACT: We advocate rigorous system design as a coherent and accountable model-based process leading from requirements to correct implementations. We present the state of the art in system design, discuss its current limitations, and identify possible avenues for overcoming them.
Rigorous system design is 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.
We conclude with a discussion advocating a system-centric vision for computing, identifying possible links with other disciplines, and emphasizing centrality of system design.
+++ UGO MONTANARI - DECLARATIVE VS PROCEDURAL KNOWLEDGE: THE CASE OF SOFT CONSTRAINT SATISFACTION PROBLEMS, WITH AN APPLICATION TO AN E-MOBILITY OPTIMIZATION PROBLEM +++
Professor at the Dipartimento di Informatica of Università di Pisa and Coordinator of the Research Group on Concurrent Models of Computation.
(
http://www.di.unipi.it/~ugo)
ABSTRACT: Large optimization problems tend to be overly complex to solve and often a globally optimal solution may be impossible to find. For this reason specific strategies are needed to solve them. We propose an approach for the coordination of declarative knowledge - that is the exact specification of the complete optimization problem - and of procedural knowledge - that is the specific knowledge about subproblems and their, possibly approximated, solution strategies. We consider Soft Constraint Satisfaction Problems (SCSPs) and we introduce a formalism, similar to a process calculus, for their specification. Cost functions are associated to terms and form a model of such specification, where operators are interpreted as optimization steps. We compare our approach with Courcelle’s results for efficient monadic second-order evaluations on tree composable graphs.
We apply our proposal to a problem studied in the e-mobility case study of the ASCENS European FET project, for which we provide a model in terms of cost functions. The procedural part concerns heuristic choices about which dynamic programming strategy should be employed and how different ad-hoc approximation heuristics could be applied.
(joint work with Nicklas Hoch, Valentina Monreale and Matteo Sammartino)
+++ KRZYSZTOF R. APT - EPISTEMIC GOSSIP PROTOCOLS +++
CWI Fellow at CWI, working in the group Networks and Optimization.
(
http://homepages.cwi.nl/~apt/)
ABSTRACT: Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other secrets. We consider distributed gossip protocols, building upon the recent work of Attamah, Van Ditmarsch, Grossi and Van der Hoek. These protocols are expressed by means of epistemic logic (for instance by statements such as `if I do not know whether agent i knows my secret I communicate it to him').
We provide an operational semantics of such protocols and set up an appropriate framework to argue about their correctness. Then we analyze specific protocols both for a ring and for complete graphs.
This is a joint work with Wiebe van der Hoek and Davide Grossi.
+++ SUNG-SHIK JONGMANS - FARHAD'S PRIDE +++
PhD student at CWI, supervised by Farhad Arbab.
ABSTRACT: Thirty minutes about something that Farhad is proud on.
