Specification and Verification of Critical Systems (SpeVeCriS)

 
The France Excellence 2018 Summer School "Specification and Verification of Critical Systems (SpeVeCriS)" will take place from July 2nd to 20th 2018 in Université Paris-Est Créteil

Short description of the school :

Software development based on formal modeling, specification and verification is a hot topic in computer science, applied to the development of critical systems (avionics, railway systems, nuclear plant control, space exploration), domains where methodologies based on testing and simulation cannot guarantee the absence of design errors or implementation errors. Formal methods require solid theoretical bases in automata theory, computability and complexity theory, logics for computer systems and algorithmics, and good mastering of computer systems modeling.  

Our summer school, based on the topics of the MeFoSyLoMa seminar, http://www.mefosyloma.fr/, aims at attracting top students in the last year of their MSc degree and will provide the theoretical and practical skills that will allow them to start a PhD in the domain of formal methods in one of the member labs of the seminar.

 

Transportation, welcome and departure at Charles-de-Gaulle airport.

The participants will be welcomed by UPEC students on their arrival at Roissy Charles-de-Gaulle airport. These students will accompany the participants during their stay in Paris. A bus service for the arrival and departure will be provided. The participants will receive a monthly pass on their arrival for the public transportation in the whole Île-de-France region.

The accommodation site is located 40 mins away from the university by public transportation.

Accomodation and meals.

The participants will be lodged at the FIAP Jean Monnet, http://www.fiap.paris/, which is an International Center for short-term visits in the 14ème arrondissement of Paris. Breakfast and dinner will be provided at the Center.

During the weekdays, a catering service will provide all participants with lunch boxes. Coffee breaks are also catered for during these days.

During weekends the catering service will also provide lunch boxes.

 

 

 

Short description of the research labs involved in the organization :

The MeFoSyLoMa seminar (Méthodes Formelles pour les Systèmes Logiques et Matériels) is organized jointly by teams from eight research labs from the Île-de-France region in the domain of the specification and verification of computer systems. Its objective is to allow the confrontation of various formal or semi-formal approaches in software design, circuit design, distributed systems, real-time systems or information systems. The originality of this seminar comes from its deliberate choice in associating theoretical approaches with methods, tools and examples and case studies issued from industry. This favors exchanges between different actors of our research domain and gives the opportunity for participants from industry to follow the evolution of the research within the domain of specification and verification.

The member labs of MeFoSyLoMa and their teams are :

·         CEDRIC (Cnam). Created in 1988, the CEDRIC lab (Centre d’Études et Recheche en Informatique et Communications) regroups seven teams developing research in computer science, applied maths and electronics at the Conservatoire National d’Arts et Métiers. The SYS team of Cedric works in the specification, synthesis, verification and evaluation of critical applications in security and safety.

·         IBISC (Univ. Evry). The IBISC research lab (Informatique, Biologie Intégrative et Systèmes Complexes) regroups four research teams working in fundamental and applied aspects of information science et technology, aiming at developing new methods, formalisms and applications towards a better comprehension of complex systems, be they alive or artificial. The COSMO team aims at studying fundamental properties of computer and biological systems and, more generally, the behavior of dynamical, reactive, decentralized and open systems.

·         LACL (Univ. Paris-Est Créteil). Created in 1997, LACL (Laboratoire d’Algorithmique, Complexité et Logique) is the research lab in computer science of the Université Paris-Est Créteil. The members of the SVS team (Spécification et Vérification des Systèmes) focus their research on theoretical and practical aspects of system modeling, specification, verification and synthesis of various aspects like concurrency, hard and soft real-time performance, mobile agents, information system design and security, parallel and cloud computing.

·         LIP6 (UPMC). The LIP6 (Laboratoire d’Informatique Paris 6) is the research lab of the Université Pierre et Marie Curie (formerly Univ. Paris 6) has three federating axes : (1) the safety, security and reliability, (2) data science, intelligence and optimization and (3) communicating objects. The research team MoVe (Modélisation et Vérification) centers its research interests in the modeling and analysis of distributed and dynamic complex systems, with special emphasis on optimized techniques for model-checking, integrating formal analysis in software development and the synthesis of new programming languages and models for improving the verifiability of distributed systems..

·         LIPN (Univ. Paris Nord). The research at LIPN (Laboratoire d’Informatique de Paris Nord) is centered in domains like Combinatorics, Algorithmics, Logic, Software Science, Natural Languages and Machine Learning. The LCR team works in the specification and verification of systems with applicationg into dynamic distributed systems and databases and complemented by temporal reasoning and representation.

·         LRDE (Epita). The LRDE lab of the EPITA Graduate School of Computer Science centers its research in two main areas of expertise : « Image processing and pattern recognition » and « Automata and verification » with a transverse research axis « Performance and genericity ». Building on its solid scientific production and academic collaborations, the laboratory has industrial contracts, conducts internal research projects and participates in collaborative academic research projects.

·         LSV (ENS Paris-Saclay). The LSV (Laboratoire de Spécification et Vérification) is the research lab in Computer Science of the École Normale Supérieure Paris-Saclay (formerly ENS Cachan). The research at the LSV centered on the verification of software and critical system and the verification of security properties in computer systems.

·         LTCI (TELECOM ParisTech). The LTCI (Laboratoire Traitement et Communication de l’Information) is a research lab of the Telecom ParisTech High School. The research themes developed within the lab focus on core computer science, networking, signal and image processing and data communications. The S3 team develops research in the architecture, the design, modeling, development, validation and evaluation of systems, software and services, by taking into account various constraints like timing, limited ressources, mobility, scalability, interoperability, robustness and reliability.

 

Scientific programme of the summer school :

 

The lectures give during this school are grouped in the following 9 topics (lecturers provided) :

 

1.    Fundamentals of model-checking. Lecturers : Catalin Dima (LACL), Alexandre Duret-Lutz (LRDE). Topics :

   Automata over infinite words and trees.

   Temporal logics for linear time and branching time, model-checking for temporal logics.

   Introduction into modeling of computer systems with automata and transition systems, and into the verification of classical problems (mutual exclusion, scheduling, communication protocols). Introduction to model-checking using the NuXMV tool.

   Utilization of the Spot model-checker developed at LRDE for the model-checking of linear-time properties.

2.    Introduction to the verification of probabilistic systems. Lecturers : Nihal Pekergin (LACL), Paolo Ballarini (École Centrale de Paris), Benoît Barbot (LACL), Lynda Mokdad (LACL). Topics :

   Temporal and probabilistic (Markovian) models : discrete and continuous Markov chains and their verification problems.

   Verification of Markov Decision Processes.

   Temporal probabilistic logics.

   Introduction to the PRISM model-checker and to the modeling and verification of classical problems using PRISM.

   Stochastic discrete event systems and their verification problems.

   Introduction to the statistical model-checker COSMOS and to the verification platform CosyVérif, developed by members of the MeFoSyLoMa seminar.

3.    Introduction to the modeling and verification using Petri Nets. Lecturers : Fabrice Kordon (LIP6), Laure Petrucci (LIPN), Étienne André (LIPN), Christine Choppy (LIPN), Thomas Chatain (LSV), Franck Pommereau (IBISC). Topics :

   Introduction to Petri Nets and Vector Addition Systems.

   Undecidable problems for parametric systems.

   Modeling of communication protocols with Petri Nets.

   Utilization of the TiNA Petri Net modeling tool.

   Modeling with ABCD based on Petri Boxes, verification with Neco and SNAKES, tools developed at IBISC.

4.    Introduction to the modeling and verification of timed and hybrid systems. Lecturers : Béatrice Bérard (LIP6), Hanna Klaudel (IBISC), Étienne André (LIPN), Thomas Chatain (LSV).

   Timed automata, difference bound matrices and the region construction

   Logics for timed systems.

   Parametric timed automata, frontiers of decidability of parametric timed systems.

   Introduction to the modeling and verification of timed systems using the UppAal model-checker.

5.    Advanced SAT-based technologies for system verification. Lecturer : Souheib Baarir (LIP6)

   SAT encodings.

   Techniques for reducing the search space for SAT problems.

6.    Games and synthesis of programs and controllers. Lecturers : Youssouf Oualhadj (LACL), Nathalie Sznajder (LIP6). Topics

   Classical two-player zero-sum non-deterministic and probabilistic games. Algorithms for solving two-player games, classical complexity results.

   Solution concepts for multi-player games (Nash equilibria, perfect subgame equilibria, etc.).  Recent results giving algorithms for computing equilibria in games, open problems.

   Partial observation in games, impact on the decidability and complexity of solving the games.

   Relationship with program and controller synthesis, challenges for the practical applications.

7.    Introduction to multi-agent systems. Lecturers : Francesco Belardinelli (IBISC), Catalin Dima (LACL). Topics :

   Epistemic logics for the representation of intelligent agents.

   Combinations of temporal and epistemic logics.

   Multi-agent modeling and introduction to the model-checker for multi-agent systems MCMAS.

   Some classical and some new directions in multi-agent modeling and verification (zero knowledge protocols, voting protocols)

8.    Introduction to interactive theorem proving. Lecturers : Julien Tesson (LACL), Luidnel Maignan (LACL). Topics :

   Introduction to the Coq proof assistant : basic functional programming, stating logical properties and proving their correctness.

   Introduction to the reasoning on formal properties of programming language and to programs correctness.

   The Curry-Howard correspondance.

9.    Applications. Lecturers : Stefan Haar (LSV), Béatrice Bérard (LIP6). Topics :

   Diagnosticability of systems.

   Biological networks.

 

 

Tentative planning.

Each 3h30 morning or afternoon slot contains a 30 min coffee break.

 

Monday 2/07

8h30-12h : Fundamentals of model-checking. Lecture

13h30-15h30 : Fundamentals of model-checking. Lecture

16h-17h30 : Français Langue Étrangère (FLE). Lecture

 

Tuesday 3/07

8h30-12h : Fundamentals of model-checking -- modeling with NuXMV. Lecture

13h30-17h : Modeling with NuXMV. Lab class

 

Wednesday 4/07

8h30-12h : Introduction to probabilistic verification. Lecture

13h30-15h30 : Modeling with Spot. Lab class.

16h-17h30 : Français Langue Étrangère (FLE). Lecture.

 

Thursday 5/07

8h30-12h : Introduction to probabilistic verification. Lecture + Lab class.

13h30-17h : Introduction to Petri Nets. Lecture.

 

Friday 6/07

8h30-12h : Introduction to probabilistic verification. Lecture + Lab class.

13h30-15h30 : Modeling with Petri Nets. Lab class

16h-17h30 : Français Langue Étrangère (FLE). Lecture

 

Monday 9/07

8h30-12h : Introduction to the verification of timed and hybrid systems. Lecture

13h30-15h30 : Modeling of timed systems with UppAal. Lab class

16h-17h30 : Français Langue Étrangère (FLE). Lecture

 

Tuesday 10/07

8h30-12h : Modeling and verification with Petri Nets. Lecture.

13h30-17h : Introduction to the CosyVerif platform, 1h30 Lecture + 1h30 Lab class

 

Wednesday 11/07

8h30-12h : SAT technologies. Lecture.

13h30-15h30 : Timed and hybrid modeling. Lecture.

16h-17h30 : Français Langue Étrangère (FLE). Lecture.

 

Thursday 12/07

8h30-12h : Timed and hybrid modeling with UppAal. Lab class.

13h30-17h après-midi : Parametric modeling and verification. Lecture.

 

Friday 13/07

8h30-12h : Games and synthesis. Lecture.

13h30-15h30 : Introduction to multi-agent systems. Lecture.

16h-17h30 : Français Langue Étrangère (FLE). Lecture.

 

Monday 16/07

8h30-12h : Games and synthesis. Lecture.

13h30-15h30 : Introductino to multi-agent systems with MCMAS. Lecture.

16h-17h30 : Français Langue Étrangère (FLE). Lecture.

 

Tuesday 17/07

8h30-12h : Games and synthesis. Lecture.

13h30-17h : Introduction to proof assistants. Lecture.

 

Wednesday 18/07

8h30-12h : Introduction to multi-agent systems with MCMAS, 1h30 Lecture + 1h30 Lab class

13h30-15h30 : Introduction to proof assistants. Lecture.

16h-17h30 : Français Langue Étrangère (FLE)

 

Thursday 19/07

8h30-12h : Introduction to proof assistants, 1h30 Lecture + 1h30 Lab class.

13h30-17h :  9h-12h30 : Applications : diagnosis. Lecture.

 

Friday 20/07

8h30-12h : Introduction to multi-agent systems with MCMAS, 1h30 Lecture + 1h30 Lab class

14h-17h30 : Applications : biological networks. Lecture.

 

Cultural activities.

During the three Saturdays of their visit, the participans at the school will be accompanied in long visits of high touristic spots around Paris : the Louvre Museum, Tour Eiffel and Notre Dame de Paris, Château de Versailles and its gardens. During these visits they will be accompanied by students at UPEC.

 

Three “official” dinners, one each week, will be organized together with the lecturers and the staff of the summer school : a “welcome dinner”, a “bâteau-mouche dinner” on the Seine and a “farewell dinner”.

A welcome breakfast will be organized on the first Monday.

 

 

 

 

REGISTRATION

 

Specification and Verification of Critical Systems, SpeVeCriS

From July 2nd to 21st, 2018 in Université Paris-Est.

The total number of places is limited to 25.

The price does not include the trip from China to Paris.

Accommodation, meals and local transportation are all included.

The summer school will deliver ECTS (to be confirmed).

The summer school is reserved to Chinese master students.

To apply, please follow the application procedure on the main page.

Price: 25.000 CNY

The French Embassy reserves a limited number of grants to students with an exceptional academic background. Grants cover the tuition fees but do not cover the trip from China to Paris.