Operational Semantics Modelling SemanticAction Refinement for Processes with Interrupt
Received date: 2003-05-12
Revised date: 2004-04-12
Online published: 2004-07-10
袁红 , 吴尽昭 . 具有中断算子进程的语义动作精化的操作语义(英文)[J]. 中国科学院大学学报, 2004 , 21(4) : 501 -511 . DOI: 10.7523/j.issn.2095-6134.2004.4.012
An operational semant ics of LOTOS including an interrupt and a ref inement operator is givenas SOS rules such that it corresponds to the denotational semantics, i. e. the transition system derivedfrom the denotational semantics is bisimilar to the transition system of the operational semantics.The ideabehind the operational semantics is that the refined action is renamed with a fresh name and all involvedchoices are triggered
[ 1 ] Robin Milner. Communicat ion and concurrency. Internat ional series in Computer Science. Prent ice Hall, 1989.
[ 2 ] Roberto Gorrieri, Arend Rensink. Action ref inement. In: J A Bergstra, A Ponse, S A Smolka, editors. Handbook of Process Algebra. North-Holland, 2001. 1047 ) 1147.
[ 3 ] Philippe Darondeau, Pierpaolo Degano. Refinement of actions in event structures and causal trees. Theoretical Computer Science, 1993,118: 21 )48.
[ 4 ] Rob van Glabbeek, Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Inf ormatica, 2001, 37: 221 ) 327.
[ 5 ] Walter Vogler. Failures semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 1991, 4: 139 ) 162[ 6 ] L Aceto, M Hennessy. Adding action refinement to a finit e process algebra. Inf ormati on and Computation, 1994, 115: 179) 247.
[ 7 ] Ursula Goltz, Roberto Gorrieri, Arend Rensink. Comparing syntactic and semantic act ion refinement. Inf ormati on and Computation, 1996 125:118 ) 143.
[ 8 ] Tommaso Bolognesi, Ed Brinksma. Introduct ion to the ISO specification language LOTOS. Computer Networks and ISDN Systems. 1987, 14: 25 )49.
[ 9 ] Rom Langerak. Transformat ions and Semant ics for LOTOS: [ PhD thesis]. Department of Comput er Science, University of Twente. 1992.
[ 10] Smson Abramsky, Achim Jung. Domain theory. In: Samson Abramsky, Dov M Gabbay, T S EMaibaum, editors. Handbook of Logic in ComputerScience, Oxford: Clarendon Press, 1994, Vol. 3: 1 ) 168.
[ 11] Harald Fecher, Mila Majster-Cederbaum, Jinzhao Wu. Bundle event structures: a revised cpo approach. Inf ormation Processing L etters,2002, 83:7 ) 12.
[ 12] Mila Majster-Cederbaum, Jinzhao Wu. Act ion ref inement for ture concurrent rea-l t ime. In: Proc. 7th IEEE int. Conf. on Engineering ofComplexComputer Systems. IEEE Comput er Society press, 2001. 58 ) 68.
[ 13] Mila Majster-Cederbaum, J Wu. Towards act ion refinement f or ture concurrent real time. Acta Inf ormati ca, 2003, 39: 1 ) 47.
[ 14] Pierpaolo Degano, Roberto Gorrieri. A causal operational semantics of action ref inement. Inf ormation and Computation. 1995, 122: 97)119.
[ 15] Arend Rensink. An even-t based SOS for a language with refinement. In: Structures in Concurrency Theory. Workshops in Computing, 1995.294 ) 309.
[ 16] Mario Bravett i, Robert o Gorrieri. Axiomatizing ST bisimulation for a process algebra with recursion and action refinement ( ext ended abstract). In:Electronic Not es in Theoreti cal Comput er Science. Elsevier Science Publishers, 1999. 27.
[ 17] Nadia Busi, Rob van Glabbeek, Roberto Gorrieri. Axiomat ising ST bisimulat ion equivalence. In: E R Olderog, edit or. Proceedings IFIP WorkingConf erence on Programming Concepts, Methods and Calculi. Elsevier Science, 1994. 169) 188.
[ 18] Mila Majster-Cederbaum,Markus Roggenbach.Transition systems from event strctures revisit ed. Inf ormation Processing Letters. 1998, 67: 119 ) 124
/
| 〈 |
|
〉 |
