Show simple item record

dc.contributor.authorCau, A. (Antonio)
dc.date.accessioned2005-09-05T19:46:29Z
dc.date.available2005-09-05T19:46:29Z
dc.date.issued2005-09-05T19:46:29Z
dc.identifier.otherIR/2005/23
dc.identifier.urihttp://hdl.handle.net/2086/46
dc.descriptionDissertation zur Erlangung des Doktorgrades der Technischen Fakultat der Christian-Albrechts-Universitat zu Kiel. Originally available in German?en
dc.description.abstractThis 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.extent1356968 bytesen
dc.format.mimetypeapplication/pdf
dc.language.isoenen
dc.relation.ispartofseriesSTRLen
dc.relation.ispartofseries1995-3en
dc.titleCompositional verification and specification of refinement for reactive systems in a dense time temporal logicen
dc.typeThesisen
dc.researchgroupSoftware Technology Research Laboratory (STRL)


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record