Panchenko T. Compositional Methods for Program Systems Specification and Verification

Specification and verification problems of pragmatically applied classes of program systems were researched by the means of composition methods in the thesis. Compositional models and languages for program systems with structured data specification were developed. Complex analysis and distribution of data structures and functions over them by abstraction levels was made. Representative completeness of nominate data of complex-nominative level was proved. Compositional methods for verification of special class systems, namely multi-instance program execution model in server environment with shared memory interleaving concurrency, were developed. Two types of partial correctness properties of programs in introduced compositional languages were formulated. Methodology of verification including method with linear complexity instead of exponential one was developed. Keywords: composition programming, composition nominative systems, program system specification, program verification, program models, execution model, properties proof, partial correctness, safety, parallel programming, interleaving concurrency, shared memory concurrency, invariant, transition system.