Scalable methods of discrete plant model generation for closed-loop model checking

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Buzhinskii, Igor
dc.contributor.author Pakonen, Antti
dc.contributor.author Vyatkin, Valeriy
dc.date.accessioned 2019-06-03T14:17:59Z
dc.date.available 2019-06-03T14:17:59Z
dc.date.issued 2017-12-18
dc.identifier.citation Buzhinskii , I , Pakonen , A & Vyatkin , V 2017 , Scalable methods of discrete plant model generation for closed-loop model checking . in Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society . Proceedings of the Annual Conference of the IEEE Industrial Electronics Society , Institute of Electrical and Electronics Engineers , pp. 5483-5488 , Annual Conference of the IEEE Industrial Electronics Society , Beijing , China , 29/10/2017 . https://doi.org/10.1109/IECON.2017.8216949 en
dc.identifier.isbn 978-1-5386-1127-2
dc.identifier.issn 1553-572X
dc.identifier.other PURE UUID: c2c5d86f-dd94-4485-9d0c-3b096d0bf117
dc.identifier.other PURE ITEMURL: https://research.aalto.fi/en/publications/scalable-methods-of-discrete-plant-model-generation-for-closedloop-model-checking(c2c5d86f-dd94-4485-9d0c-3b096d0bf117).html
dc.identifier.other PURE FILEURL: https://research.aalto.fi/files/33889716/ELEC_Buzhinsky_etal_Scalable_Methods_of_Discrete_IECON_2017_accepted.pdf
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/38362
dc.description.abstract To facilitate correctness and safety of mission-critical automation systems, formal methods should be applied in addition to simulation and testing. One of such formal methods is model checking, which is capable of verifying complex requirements for the system's model. If both the controller and the controlled plant are formally modeled, then the variant of this technique called closed-loop model checking can be applied. Recently, a technique of automatic plant model generation has been proposed which is applicable in this scenario. This paper continues the work in this direction by presenting two plant model construction approaches which are much more scalable with respect to the previous one, and puts this work into a more practical context. The approaches are evaluated on a case study from the nuclear automation domain. en
dc.format.extent 6
dc.format.extent 5483-5488
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher IEEE
dc.relation.ispartof Annual Conference of the IEEE Industrial Electronics Society en
dc.relation.ispartofseries Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society en
dc.relation.ispartofseries Proceedings of the Annual Conference of the IEEE Industrial Electronics Society en
dc.rights openAccess en
dc.subject.other 113 Computer and information sciences en
dc.title Scalable methods of discrete plant model generation for closed-loop model checking en
dc.type A4 Artikkeli konferenssijulkaisussa fi
dc.description.version Peer reviewed en
dc.contributor.department Department of Electrical Engineering and Automation
dc.contributor.department VTT Technical Research Centre of Finland
dc.contributor.department Department of Electrical Engineering and Automation en
dc.subject.keyword model checking
dc.subject.keyword solid modeling
dc.subject.keyword automation
dc.subject.keyword computational modeling
dc.subject.keyword context modeling
dc.subject.keyword data models
dc.subject.keyword tools
dc.subject.keyword 113 Computer and information sciences
dc.identifier.urn URN:NBN:fi:aalto-201906033447
dc.identifier.doi 10.1109/IECON.2017.8216949
dc.type.version acceptedVersion


Files in this item

Files Size Format View

There are no open access files associated with this item.

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse