• 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

Verification of a timed multitask system with UPPAAL

Roussel, Jean-Marc; de Smet, Olivier; Bel Mokadem, Houda; Bérard, Béatrice; Gourcuff, Vincent (2005), Verification of a timed multitask system with UPPAAL, Proceedings of 10th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2005, September 19-22, 2006, Catania, Italy, IEEE. http://dx.doi.org/10.1109/ETFA.2005.1612699

View/Open
publi66.pdf (221.2Kb)
Type
Communication / Conférence
Date
2005
Conference title
10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2005)
Conference date
2005-09
Conference city
Catane
Conference country
Italie
Book title
Proceedings of 10th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2005, September 19-22, 2006, Catania, Italy
Publisher
IEEE
ISBN
0-7803-9401-1
Publication identifier
http://dx.doi.org/10.1109/ETFA.2005.1612699
Metadata
Show full item record
Author(s)
Roussel, Jean-Marc

de Smet, Olivier

Bel Mokadem, Houda

Bérard, Béatrice
Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision [LAMSADE]
Gourcuff, Vincent
Abstract (EN)
Since it is an important issue for users and system designers, verification of PLC programs has already been studied in various contexts, mostly for untimed programs. More recently, timed features were introduced and modeled with timed automata. In this case study, we consider a part of the so-called MSS (mecatronic standard system) platform from Bosh group, a framework where time aspects are combined with multitask programming. Our model for station 2 of the MSS platform is a network of timed automata, including automata for the operative part and for the control program, written in Ladder Diagram. This model is constrained with atomicity hypotheses concerning program execution and model checking of a reaction time property is performed with the tool UPPAAL.
Subjects / Keywords
Programmable Logic Controllers; Timed Automata; Model Checking

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
    Timed temporal logics for abstracting transient states 
    Bel Mokadem, Houda; Bérard, Béatrice; Bouyer, Patricia; Laroussinie, François (2006) Communication / Conférence
  • Thumbnail
    A New Modality for Almost Everywhere Properties in Timed Automata 
    Bel Mokadem, Houda; Bérard, Béatrice; Bouyer, Patricia; Laroussinie, François (2005) Communication / Conférence
  • Thumbnail
    Modélisation et vérification d'un évaporateur en Uppaal 
    Ben Gaid, Mongi; Bérard, Béatrice; de Smet, Olivier (2004) 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
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