| Les deux révisions précédentes
Révision précédente
Prochaine révision
|
Révision précédente
|
muc_2009_2010_lecture2 [2009/12/11 15:11]
tigli |
muc_2009_2010_lecture2 [2010/01/05 12:31] (Version actuelle)
tigli |
| {{:mucimg.jpg|}} | {{:mucimg.jpg|}} |
| ===== Lecture 1 : Introduction to Middleware for Ubiquitous Computing ===== | ====== Lecture 2 : Formal Methods for Middleware verification ====== |
| |
| * Date : December, 14th 2009 | * Date : December, 14th 2009 |
| * Duration : 4h | * Duration : 4h |
| |
| ==== Ressources : ==== | |
| |
| * Slides of the lecture "First trends in Middleware for Ubiquituous Computing" : [[http://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture1/Lecture1_MUC_UBINET_2010_slides.pdf|Middleware for Ubiquitous Computing WComp 2.0]] | |
| |
| |
| ====== 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. |
| * 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. |
| 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 |
| * Halbwachs, N., A tutorial of Lustre (1993). | * Halbwachs, N., A tutorial of Lustre (1993). |
| |
| ===== Verification Techniques ===== | |
| |
| {{:verification.ppt|From Testing ... through Static Analysis... to Formal Verification (Annie Ressouche)}} | ====== 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]] |
| | |
| | * Lustre Manual : {{https://rainbow.i3s.unice.fr/~tigli/cours/MUC/Lecture2/LustreManual/lv4man.ps| paper }} |
| | |
| | * 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]] |
| | |
| | * 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]] |
| | |
| | ===== References ===== |
| | |
| | * 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 ===== | ===== Lustre ===== |
| 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://www.cygwin.com/|Cywin installation ]] |
| | == Installation :== |
| |
| Within a cygwin shell, extract the archive (typically in /usr/local). Modify your bashrc file with: | Within a cygwin shell, extract the archive (typically in /usr/local). Modify your bashrc file with: |
| |
| |
| ===== References ===== | |
| |
| * 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) | |
| |
