Combined use of formal methods for reliability assurance of software for safety-critical systems
Loading...
URL
Journal Title
Journal ISSN
Volume Title
School of Electrical Engineering |
Doctoral thesis (article-based)
| Defence date: 2019-06-28
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
2019
Major/Subject
Mcode
Degree programme
Language
en
Pages
102 + app. 90
Series
Aalto University publication series DOCTORAL DISSERTATIONS, 101/2019
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.Description
This doctoral thesis was conducted under a convention for the joint supervision of thesis at Aalto University (Finland) and ITMO University (Russia)
Supervising professor
Vyatkin, Valeriy, Prof., Aalto University, Department of Electrical Engineering and Automation, FinlandShalyto, Anatoly, Prof., ITMO University, Russia
Keywords
formal verification, model checking, formal synthesis, closed-loop modeling, safety-critical systems
Other note
Parts
-
[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-201906033498DOI: 10.1109/TII.2017.2670146 View at publisher
-
[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-201906033388DOI: 10.1007/s10009-016-0442-1 View at publisher
-
[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-201906033447DOI: 10.1109/IECON.2017.8216949 View at publisher
-
[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-201906033459DOI: 10.1109/ETFA.2017.8247578 View at publisher
-
[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-201906033484DOI: 10.1109/ISIE.2018.8433793 View at publisher
-
[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 View at publisher
- [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.