MOSIG 2 - Option DEMIPS - UE Embedded Systems

Un article de Ensiwiki.

Sommaire

1 This is the page for the "Embedded Systems" course of the MOSIG, 2009-2010 edition.
2 The calendar
3 Notes, slides
4 General Information, additional reading
5 Research Proposals related to the course
6 Archives

This is the page for the "Embedded Systems" course of the MOSIG, 2009-2010 edition.

For this edition, the teachers are:

(FM) Florence Maraninchi (Verimag laboratory), see webpage [1]
(BJ) Barbara Jobtsmann (now Verimag laboratory, previously with EPFL), see webpage [2]

The course is on wednesday afternoon, from 14:00 to 17:00, from September 23, 2009 to January 20, 2010. We will not teach every week.

The calendar

The course can be found on the official calendar web pages of Grenoble INP/Ensimag or UJF/UFRIMAG (the ADE pages), but the very last news will be here. Please check this calendar.

wednesday, sep 23 (1) FM General introduction, constraints for the design of embedded systems, models, verification problems (where: CUEFA 113)
wednesday,sep 30 (2) FM asynchronous models - principles, examples (where: Ensimag H103, the map is here (choose Ensimag Campus), there are two green circles, Building H is the left one)
wednesday, oct 7 no course
wednesday, oct 14 no course
wednesday, oct 21 (3) FM asynchronous models (a modeling exercise, adding time), synchronous models - principles, time in synchronous models. Where : H103 (see last lecture).
wednesday, oct 28 no course - holidays
wednesday, nov 4 (4) (H103) FM synchronous models (examples, modeling asynchrony with synchronous products)
thursday, nov 12 (5) (D117) FM a model-extraction example, abstract interpretation
wednesday, nov 18 (6) (H103) FM abstract interpretation

Wednesday nov 25 (7) BJ (H103 from 14:00 to 15:30, then E201 from 15:30 to 17:00)
dec 2 (8) BJ (H103 from 14:00 to 15:30, then E201 from 15:30 to 17:00)
dec 9 no course
dec 16 9 BJ (H103 from 14:00 to 15:30, then E201 from 15:30 to 17:00)
jan 6 10 BJ (H103 from 14:00 to 15:30, then E201 from 15:30 to 17:00)
jan 13 11 BJ (H103 from 14:00 to 15:30, then E201 from 15:30 to 17:00)
jan 20 12 BJ (H103 from 14:00 to 15:30, then E201 from 15:30 to 17:00)
jan 27, this is the week of the EXAMS

Notes, slides

The pdf files

For the first part by FM, the files are available here: [3]

First part, General Introduction on embedded systems, models, validation
Second part, from systems to models to verification tools, asynchronous models
Third part, brief introduction to synchronous models.
Fourth part, examples of synchronous models/programs, asynchronous vs. synchronous models, model-extraction for SystemC
Fifth part, abstract interpretation

Additional files :

A paper on the analysis of caches
a set of slides on convex polyhedra and relational analysis

For the second part by BJ, the files are available:

Slides for the first lecture [4], Exercises[5] Solutions [6][7]

Slides for the second lecture [8], Exercises[9], Solutions[10],

Slides for the third lecture [11], slides from Daniel Kroening on BDDs [12], Exercises[13], miniBDD[14] Solutions: miniBdd file Summary of solutions

Slides for the fourth lecture [15], Exercises [16], Dining philosophers[17][18] Solutions [19]

Slides for the fifth lecture [20], Exercises [21], Solutions [22]

Slides for the sixth lecture [23]

Structure of the course (first part by F. Maraninchi)

On sep 23 I used slides 1-39, 56-61, 66-70, 73-92, 134-137.

On sep 30 I used slides 110 to 135 (from systems to models to formal verification).

+ slides 144 to 179 (asynchronous models).

Exercise: on slide 176, substitute P(s1) to P(s2) on the transition between X' and B'. Build the graph of all possible behaviors. How do you observe the bug on this graph?

On oct 21, we looked at how to model cooperative threads that communicate with events, using asycnhronous products. Then we discussed the introduction of time in asynchronous models. Then I used slide from yhr third part, to introduce synchronous models. Then we had quite informal discussions on time in synchronous models.

On nov 4, I used slides 278-355 and then 370-374

On nov 12, I used slides 356-369, and then started abstract interpretation (slides 386 to 457, 473-475, 478-492).

On nov 18 (last lecture), I used the additional slides on convex polyhedra by N. Halbwachs [24], used the slides 520-590 on the theory of fix points, Galois connections, and abstract interpretation, and finally used the slides 506-519 on the cache example described in the paper available here [25].

Structure of the course (second part by B. Jobstmann)

The second part of the course gives an introduction to a verification technique called model checking.

On nov 25: examples of systems and properties that can be verified by model checking, translation of Verilog (a synchronous language use to describe hardware) to transition graphs, syntax and semantics of Computation Tree Logic (CTL), a popular temporal logic for the specification of properties.

On dec 2: CTL-model checking based on fixpoint computation

On dec 16: Symbolic Model Checking and Binary Decision Diagrams (BDD)

On jan 6: CTL with fairness, generation of counterexample and witnesses to analyze the result

On jan 13: bisimulation and simulation, syntax and semantics of LTL, another temporal logic that is commonly used.

On jan 20: Model checking algorithms for LTL based on Buchi automaton, which are automaton that accept infinite strings.

General Information, additional reading

An article describing a complete automaton-based synchronous language [26]
Courses at Collège de France:
- Gérard Berry 2007 [27], in particular [28]
- Gérard Berry 2009 [29]
Verimag Laboratory [30]
The SCADE Tool [31]
The short story on the map of the world at the scale 1:1, Jorge Luis Borges, Del rigor en la ciencia - Historia universal de la infamia [32]
A note on the DO 178B norm for safety-critical software in avionics [33]
2007 Turing Award, model-checking [34]
Ariane 5 crash (flight 501, 1996) [35]
The MathWorks/Polyspace [36]
Several examples of industrial verification tools:
- Prover Technologies [37]
- Cadence [38]
- Mentor [39]

Books:
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, 1992.
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety, 1995.
- E. Clarke, O. Grumberg, and D. Peled, Model Checking, 2000.
- C. Baier and J.-P. Katoen, Principles of Model Checking, 2008.

Research Proposals related to the course

Some of the research proposals of the MOSIG 2R are related to the contents of the course. You can also check the "master" section of the list published here: [40].