000 | 02590n a2200325#a 4500 | ||
---|---|---|---|
001 | 21719 | ||
003 | P5A | ||
005 | 20221213140139.0 | ||
008 | 950209s1994 dk a tb 000 0 eng d | ||
035 | _aocm31960448 | ||
040 |
_aPMC _cPMC |
||
049 | _aP5AA | ||
090 | _atext | ||
100 | 1 |
_aJensen, Ole H. _923128 |
|
245 | 1 | 0 |
_aModel construction for hybrid implicit specifications/ _cby Ole Hogh Jensen, Christian Jeppesen, Jarl Tuxen Lang. |
260 |
_aAalborg, Denmark: _bUniversity of Aalborg, Institute for Electronic Systems, Dept. of Mathematics and Computer Science, _c[1994]. |
||
300 |
_aviii, 150 p.: _bill.; _c24 cm. |
||
490 | 1 |
_aReport / University of Aalborg. Institute for Electronic Systems. Dept. of Mathematics and Computer Science,; _x0106-0791; _vR 94-2012 |
|
500 | _aCover title. | ||
500 | _a"March 1994." | ||
502 | _aThesis (M.S.)--Aalborg University, 1994. | ||
504 | _aIncludes bibliographical references. | ||
520 | _aAbstract: "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." | ||
650 | 0 | 4 |
_aComputer programs. _937456 |
697 |
_aTeses Externas _924308 |
||
700 | 1 |
_aJeppesen, Christian _923129 |
|
700 | 1 |
_aLang, Jarl Tuxen _923130 |
|
830 | 0 |
_aReport (Aalborg universitetscenter. Afdeling for matematik og datalogi); _vR 94-2012. _929882 |
|
942 |
_2impa _cTHESIS |
||
999 |
_aJENSEN, Ole H.; JEPPESEN, Christian; LANG, Jarl Tuxen. <b> Model construction for hybrid implicit specifications. </b> Aalborg, Denmark, [1994]. viii, 150 p. Thesis (M.S.)--Aalborg University, 1994. _c21951 _d21951 |