Compositional verification and specification of refinement for reactive systems in a dense time temporal logic

Abstract

This thesis introduces a compostitional dense time temporal logic for the compositions and refinement of reactive systems. A reactive system is specified by a pair consisting of a machine and a condition on the computations of this machine. In order to compose reactive systems, each step in a computation has additionally composition information such as “this is a system step”, or “this is an environment step” or “this is a communication step”. By defining a merge operator that merges two steps into one step compostionality is achieved. Because a dense time temporal logic is used refinement can be expressed easily in this logic. Existing proof rules for refinement are reformulated in our formalism. The notion of relative refinement is introduced to handle refinement of systems that only under certain conditions are considered to be correct refinements. The proof rules for “normal” refinement are extended to handle relative refinement of systems. Relative refinement is used to formalize Dijkstra’s development strategy for the solution of the readers/writers problem and to formalize a development strategy for certain fault tolerant systems. This development strategy is applied to the development of a fault tolerant storage system.