Publication
Contract Based Verification of IEC 61499
| dc.contributor.author | Pereira, David | |
| dc.contributor.author | Pinho, Luís Miguel | |
| dc.contributor.author | Lindgren, Per | |
| dc.contributor.author | Lindner, Marcus | |
| dc.date.accessioned | 2017-02-06T14:48:24Z | |
| dc.date.available | 2017-02-06T14:48:24Z | |
| dc.date.issued | 2016 | |
| dc.description | 14th International Conference on Industrial Informatics (INDIN 2016). 18 to 21, Jul, 2016, Factory Automation. Poitiers, France. | pt_PT |
| dc.description.abstract | The IEC 61499 standard proposes an event driven execution model for component based (in terms of Function Blocks), distributed industrial automation applications. However, the standard provides only an informal execution semantics, thusin consequence behavior and correctness relies on the design decisions made by the tool vendor. In this paper we present the formalization of a subset of the IEC 61499 standard in order to provide an underpinning for the static verification of Function Block models by means of deductive reasoning. Specifically, we contribute by addressing verification at the component,algorithm, and ECC levels. From Function Block descriptions, enrichedwith formal contracts, we show that correctness of component compositions, as well as functional and transitional behavior can be ensured. Feasibility of the approach is demonstrated by manually encoding a set of representative use-cases in WhyML,for which the verification conditions are automatically derived (through the Why3 platform) and discharged (using automaticSMT-based solvers). Furthermore, we discuss opportunities and challenges towards deriving certified executables for IEC 61499 models. | pt_PT |
| dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
| dc.identifier.doi | 10.1109/INDIN.2016.7819147 | pt_PT |
| dc.identifier.uri | http://hdl.handle.net/10400.22/9519 | |
| dc.language.iso | eng | pt_PT |
| dc.relation | Embedded Multi-Core Systems for Mixed Criticality Applications in Dynamic and Changeable Real-Time Environments | |
| dc.relation.ispartofseries | INDIN;2016 | |
| dc.subject | IEC 61499 | pt_PT |
| dc.subject | Industrial automation | pt_PT |
| dc.title | Contract Based Verification of IEC 61499 | pt_PT |
| dc.type | conference object | |
| dspace.entity.type | Publication | |
| oaire.awardTitle | Embedded Multi-Core Systems for Mixed Criticality Applications in Dynamic and Changeable Real-Time Environments | |
| oaire.awardURI | info:eu-repo/grantAgreement/EC/FP7/621429/EU | |
| oaire.citation.conferencePlace | 18 to 21, Jul, 2016, Factory Automation. Poitiers, France | pt_PT |
| oaire.citation.title | 14th International Conference on Industrial Informatics | pt_PT |
| oaire.fundingStream | FP7 | |
| person.familyName | Pinho | |
| person.givenName | Luis Miguel | |
| person.identifier.ciencia-id | 8112-2108-F3B2 | |
| person.identifier.orcid | 0000-0001-6888-1340 | |
| person.identifier.rid | M-3416-2013 | |
| person.identifier.scopus-author-id | 6602594556 | |
| project.funder.identifier | http://doi.org/10.13039/501100008530 | |
| project.funder.name | European Commission | |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | conferenceObject | pt_PT |
| relation.isAuthorOfPublication | fd791145-af93-47d9-bbe8-647a326d2f39 | |
| relation.isAuthorOfPublication.latestForDiscovery | fd791145-af93-47d9-bbe8-647a326d2f39 | |
| relation.isProjectOfPublication | c05ca6d0-eb47-46e6-93ae-3218a8c9ee48 | |
| relation.isProjectOfPublication.latestForDiscovery | c05ca6d0-eb47-46e6-93ae-3218a8c9ee48 |