Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

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
Ligne 1: Ligne 1:
 {{:​mucimg.jpg|}} {{:​mucimg.jpg|}}
-===== Lecture ​Introduction to Middleware ​for Ubiquitous Computing ​=====+====== Lecture ​Formal Methods ​for Middleware verification ======
  
   * 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"​ : [[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.
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 ​... 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.pspaper }} 
 + 
 +  * 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 =====
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://​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:
Ligne 80: Ligne 95:
  
  
-===== 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)  
  
muc_2009_2010_lecture2.1260540694.txt.gz · Dernière modification: 2009/12/11 15:11 par tigli
Piste:
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
CC Attribution-Noncommercial-Share Alike 3.0 Unported
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0