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

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorBuzhinskii, Igor
dc.contributor.departmentSähkötekniikan ja automaation laitosfi
dc.contributor.departmentDepartment of Electrical Engineering and Automationen
dc.contributor.schoolSähkötekniikan korkeakoulufi
dc.contributor.schoolSchool of Electrical Engineeringen
dc.contributor.supervisorVyatkin, Valeriy, Prof., Aalto University, Department of Electrical Engineering and Automation, Finland
dc.contributor.supervisorShalyto, Anatoly, Prof., ITMO University, Russia
dc.date.accessioned2019-06-07T09:01:14Z
dc.date.available2019-06-07T09:01:14Z
dc.date.defence2019-06-28
dc.date.issued2019
dc.descriptionThis doctoral thesis was conducted under a convention for the joint supervision of thesis at Aalto University (Finland) and ITMO University (Russia)en
dc.description.abstractMission-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.extent102 + app. 90
dc.format.mimetypeapplication/pdfen
dc.identifier.isbn978-952-60-8574-6 (electronic)
dc.identifier.isbn978-952-60-8573-9 (printed)
dc.identifier.issn1799-4942 (electronic)
dc.identifier.issn1799-4934 (printed)
dc.identifier.issn1799-4934 (ISSN-L)
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/38452
dc.identifier.urnURN:ISBN:978-952-60-8574-6
dc.language.isoenen
dc.opnLesage, Jean-Jacques, Prof., ENS Paris-Saclay, France
dc.publisherAalto Universityen
dc.publisherAalto-yliopistofi
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.relation.ispartofseriesAalto University publication series DOCTORAL DISSERTATIONSen
dc.relation.ispartofseries101/2019
dc.revRoop, Partha, Prof., University of Auckland, New Zealand
dc.revProvost, Julien, Prof., Technical University of Munich, Germany
dc.subject.keywordformal verificationen
dc.subject.keywordmodel checkingen
dc.subject.keywordformal synthesisen
dc.subject.keywordclosed-loop modelingen
dc.subject.keywordsafety-critical systemsen
dc.subject.otherElectrical engineeringen
dc.titleCombined use of formal methods for reliability assurance of software for safety-critical systemsen
dc.typeG5 Artikkeliväitöskirjafi
dc.type.dcmitypetexten
dc.type.ontasotDoctoral dissertation (article-based)en
dc.type.ontasotVäitöskirja (artikkeli)fi
local.aalto.acrisexportstatuschecked 2019-07-02_1310
local.aalto.archiveyes
local.aalto.formfolder2019_06_06_klo_16_56
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
isbn9789526085746.pdf
Size:
1.1 MB
Format:
Adobe Portable Document Format