Show simple item record

dc.contributor.authorBen Gaid, Mongi
dc.contributor.authorBérard, Béatrice
HAL ID: 9360
dc.contributor.authorde Smet, Olivier
HAL ID: 735194
dc.date.accessioned2009-10-07T11:48:59Z
dc.date.available2009-10-07T11:48:59Z
dc.date.issued2005
dc.identifier.urihttps://basepub.dauphine.fr/handle/123456789/2158
dc.description.abstractfrDans ce travail, nous nous intéressons à des aspects temporisés de la programmation des automates programmables industriels (API). 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, avec l'outil UPPAAL, comment cette hypothèse permet d'améliorer les performances pour la vérification de propriétés de ce système.en
dc.language.isoenen
dc.subjectAutomates programmables industrielsen
dc.subjectAutomates temporisésen
dc.subjectModel checkingen
dc.subject.ddc003en
dc.titleVerification of an evaporator system with Uppaalen
dc.typeArticle accepté pour publication ou publié
dc.contributor.editoruniversityotherEcole Normale Supérieure de Cachan – Université Paris Sud - Paris XI;France
dc.contributor.editoruniversityotherINRIA Grenoble;France
dc.description.abstractenIn this work, we study some timed features for PLC (Programmable Logic Controller) programming. This study is illustrated with a two tanks system for which we propose a component based model. The control program, written in Ladder Diagram, as well as the operating part are modeled by a network of timed automata, with a strong hypothesis of atomicity about program execution. We show on this example, using the tool UPPAAL, how this hypothesis increases the efficiency of verification for several properties of the system.en
dc.relation.isversionofjnlnameJournal Européen des Systèmes Automatisés
dc.relation.isversionofjnlvol39en
dc.relation.isversionofjnlissue9-10en
dc.relation.isversionofjnldate2005
dc.relation.isversionofjnlpages1079-1098en
dc.relation.isversionofdoihttp://dx.doi.org/10.3166/jesa.39.1079-1098en
dc.description.sponsorshipprivateouien
dc.relation.isversionofjnlpublisherHermèsen
dc.subject.ddclabelRecherche opérationnelleen


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record