Outils pour utilisateurs
muc_2009_2010_lecture3
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_lecture3 [2010/01/04 13:43] tigli créée |
muc_2009_2010_lecture3 [2010/01/05 08:25] (Version actuelle) tigli |
||
|---|---|---|---|
| Ligne 7: | Ligne 7: | ||
| - | There are currently two families of formal methods. These two approaches are complementary. | + | ===== Part 1 : How to Design Components in a Middleware for Ubiquitous Computing WComp 2.0 ===== |
| - | ===== Proof-based verification ===== | ||
| - | Example : such as B or Z | + | * Date : December, 15th 2009 |
| + | * Instructor : A. Ressouche - J-Y. Tigli | ||
| + | * Duration : 3h | ||
| - | In proof-based methods, the model is described by | + | ==== Ressources : ==== |
| - | means of axioms, properties are theorems to be verified using a theorem prover. | + | |
| - | Proof-based techniques allow the analysis of infinite systems. However, the use of a theorem prover is a very difficult and a very technical task that is hard to automate. | + | * Tutorial slides : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture1/Tutorial1_MUC_UBINET_2010_Slides.pdf|Middleware for Ubiquitous Computing WComp 2.0]] |
| + | * Tutorial paper : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture1/Tutorial1_MUC_Ubinet_2010_Doc.pdf|Middleware for Ubiquitous Computing WComp 2.0]] | ||
| - | === References === | ||
| - | * Abrial, J., “Z: an introduction to formal methods,” Cambridge University Press, 1995. | ||
| - | * Diller, A., “The B-book,” John Willey & SONS, 1994. | ||
| - | ===== Model-checking ===== | ||
| - | Example : such as Spin or Lustre. | + | * VMware WComp environment iw distributed on DVD and USB Key during the lecture. |
| + | * Remark : If you're under linux be careful : replace the configuration file of your virtual machine vmplayer by [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture1/ |this one ]] and then after running, start the audio service | ||
| + | * Remark : Find here a Light UPnP server if you need [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture1/ |UPnP Light]] | ||
| - | In model checking, the model is expressed using a language from which an exhaustive | + | * Correction : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture1/Correction.zip |Tutorial correction]] |
| - | execution can be computed (this usually requires a mathematically based | + | |
| - | 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. | + | |
| - | Model checking is dedicated to finite-state systems but modeling and verification can be done using graphical toolkits and most steps can be automated | + | ==== References : ==== |
| - | === References === | + | * [[http://rainbow.i3s.unice.fr/wikiwcomp/| Official WComp Project Website]] |
| + | * Vincent Hourdin, Jean-Yves Tigli, Stéphane Lavirotte, Gaëtan Rey, Michel Riveill, “SLCA, Composite Services for Ubiquitous Computing”, in the proceedings of the International Conference on Mobile Technology, Applications and Systems, Sep 2008. | ||
| + | * 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://www.ijcsi.org/papers/4-1-1-9.pdf|paper}}. | ||
| + | * 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, éditeur Springer Paris, ISSN 0003-4347 (Print) 1958-9395 (Online), Vol. 64, No 3-4, March-April 2009, {{http://www.springerlink.com/content/x833j0143h133v67/fulltext.pdf|paper}}. | ||
| - | * Halbwachs, N., A tutorial of Lustre (1993). | + | ===== Part 2 : How to Design Proved Components in WComp Middleware ===== |
| - | + | ||
| - | + | ||
| - | ====== Ressources : ====== | + | |
| - | + | ||
| - | * Slides of the lecture "Synchronous Languages Verification" : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Lecture2_MUC_UBINET_2010_verif_slides.pdf|Synchronous Languages Verification]] | + | |
| - | + | ||
| - | * Sample Lustre programs to illustrate the lecture [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Lecture%202%20Sample%20programs.zip|Sample Lustre programs]] | + | |
| * Documentation for the tutorial 3 " Verification with Lustre and Lesar " : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Tutorial3_MUC_Ubinet_2010_Doc.pdf|Tutorial 3, Verification with Lustre and Lesar]] | * Documentation for the tutorial 3 " Verification with Lustre and Lesar " : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Tutorial3_MUC_Ubinet_2010_Doc.pdf|Tutorial 3, Verification with Lustre and Lesar]] | ||
| - | |||
| * Sample code in Lustre: [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Tutorial3/|Tutorial 3, sample code in Lustre]] | * Sample code in Lustre: [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Tutorial3/|Tutorial 3, sample code in Lustre]] | ||
| - | |||
| - | |||
| * Documentation for the tutorial 2 "Creating an advanced Component in WComp 2.0" : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Tutorial2_MUC_Ubinet_2010_Doc.pdf|Tutorial 2, Creating an advanced Component in WComp 2.0]] | * Documentation for the tutorial 2 "Creating an advanced Component in WComp 2.0" : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/Tutorial2_MUC_Ubinet_2010_Doc.pdf|Tutorial 2, Creating an advanced Component in WComp 2.0]] | ||
| - | ===== References ===== | + | ===== Part 3 : Student Projects ===== |
| - | + | ||
| - | * On the Formal Verification of Middleware Behavioral Properties, Jérôme Huguesa, Thomas Vergnauda, Laurent Pauteta, Yann Thierry-Miega, Soheib Baarira, and Fabrice Kordona, Electronic Notes in Theoretical Computer Science, Elsevier editor, Volume 133, 31 May 2005, Pages 139-157, Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004) | + | |
| - | + | ||
| - | + | ||
| - | ====== Tools : ====== | + | |
| - | + | ||
| - | + | ||
| - | ===== Lustre ===== | + | |
| - | + | ||
| - | Software : [[http://www-verimag.imag.fr/~raymond/LNW1023/|Lustre V4 / Lesar Distribution]] | + | |
| - | + | ||
| - | Lustre/Lesar V4 for cygwin | + | |
| - | + | ||
| - | This distribution is experimental. | + | |
| - | + | ||
| - | == Requirements :== | + | |
| - | + | ||
| - | It requires a recent, fully installed version of the cygwin system for Windows (gcc, g++, tcl/tk etc). | + | |
| - | [[http://www.cygwin.com/|Cywin installation ]] | + | |
| - | == Installation :== | + | |
| - | + | ||
| - | Within a cygwin shell, extract the archive (typically in /usr/local). Modify your bashrc file with: | + | |
| - | + | ||
| - | export LUSTRE_INSTALL=/usr/local/lustre | + | |
| - | export PATH=$LUSTRE_INSTALL/bin:$PATH | + | |
| - | export MANPATH=$MANPATH:$LUSTRE_INSTALL/man: | + | |
| - | + | ||
| - | [[http://www-verimag.imag.fr/~raymond/LNW1023/cygwin/lv4-cyg-00.tgz|windows beta distribution]] | + | |
| - | + | ||
| - | ===== NuSMV ===== | + | |
| - | + | ||
| - | [[http://nusmv.irst.itc.it/NuSMV/index.html|An overview of NuSMV]] | + | |
| - | 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. | + | Students must provide : |
| + | * A Proved Bean Component (lustre checked code, corresponding C code generated, corresponding Bean code) | ||
| + | * A sample WComp assembly to illustrate how this proved component works. | ||
| + | * A document with all necessary explanations | ||
| - | 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, but at the same time it can introduce danger of inconsistency (for non expert users). | + | Put all these files and documents on a web site and send them to JY Tigli before february, the 1st, 2010. |
| + | Deadline : february, the 1st, 2010 | ||
| + | ^ Student Name ^ Cursus (SI5 / Uibnet) ^ Project Number ^ Project Titlte ^ Subject ^ | ||
| + | | | | 0 | Barrier | A barrier is a type of synchronization method. A barrier for a group of event means any event must stop at this point and cannot proceed until all other events reach this barrier | | ||
| + | | | | 1 | Lock | A lock is a synchronization mechanism for enforcing limits on access to a resource in an environment where there are many threads of execution. Locks are one way of enforcing concurrency control policies. Only one event is emitted at at time | | ||
| + | | | | 2 | Arbitration | Arbitration between input events | | ||
| + | | | | 3 | Average | Average value is emitted from the values of input events | | ||
| + | | | | 4 | Moving average | Average value is emitted from the values of input events | | ||
| + | | | | 5* | Function* Allaccess | returned value of one external DLL function is emitted when all value parameters are available (triggered on all input events) | | ||
| + | | | | 6* | Function* Oneaccess | returned value of one external DLL function is emitted as soon as at least on value parameter is available (triggered on one input events) | | ||
| + | | | | 7* | Function* Thisaccess | returned value of one external DLL function is emitted as soon as one specific event arrive (triggered on one specific input events) | | ||
| + | | | | 8* | Function* AllaccessNewvalue | new returned value of one external DLL function is emitted when all value parameters are available (triggered on all input events and state change) | | ||
| + | | | | 9* | Function* OneaccessNewvalue | new returned value of one external DLL function is emitted as soon as at least on value parameter is available (triggered on one input events and state change ) | | ||
| + | | | | 10* | Function* OneaccessNewvalue | new returned value of one external DLL function is emitted as soon as one specific event arrive (triggered on one specific input events and state change) | | ||
| + | | | | 11 | | | | ||
| + | | | | 12 | | | | ||
| + | | | | 13 | | | | ||
| + | | | | 14 | | | | ||
| + | | | | 15 | | | | ||
| + | | | | 16 | | | | ||
| + | | | | 17 | | | | ||
| + | | | | 18 | | | | ||
| + | | | | 19 | | | | ||
| + | | | | 20 | | | | ||
| + | | | | 21 | | | | ||
| + | | | | 22 | | | | ||
| + | | | | 23 | | | | ||
| + | | | | 24 | | | | ||
| + | | | | 25 | | | | ||
| + | | | | 26 | | | | ||
| + | | | | 27 | | | | ||
| + | | | | 28 | | | | ||
| + | | | | 29 | | | | ||
| + | | | | 30 | | | | ||
| + | | | | 31 | | | | ||
| + | | | | 32 | | | | ||
| + | | | | 33 | | | | ||
| + | | | | 34 | | | | ||
| + | | | | 35 | | | | ||
| + | | | | 36 | | | | ||
| + | | | | 37 | | | | ||
| + | | | | 38 | | | | ||
| + | | | | 39 | | | | ||
muc_2009_2010_lecture3.1262609038.txt.gz · Dernière modification: 2010/01/04 13:43 par tigli
Outils de la page
Sauf mention contraire, le contenu de ce wiki est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 4.0 International
