skip to main content
Guest
My Research
My Account
Sign out
Sign in
This feature requires javascript
Library Search
Find Databases
Browse Search
E-Journals A-Z
E-Books A-Z
Citation Linker
Help
Language:
English
Vietnamese
This feature required javascript
This feature requires javascript
Primo Search
All Library Resources
All
Course Materials
Course Materials
Search For:
Clear Search Box
Search in:
All Library Resources
Or hit Enter to replace search target
Or select another collection:
Search in:
All Library Resources
Search in:
Print Resources
Search in:
Digital Resources
Search in:
Online E-Resources
Advanced Search
Browse Search
This feature requires javascript
Search Limited to:
Search Limited to:
Resource type
criteria input
anywhere in the record
in the title
as author/creator
in subject
Full Text
ISBN
ISSN
TOC
Keyword
Field
Show Results with:
in the title
Show Results with:
anywhere in the record
in the title
as author/creator
in subject
Full Text
ISBN
ISSN
TOC
Keyword
Field
Show Results with:
criteria input
that contain my query words
with my exact phrase
starts with
Show Results with:
Search type Index
criteria input
AND
OR
NOT
This feature requires javascript
A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions
Attribution
Digital Resources/Online E-Resources
Citations
Cited by
View Online
Details
Recommendations
Reviews
Times Cited
External Links
This feature requires javascript
Actions
Add to My Research
Remove from My Research
E-mail
Print
Permalink
Citation
EasyBib
EndNote
RefWorks
Delicious
Export RIS
Export BibTeX
This feature requires javascript
Title:
A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions
Author:
Cousineau, Denis
;
Inoue, Hiroaki
;
Marché, Claude
;
Mentré, David
Subjects:
Computer Science
Description:
Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In a previous work, we proposed a method for verifying that a given Ladder program conforms to an expected behaviour expressed by a timing chart, describing a scenario of execution. This method relies on a modelling of Ladder programs in WhyML, the language of the Why3 environment for deductive program verification. In this approach, the WhyML modelling of individual Ladder instructions has to be trusted.This report proposes a methodology to increase the trust in the WhyML modelling of Ladder instructions. Our approach relies on a comparison of the execution of Ladder programs with an execution by Why3 of a simulation of the translated program. With this technique, we have been able to validate our modelling of Ladder instructions, and also discover and fix a subtle bug in the modelling of one particular instruction. Les automates programmables industriels (PLC en anglais) sont des dispositifs numériques industriels utilisés pour contrôler les processus de fabrication automatisés, tels que les lignes d'assemblage. Le langage Ladder est un langage de programmation utilisé pour développer des logiciels pour de tels dispositifs. Dans un travail précédent, nous avons proposé une méthode pour vérifier qu'un programme Ladder donné est conforme à un comportement attendu exprimé par un diagramme de temps, décrivant un scénario d'exécution. Cette méthode s'appuie sur une modélisation des programmes Ladder en WhyML, le langage de l'environnement Why3 pour la vérification déductive des programmes. Cette méthode s'appuie sur une modélisation des instructions individuelles Ladder, à laquelle il faut faire confiance. Ce rapport propose une méthodologie pour accroître la confiance dans la modélisation WhyML des instructions Ladder. Notre approche repose sur une comparaison des exécutions d'un programme Ladder avec une exécution par Why3 d'une simulation du programme traduit. Grâce à cette technique, nous avons pu valider notre modélisation des instructions Ladder, et également découvrir et corriger un bug subtil dans la modélisation d’une instruction particulière.
Creation Date:
2024
Language:
English
Source:
Hyper Article en Ligne (HAL) (Open Access)
This feature requires javascript
This feature requires javascript
Back to results list
This feature requires javascript
This feature requires javascript
Searching Remote Databases, Please Wait
Searching for
in
scope:(TDTS),scope:(SFX),scope:(TDT),scope:(SEN),primo_central_multiple_fe
Show me what you have so far
This feature requires javascript
This feature requires javascript