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

De Montfort University Open Research Archive

Show simple item record Cau, A. (Antonio) 2005-09-05T19:46:29Z 2005-09-05T19:46:29Z 2005-09-05T19:46:29Z
dc.identifier.other IR/2005/23
dc.description Dissertation zur Erlangung des Doktorgrades der Technischen Fakultat der Christian-Albrechts-Universitat zu Kiel. Originally available in German? en
dc.description.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. en
dc.format.extent 1024136 bytes
dc.format.extent 1356968 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1995-3 en
dc.title Compositional verification and specification of refinement for reactive systems in a dense time temporal logic en
dc.type Thesis en
dc.researchgroup Software Technology Research Laboratory (STRL)

Files in this item

This item appears in the following Collection(s)

Show simple item record