muc_2009_2010_lecture2
Différences
Ci-dessous, les différences entre deux révisions de la page.
Prochaine révision | Révision précédente | ||
muc_2009_2010_lecture2 [2009/12/11 14:09] – créée 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 | + | There are currently two families |
- | ==== References : ==== | + | ===== Proof-based verification ===== |
+ | Example : such as B or Z | ||
- | * CLASSICAL MIDDLEWARES : | + | In proof-based methods, the model is described by |
- | | + | means of axioms, properties are theorems to be verified using a theorem prover. |
- | * MIDDLEWARES TAXONOMIES : | + | Proof-based techniques allow the analysis of infinite systems. However, the use of a theorem prover is a very difficult |
- | * W. Emmerich Taxonomy (2000) | + | |
- | * D.E. Baken (2001) | + | |
- | * R. E. Schantz | + | |
+ | === References === | ||
+ | * Abrial, J., “Z: an introduction to formal methods,” Cambridge University Press, 1995. | ||
+ | * Diller, A., “The B-book,” John Willey & SONS, 1994. | ||
- | * NEW TRENDS FOR MIDDLEWARES | + | ===== Model-checking ===== |
- | * A Perspective on the Future of Middleware-based Software Engineering. | + | |
- | * Middleware for Network Eccentric and Mobile Applications; | + | |
- | * A Perspective on the Future of Middleware-based Software Engineering. V. Issarny, M. Caporuscio, N. Georgantas. In Future of Software Engineering 2007 (FOSE) at ICSE (International Conference on Software Engineering). L. Briand and A. Wolf editors, IEEE-CS Press. 2007. | + | |
- | * A Survey on Service Composition Middleware in Pervasive Environments Ibrahim N., Le Mouël F. International Journal of Computer Science Issues (IJCSI) 1 (2009) 1–12 | + | |
- | * Middleware Technologies for Ubiquitous Computing, Ibrahim N., Le Mouël F., Frénot S, in Handbook of Research on Next Generation Networks and Ubiquitous Computing, IGI Global Publication (Ed.) (2009) | + | |
- | * Gordon Blair, “From Mobility to Ubiquity and Beyond: Challenges to Middleware”, | + | |
- | ===== Tutorial 1 : Middleware for Ubiquitous Computing WComp 2.0 ===== | + | Example |
- | * Date : December, 7th 2009 | + | In model checking, the model is expressed using a language from which an exhaustive |
- | * Instructor : J.-Y. Tigli | + | execution can be computed (this usually requires a mathematically based |
- | * Duration : 3h | + | definition). An “execution engine” produces the exhaustive state space associated |
+ | to the system as a graph where actions (atomic instructions in the language) relate | ||
+ | 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. | ||
- | ==== Ressources : ==== | + | Model checking is dedicated to finite-state systems but modeling and verification can be done using graphical toolkits and most steps can be automated |
- | * Tutorial slides : [[http:// | + | === References |
- | * Tutorial paper : [[http:// | + | |
+ | * Halbwachs, N., A tutorial of Lustre (1993). | ||
- | | + | ====== Ressources : ====== |
- | | + | |
- | * Remark | + | |
+ | |||
+ | | ||
+ | |||
+ | * Sample Lustre programs to illustrate the lecture | ||
+ | |||
+ | * Documentation for the tutorial 3 " Verification with Lustre | ||
+ | |||
+ | | ||
+ | |||
+ | |||
+ | * Documentation for the tutorial 2 " | ||
+ | |||
+ | ===== References ===== | ||
+ | |||
+ | * On the Formal Verification of Middleware Behavioral Properties, Jérôme Huguesa, Thomas Vergnauda, Laurent Pauteta, Yann Thierry-Miega, | ||
+ | |||
+ | |||
+ | ====== Tools : ====== | ||
+ | |||
+ | |||
+ | ===== Lustre ===== | ||
+ | |||
+ | Software : [[http:// | ||
+ | |||
+ | Lustre/ | ||
+ | |||
+ | This distribution is experimental. | ||
+ | |||
+ | == 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 / | ||
+ | |||
+ | export LUSTRE_INSTALL=/ | ||
+ | export PATH=$LUSTRE_INSTALL/ | ||
+ | export MANPATH=$MANPATH: | ||
+ | |||
+ | [[http:// | ||
+ | |||
+ | ===== NuSMV ===== | ||
+ | |||
+ | [[http:// | ||
+ | |||
+ | |||
+ | NuSMV is a software tool for the formal verification of finite state systems. It has been developed jointly by ITC-IRST and by Carnegie Mellon University. | ||
+ | |||
+ | NuSMV allows to check finite state systems against specifications in the temporal logic CTL. The input language of NuSMV is designed to allow the description of finite state systems that range from completely synchronous to completely asynchronous. The NuSMV language (like the language of SMV) provides for modular hierarchical descriptions and for the definition of reusable components. The basic purpose of the NuSMV language is to describe (using expressions in propositional calculus) the transition relation of a finite Kripke structure. This provides a great deal of flexibility, | ||
- | * Correction : [[http:// | ||
- | ==== References : ==== | ||
- | * [[http:// | ||
- | * Vincent Hourdin, Jean-Yves Tigli, Stéphane Lavirotte, Gaëtan Rey, Michel Riveill, “SLCA, Composite Services for Ubiquitous Computing”, | ||
- | * J.-Y. Tigli, S. Lavirotte, G. Rey, V. Hourdin, M. Riveill, “Lightweight Service Oriented Architecture for Pervasive Computing” IJCSI International Journal of Computer Science Issues, Vol. 4, No. 1, September 2009, ISSN (Online): 1694-0784, ISSN (Print): 1694-0814, {{http:// | ||
- | * J.-Y. Tigli, S. Lavirotte, G. Rey, V. Hourdin, D. Cheung, E. Callegari, M. Riveill “WComp middleware for ubiquitous computing: Aspects and composite event-based Web services” in Annals of Telecommunications, |
muc_2009_2010_lecture2.1260540569.txt.gz · Dernière modification : 2009/12/11 14:09 de tigli