|
Fig. 1. General flow of control algorithm verification based on the Model Checking approach
|
A verification technique for control algorithms in complex technical systems was introduced (Fig. 1). The technique is based on the Model Checking approach and allow to process the informal technical requirements into executable algorithm specification (in Reflex language) and a list of requirements formalized in linear temporal logic (LTL) rules.
In a cycle, based on the current requirement, the formal algorithm specification is reduced to module M expressed in a format suitable for formal verification (Kripke structure). Automated verification of the module is then performed (M is checked against the property φ). In case of no error the next cycle is executed to check the next requirement in the list. In case of an error, the process is stopped to analyze and correct the error.
The conceptual framework of process-oriented programming (the hyperprocess model) is used for test specification. This model is supported by both linguistic (Relfex programming language) and instrumental (Relfex language translator and IDE based on Notepad++ editor) tools. Sample task impementations show that Reflex language, apart from actual specification of control algorithms, can be utilized to specify test models. Regular programming tools provide automatic transformation of the algorithm specifications into executable code. Unlike other Model Checking techniques this generated code does not require any further implementation or debugging expenses.
Publications
1. Lyah T., Zyubin V. Applying virtual control object concepts to industrial control and automation tasks // Ershov Informatics Conference: Workshop On Science Intensive Applied Software. June 24–27, 2014, St. Petersburg, Russia. Proceedings. P. 57–64.
2. Lyah T. Testing control algorithms with virtual control objects and formal methods // In proceedings of 53-rd International Scientific Student Conference: Information technology, Novosibirsk, April 11-17, 2015, p. 114.
|
