muc_2009_2010_lecture2
Différences
Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentesRévision précédenteProchaine révision | Révision précédente | ||
| muc_2009_2010_lecture2 [2009/12/11 14:11] – tigli | muc_2009_2010_lecture2 [2010/01/05 11:31] (Version actuelle) – tigli | ||
|---|---|---|---|
| Ligne 1: | Ligne 1: | ||
| {{: | {{: | ||
| - | ===== Lecture | + | ====== Lecture |
| * Date : December, 14th 2009 | * Date : December, 14th 2009 | ||
| Ligne 6: | Ligne 6: | ||
| * Duration : 4h | * Duration : 4h | ||
| - | ==== Ressources : ==== | ||
| - | |||
| - | * Slides of the lecture "First trends in Middleware for Ubiquituous Computing" | ||
| - | |||
| - | |||
| - | ====== Course 2 : Formal Methods for Middleware verification ====== | ||
| There are currently two families of formal methods. These two approaches are complementary. | There are currently two families of formal methods. These two approaches are complementary. | ||
| Ligne 27: | Ligne 21: | ||
| * Abrial, J., “Z: an introduction to formal methods,” Cambridge University Press, 1995. | * Abrial, J., “Z: an introduction to formal methods,” Cambridge University Press, 1995. | ||
| * Diller, A., “The B-book,” John Willey & SONS, 1994. | * Diller, A., “The B-book,” John Willey & SONS, 1994. | ||
| - | |||
| ===== Model-checking ===== | ===== Model-checking ===== | ||
| - | |||
| Example : such as Spin or Lustre. | Example : such as Spin or Lustre. | ||
| Ligne 40: | Ligne 32: | ||
| to states (a given possible value of the system’s context). It is then possible to | to states (a given possible value of the system’s context). It is then possible to | ||
| explore the graph to check if a property is satisfied. | explore the graph to check if a property is satisfied. | ||
| - | |||
| Model checking is dedicated to finite-state systems but modeling and verification can be done using graphical toolkits and most steps can be automated | Model checking is dedicated to finite-state systems but modeling and verification can be done using graphical toolkits and most steps can be automated | ||
| Ligne 48: | Ligne 39: | ||
| * Halbwachs, N., A tutorial of Lustre (1993). | * Halbwachs, N., A tutorial of Lustre (1993). | ||
| - | ===== Verification Techniques ===== | ||
| - | {{:verification.ppt|From Testing | + | ====== Ressources : ====== |
| + | |||
| + | * Slides of the lecture " | ||
| + | |||
| + | * Lustre Manual : {{https://rainbow.i3s.unice.fr/ | ||
| + | |||
| + | * Sample Lustre programs to illustrate the lecture | ||
| + | |||
| + | * Documentation for the tutorial 3 " Verification with Lustre and Lesar " : [[http:// | ||
| + | |||
| + | * Sample code in Lustre: [[http:// | ||
| + | |||
| + | |||
| + | * Documentation for the tutorial 2 " | ||
| + | |||
| + | ===== References ===== | ||
| + | |||
| + | * On the Formal Verification | ||
| + | |||
| + | |||
| + | ====== Tools : ====== | ||
| ===== Lustre ===== | ===== Lustre ===== | ||
| Ligne 60: | Ligne 71: | ||
| This distribution is experimental. | This distribution is experimental. | ||
| - | It requires a recent, fully installed version of the cygwin system for Windows (gcc, g++, tcl/tk etc). | + | == Requirements :== |
| + | |||
| + | It requires a recent, fully installed version of the cygwin system for Windows (gcc, g++, tcl/tk etc). | ||
| + | [[http:// | ||
| + | == Installation :== | ||
| Within a cygwin shell, extract the archive (typically in / | Within a cygwin shell, extract the archive (typically in / | ||
| Ligne 80: | Ligne 95: | ||
| - | ===== References ===== | ||
| - | |||
| - | * On the Formal Verification of Middleware Behavioral Properties, Jérôme Huguesa, Thomas Vergnauda, Laurent Pauteta, Yann Thierry-Miega, | ||
muc_2009_2010_lecture2.1260540694.txt.gz · Dernière modification : 2009/12/11 14:11 de tigli