Specification and Compositional Verification of Real-Time Systems

摘要

The specification and verification of real time properties of computer programsare addressed. A metric temporal logic approach and a Hoare style formalism are investigated for use in a compositional axiomatization of several versions of the programming language. The development from non-compositional proof methods towards compositional proof systems for non-real time partial correctness of parallel programs is discussed. A compositional semantics for this language is defined and proofs for the two above mentioned approaches are formulated. An example of a watchdog timer illustrates how these two proof systems can be used to verify design steps during the process of top down program development. Both formalisms are then adapted to deal with program variables. The maximal parallelism assumption is used. The model is generalized to multiprogramming where several processes can be executed on a single processor. Scheduling is based on priorities which can be assigned to statements in the program. Both proof methods can be modified to prove properties of uniprocessor implementations.