Editorial
Unlike the previous articles by Professor Anatoly Shalyto, this is not a journalistic text. It is intended for professionals in the field of software development. This, however, is not about programming, but about more important, subtle and complex work – the effective design of process control systems, ensuring the correctness of the developed product, and the convenience of its maintenance. Maxim Buzdalov, one of the author’s students, Candidate of Technical Sciences, World Champion in Programming (ICPC) as part of the ITMO team, reviewed the article, giving it a positive review.
Under Verification [1] usually refers to checking an informally constructed application program against a formal specification. This process must be repeated for each newly created application program.
It is believed that verification allows you to establish that “we created the product the way we intended to make it”, and validation confirms that “we created the right product.” Therefore, in the general case, an error is not only something that is established formally (by verification), but also informally (by validation). In this case, testing can be considered as a kind of validation, which is carried out in order to determine whether the behavior of the system corresponds to its expected behavior on the final set of tests.
If a formal specification becomes executable, then instead of verifying each of the application programs generated by it, verification is carried out only once – the application program generator program is verified once. If the qualifications of the creators of the generator for its verification are not enough, then it can be validated – checked, perhaps statistically, for the correctness of building application programs with its help.
So if the specification is executable and the generator program is verified, or at least validated, then the problem of verification of application programs disappears!
There are two options (cases) for creating programs: in the presence of a formal specification at the beginning of the design and in its absence at this stage of the system creation.
In the first case, with the approach under consideration, it is possible to verify not the program itself, but the informally constructed model by which it is generated. When using automatic programming, such a model is a system of transition graphs of finite automata. This model for the program is the executable specification, which must be verified against the original specification, as it is assumed to exist. In this case, we can talk about “verification of the automaton model”.
However, a formal specification at the beginning of the design is extremely rare: either for very simple objects, or for incredibly important objects.
In work [2] such a simple object is an alarm clock, the behavior of the control system of which is described by only one automaton transition graph with only three states. The authors show that even such a model is difficult to verify: it was successfully executed for the initially constructed formal specification in the form of a certain number of temporal rules, but when changes were made to the specification – the number of temporal rules was increased, an error was found in the transition graph. Let us pay attention to the fact that in this case the formal specification is built informally, it is not verified, and its changes are related to validation.
For very responsible objects in the presence of unique specialistsas was the case with the automation of the London Underground, verification is carried out with further validation throughout the entire life cycle.
In the second case, when designing control systems for complex technological objects, there is no formal specification at the beginning of the design. From the Customer, at best, you can get only scattered information and knowledge about how the system should work, and usually in the main mode. For various reasons, the Customer cannot describe all the subtleties of the work at the early stages of creating the system.
Some knowledge (perhaps basic) is added by the Developer of the control system, if he is an experienced specialist. According to the information from the Customer and the Developer, you can informally write a program, and then we will be left without a formal specification, or you can informally build a formal specification (fix the above information in some formal language). The first way is traditional [3]but, in my opinion, it is a dead end, so I suggest using the second way with generating a program according to an informally constructed formal specification.
This raises the question of what mathematical apparatus to use in its construction. As noted above, for the considered class of systems, I propose to use the system of transition graphs of finite automata as a formal specification. According to this specification, the program must be built (generated) formally and isomorphically. At the same time, it will not only comply with the specification, but will also be “outwardly similar” to it.
The correctness of such a specification requires verification – validation. “Correctness” is an informal concept, it should “arrange”: the equipment (with the currently existing specification, its accidents and breakdowns should not occur) and all specialists involved in the creation of the system, who do everything possible to make the equipment “comfortable” in the future “.
Any test can be considered as a validation to confirm the correctness of the specification and refine it if necessary. Refinement is provided by making appropriate changes to the system of transition graphs that exists at that time. However, since errors may be introduced during the adjustment, it is necessary to carry out tests again after this, etc.
The operation of the system (especially experienced) can also be considered as a refinement of the specification. Only at the time of the decommissioning of the system, if it existed in a single copy, can we consider that, finally, the specification has been received, which is final, and then on the condition that a modification of the system will not be created on its basis. Thus, at each moment of time there is a formal specification, which at any stage of validation may require adjustment.
It follows from the foregoing that the specification of the formal specification of the control system is carried out by validation throughout its entire life cycle, and when creating its modification, and after its completion.
Validation means, in particular, include testing, as well as checking the fulfillment of temporal properties used in traditional verification. [3].
I draw your attention to the fact that in the proposed approach, the transition graph system is not only an executable specification, but also a programming language. At the same time, after the validation of the specification, verification or even validation of the program built according to it is not required!
The proposed approach was used in the works [4, 5].
It follows from the foregoing that, at one time, having called the book “Verification of automaton programs” [6], we acted insufficiently correctly, since already when writing it, we assumed that automaton programs are built not heuristically, but formally according to the specification. Therefore, it should have been called either “Verification of Automaton Models” or “Validation of Automaton Specifications”, the second name being much more practical.
Based on the foregoing, the expression “Verification of automaton programs” can be used as jargon for the concept of “Validation of automaton specifications”, as well as the well-known expression “Minimization of Boolean functions”, which is commonly used instead of the concept of “Minimization of Boolean formulas” [7]. The latter is due to the fact that a Boolean function (truth table), if it essentially depends on all its variables, cannot be minimized – in contrast to a Boolean formula, for which this is possible in most cases.
Literature
