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

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.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.identifier.otherIR/2005/23
dc.identifier.urihttp://hdl.handle.net/2086/46
dc.language.isoenen
dc.relation.ispartofseriesSTRLen
dc.relation.ispartofseries1995-3en
dc.researchgroupSoftware Technology Research Laboratory (STRL)
dc.titleCompositional verification and specification of refinement for reactive systems in a dense time temporal logicen
dc.typeThesisen

Files

Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
root.pdf
Size:
1000.13 KB
Format:
Adobe Portable Document Format
Description:
Main article text
No Thumbnail Available
Name:
root.ps
Size:
1.29 MB
Format:
Postscript Files
Description:
Main article in postscript
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.78 KB
Format:
Item-specific license agreed upon to submission
Description: