Model construction for hybrid implicit specifications/ by Ole Hogh Jensen, Christian Jeppesen, Jarl Tuxen Lang.
Series: Report (Aalborg universitetscenter. Afdeling for matematik og datalogi) ; R 94-2012.Publication details: Aalborg, Denmark: University of Aalborg, Institute for Electronic Systems, Dept. of Mathematics and Computer Science, [1994].Description: viii, 150 p.: ill.; 24 cmSubject(s): Dissertation note: Thesis (M.S.)--Aalborg University, 1994. Summary: Abstract: "Top-down design of a reactive system, such as a computer program, can be viewed as a stepwise refinement of a specification. In order to ensure that the specification is indeed a correct description of the desired system, it is advantageous to be able to synthesize (perhaps automatically) prototypes from specifications. This thesis considers model construction, i.e. synthesis of prototypes, for hybrid implicit specifications of the form C(P₁ ..., P[subscript n];G₁ ..., G[subscript m]) sat F asserting that the process C(P₁ ..., P[subscript n];Q₁ ..., Q[subscript m]) satisfies the specification F whenever the process Q[subscript i] satisfies the specification G[subscript i] for 1 [<or =] i [<or =] m. We offer the theoretical development of a tableau-like method for constructing the processes P₁ ..., P[subscript n] (as labelled transition systems) when C is given as a context of process algebra (such as CCS), and F is given as a formula of Hennessy-Milner Logic with maximal recursion. Furthermore, we report on a prototype implementation of a model construction tool based on the presented theory."| Item type | Current library | Collection | Call number | Copy number | Status | Date due | Barcode |
|---|---|---|---|---|---|---|---|
Thesis
|
Castorina Estantes Abertas (Open Shelves) | Teses (Thesis) | 1 | Available | 39063000274053 |
Cover title.
"March 1994."
Thesis (M.S.)--Aalborg University, 1994.
Includes bibliographical references.
Abstract: "Top-down design of a reactive system, such as a computer program, can be viewed as a stepwise refinement of a specification. In order to ensure that the specification is indeed a correct description of the desired system, it is advantageous to be able to synthesize (perhaps automatically) prototypes from specifications. This thesis considers model construction, i.e. synthesis of prototypes, for hybrid implicit specifications of the form C(P₁ ..., P[subscript n];G₁ ..., G[subscript m]) sat F asserting that the process C(P₁ ..., P[subscript n];Q₁ ..., Q[subscript m]) satisfies the specification F whenever the process Q[subscript i] satisfies the specification G[subscript i] for 1 [<or =] i [<or =] m. We offer the theoretical development of a tableau-like method for constructing the processes P₁ ..., P[subscript n] (as labelled transition systems) when C is given as a context of process algebra (such as CCS), and F is given as a formula of Hennessy-Milner Logic with maximal recursion. Furthermore, we report on a prototype implementation of a model construction tool based on the presented theory."
There are no comments on this title.