Pascal Raymond Chargé de Recherche au CNRS Laboratoire VERIMAG Centre Equation 2, avenue de Vignate F-38610 Gières Cedex FRANCE Tel: +33/0 456 52 03 56 Fax: +33/0 456 52 03 44 Pascal.Raymond@imag.fr

Enseignement

Ensimag SLE 3a, Modélisation Réaliste et Implantation

• La page générale (Thao Dang)
• La page dédiée à la méthode Simulink -> Lustre -> OSEK
• La page dédiée au chargement des programmes
  

Année 2009/2010

• Approche Synchrone EJCP'11-Dinard

• 19 mars 2010, CNAM : cours Méthodes formelles de développement (5) Modèles des systèmes réactifs et parallèles.
• 26 mars 2010, CNAM : cours Méthodes formelles de développement (6) Programmation Synchrone.

• Approche Synchrone

Teaching

• Synchronous Approach tutorial slides

• Lego NXT ressources

• Publications
• Some tools
• Photo

Tools

• The Lustre/Lesar distribution provides a compiler and a model checker for the Lustre programming language. The manual pages are available here (Post-Script).

• BDDC v2 is a (simple) symbolic calculator based on bdds (binary decision diagrams).

• Reglo is a compiler which translates regular expressions into either a set of language equations, or into a Lustre program.

Research interests

• Reactive, Real-Time, Synchronous programming.
• The Lustre data-flow synchronous language.
• Automatic verification of finite-state systems.

Short Curriculum Vitae