Combined use of formal methods for reliability assurance of software for safety-critical systems

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Buzhinskii, Igor
dc.date.accessioned 2019-06-07T09:01:14Z
dc.date.available 2019-06-07T09:01:14Z
dc.date.issued 2019
dc.identifier.isbn 978-952-60-8574-6 (electronic)
dc.identifier.isbn 978-952-60-8573-9 (printed)
dc.identifier.issn 1799-4942 (electronic)
dc.identifier.issn 1799-4934 (printed)
dc.identifier.issn 1799-4934 (ISSN-L)
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/38452
dc.description This doctoral thesis was conducted under a convention for the joint supervision of thesis at Aalto University (Finland) and ITMO University (Russia) en
dc.description.abstract Mission-critical systems play an important role in our lives by regulating the production processes of consumer goods and controlling transportation and power plants. Recently, these systems have become more complex due to the advent of Industry 4.0, which has brought about the Internet of Things as well as smart homes and factories. At the same time, automation systems must be correct to fulfill their purpose and safe to interact with humans and prevent disasters from happening. To successfully ensure reliability (correctness and safety), in addition to conventional approaches of testing and simulation, formal methods should be applied. These methods, including model checking and formal model synthesis, increase the safety of systems by means of exhaustive analysis. This thesis considers combined use of three different types of formal methods: verification, synthesis and testing, and as a result it proposes several automated formal reliability assurance approaches for control software. Specifically, it examines three sub-areas of combined use of formal methods. Firstly, the thesis proposes model checking based methods to generate finite-state models of plants and control software. Secondly, it considers the use of generated models in open-loop and closed-loop model checking of automation systems. Thirdly, it explores how model checking can be used to test closed-loop systems. The following key results were obtained: (1) two SAT solver based methods were developed to generate plant and controller finite-state models with the minimum possible number of states; (2) new practical plant model generation methods were developed that are more scalable than the ones known before and support plant modularity; (3) a comprehensive verification methodology was proposed to verify manually created formal models by comparing them with formally synthesized models; and (4) a closed-loop verification approach was proposed that combines testing and model checking. From a practical point of view, these results extend the capabilities of modern formal methods to assure the reliability of mission-critical systems. In addition, the approaches proposed in the thesis increase the level of automation of this process. The practical applicability of the developed approaches was shown, in particular for verification of nuclear instrumentation and control systems. en
dc.format.extent 102 + app. 90
dc.format.mimetype application/pdf en
dc.language.iso en en
dc.publisher Aalto University en
dc.publisher Aalto-yliopisto fi
dc.relation.ispartofseries Aalto University publication series DOCTORAL DISSERTATIONS en
dc.relation.ispartofseries 101/2019
dc.relation.haspart [Publication 1]: Igor Buzhinsky, Valeriy Vyatkin. Automatic inference of finite-state plant models from traces and temporal properties. IEEE Transactions on Industrial Informatics, pp. 1521–1530, 2017, vol. 13, no. 4. Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201906033498. DOI: 10.1109/TII.2017.2670146
dc.relation.haspart [Publication 2]: Vladimir Ulyantsev, Igor Buzhinsky, Anatoly Shalyto. Exact finite-state machine identification from scenarios and temporal properties. International Journal on Software Tools for Technology Transfer, pp. 35–55, 2018, vol. 20, no. 1. Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201906033388. DOI: 10.1007/s10009-016-0442-1
dc.relation.haspart [Publication 3]: Igor Buzhinsky, Antti Pakonen, Valeriy Vyatkin. Scalable methods of discrete plant model generation for closed-loop model checking. In 43rd Annual Conference of the IEEE Industrial Electronics Society IECON), October 29 – November 1, 2017, Beijing, China, pp. 5483–5488. Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201906033447. DOI: 10.1109/IECON.2017.8216949
dc.relation.haspart [Publication 4]: Igor Buzhinsky, Valeriy Vyatkin. Modular plant model synthesis from behavior traces and temporal properties. In 22nd IEEE Conference on Emerging Technologies & Factory Automation (ETFA), September 12–15, 2017, Limassol, Cyprus. Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201906033459. DOI: 10.1109/ETFA.2017.8247578
dc.relation.haspart [Publication 5]: Igor Buzhinsky, Antti Pakonen, Valeriy Vyatkin. Synthesis-aided reliability assurance of basic block models for model checking purposes. In 27th IEEE International Symposium on Industrial Electronics (ISIE), June 13–15, 2018, Cairns, Australia, pp. 669–674. Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201906033484. DOI: 10.1109/ISIE.2018.8433793
dc.relation.haspart [Publication 6]: Igor Buzhinsky, Valeriy Vyatkin. Testing automation systems by means of model checking. In 22nd IEEE Conference on Emerging Technologies & Factory Automation (ETFA), September 12–15, 2017, Limassol, Cyprus.Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201906033467. DOI: 10.1109/ETFA.2017.8247579
dc.relation.haspart [Publication 7]: Igor Buzhinsky, Valeriy Vyatkin. Combining closed-loop test generation and execution by means of model checking. Submitted to International Journal on Software Tools for Technology Transfer, November 2018.
dc.subject.other Electrical engineering en
dc.title Combined use of formal methods for reliability assurance of software for safety-critical systems en
dc.type G5 Artikkeliväitöskirja fi
dc.contributor.school Sähkötekniikan korkeakoulu fi
dc.contributor.school School of Electrical Engineering en
dc.contributor.department Sähkötekniikan ja automaation laitos fi
dc.contributor.department Department of Electrical Engineering and Automation en
dc.subject.keyword formal verification en
dc.subject.keyword model checking en
dc.subject.keyword formal synthesis en
dc.subject.keyword closed-loop modeling en
dc.subject.keyword safety-critical systems en
dc.identifier.urn URN:ISBN:978-952-60-8574-6
dc.type.dcmitype text en
dc.type.ontasot Doctoral dissertation (article-based) en
dc.type.ontasot Väitöskirja (artikkeli) fi
dc.contributor.supervisor Vyatkin, Valeriy, Prof., Aalto University, Department of Electrical Engineering and Automation, Finland
dc.contributor.supervisor Shalyto, Anatoly, Prof., ITMO University, Russia
dc.opn Lesage, Jean-Jacques, Prof., ENS Paris-Saclay, France
dc.rev Roop, Partha, Prof., University of Auckland, New Zealand
dc.rev Provost, Julien, Prof., Technical University of Munich, Germany
dc.date.defence 2019-06-28
local.aalto.acrisexportstatus checked 2019-07-02_1310


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse