• PDF / 124,534 Bytes
• 10 Pages / 594 x 792 pts Page_size
• 31 Downloads / 194 Views

DOWNLOAD

REPORT

---

CYBERNETICS PROGRAM VERIFICATION: STATE OF THE ART, PROBLEMS, AND RESULTS. I S. L. Kryvyia† and O. M. Maksymetsa‡

UDC 51.681.3

Abstract. An analytical survey of modern verification methods for sequential functional, reactive, and distributed systems is presented. The emphasis is on methods based on properties of abstract interpretation, transition systems, and Petri nets. Keywords: verification, abstract interpretation, transition system, Petri net, model checking.

This work is a continuation of the surveys that were initiated in [1, 2] and consider verification methods for procedural programs with the orientation toward the use of program dynamic logics (in particular, Hoare logic). The first part of the present publication describes a method of abstract interpretations of an analysis of semantic properties of sequential programs, and the second considers the mentioned methods and their applications oriented toward the verification of reactive and distributed systems. The choice of these directions is explained by the fact that it is these directions that are actively developed and put into practice in the field of verification at the present time. The semantic analysis of programs is based on the use of a program analyzer. Such an analyzer is understood to be a program whose input is a (possibly, annotated) program and that produces (at its output) answers to questions about program properties that take place throughout the execution of the program. As a result of the algorithmic unsolvability of the verification problem or because of a great complexity of the verification process, these answers will inevitably be partial, but they also always are very important. An approach to the verification problem is the method of abstract interpretations whose fundamentals are described in this work. 1. ABSTRACT INTERPRETATIONS Abstract interpretations were first introduced by F. Sintzoff [3] to automate program analysis processes and then were developed in [4–6] and [7, 8]. The main idea of abstract interpretations lies in finding restrictions (abstract by nature) on semantic structures of programs in order that tools of automatic proof of statements in logical languages and tools of computer algebra may be applied. In this sense, the method of abstract interpretations is placed into methods such as the analysis of data flows in programs, mixed computations, and program transformations during code generation [9]. Properties and their abstractions. Let Q be some set of objects (for example, program states, run traces, etc.), and let P be a set of objects having a certain property, i.e., P Î B (Q ) , where B (Q ) is the Boolean of the set Q. Since properties determine subsets from B (Q ), they form a complete Boolean lattice G = ( B (Q ), Í , Æ, Q , U , I , ' ) with respect to set-theoretic operations whose elements are partially ordered by the inclusion relation (Í) for sets. Recall that a complete lattice is understood to be an algebra R = (A ,{ô , ^ , a, ò , ó }), where A is a set partially ordered by a partial order r