Разработка формальных требований к поведению распределенных программных систем

Developing formal temporal requirements to distributed program systems

Article's language
English
Abstract
Developing temporal requirements to distributed program systems an engineer should determine and systemize event sequences caused by system processes interleaving. A number of such sequences grow exponentially that makes the requirement development procedure nontrivial. This is why engineers prefer not to construct or construct elementary formal requirements. As result powerful formal verification methods become unavailable or some important properties of distributed systems leaved unexpressed. While it is well-known, that development of formal requirement even without verification improves an quality of a distributed system structure and functions. In this paper we suggest a method for formal temporal systems development which is easy-to-use. The method is based on scalable patterns of linear temporal logic formulas. Using this method we developed formal temporal requirements to a practical program control system (a vehicle power supply control system). Verifying the requirements with the model checking method we found 3 critical errors that were missed by developers of the vehicle power supply control system during design and testing.
DOI
10.31144/si.2307-6410.2016.n8.p21-32
Pages
21-32
File
shoshmina.pdf131.97 KB
Number