• xmlui.mirage2.page-structure.header.title
    • français
    • English
  • Help
  • Login
  • Language 
    • Français
    • English
View Item 
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Browse

BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesTypeThis CollectionBy Issue DateAuthorsTitlesType

My Account

LoginRegister

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors
Thumbnail

Modélisation et vérification d'un évaporateur en Uppaal

Ben Gaid, Mongi; Bérard, Béatrice; de Smet, Olivier (2004), Modélisation et vérification d'un évaporateur en Uppaal, in Julliand, Jacques, Proceedings 6ème Conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'04, Besançon, France, Juin 2004, LIFC : Besançon, p. 223-238

View/Open
Uppaal_berard.PDF (193.0Kb)
Type
Communication / Conférence
Date
2004
Conference title
6ème Conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04)
Conference date
2004-06
Conference city
Besançon
Conference country
France
Book title
Proceedings 6ème Conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'04, Besançon, France, Juin 2004
Book author
Julliand, Jacques
Publisher
LIFC
Published in
Besançon
Pages
223-238
Metadata
Show full item record
Author(s)
Ben Gaid, Mongi

Bérard, Béatrice

de Smet, Olivier
Abstract (FR)
Dans ce travail, nous nous intéressons aux aspects temporisés de la programmation des automates programmables industriels (API). La vérification des programmes d'API est un enjeu important pour les constructeurs, ce qui a déjà suscité de nombreux travaux. L'étude de propriétés quantitatives faisant intervenir le temps a été abordée plus récemment, avec des difficultés supplémentaires liées à l'introduction de temporisateurs et d'horloges. En utilisant l'exemple d'un mécanisme d'évaporation, nous proposons une modélisation du système contrôlé ainsi que du programme de contrôle écrit en Ladder Diagram, sous la forme d'un réseau d'automates temporisés, avec une hypothèse forte d'atomicité pour l'ensemble des instructions du programme. Nous montrons, sur cet exemple, comment cette hypothèse permet de réduire la taille du modèle et d'accélérer les calculs d'accessibilité. Les performances sont illustrées par la vérification de plusieurs propriétés de l'évaporateur avec l'outil Uppaal.
Subjects / Keywords
vérification par model-checking; automates temporisés; Automates programmables industriels

Related items

Showing items related by title and author.

  • Thumbnail
    Verification of an evaporator system with Uppaal 
    Ben Gaid, Mongi; Bérard, Béatrice; de Smet, Olivier (2005) Article accepté pour publication ou publié
  • Thumbnail
    Verification of a timed multitask system with UPPAAL 
    Roussel, Jean-Marc; de Smet, Olivier; Bel Mokadem, Houda; Bérard, Béatrice; Gourcuff, Vincent (2005) Communication / Conférence
  • Thumbnail
    Comparison of the Expressiveness of Timed Automata and Time Petri Nets 
    Roux, Olivier-Henri; Bérard, Béatrice; Cassez, Franck; Haddad, Serge; Lime, Didier (2005) Communication / Conférence
  • Thumbnail
    When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets? 
    Roux, Olivier-Henri; Lime, Didier; Haddad, Serge; Cassez, Franck; Bérard, Béatrice (2005) Communication / Conférence
  • Thumbnail
    Comparison of Different Semantics for Time Petri Nets 
    Roux, Olivier-Henri; Lime, Didier; Haddad, Serge; Cassez, Franck; Bérard, Béatrice (2005) Communication / Conférence
Dauphine PSL Bibliothèque logo
Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16
Phone: 01 44 05 40 94
Contact
Dauphine PSL logoEQUIS logoCreative Commons logo