欢迎访问中国科学院大学学报,今天是

中国科学院大学学报 ›› 2004, Vol. 21 ›› Issue (4): 501-511.DOI: 10.7523/j.issn.2095-6134.2004.4.012

• • 上一篇    下一篇

具有中断算子进程的语义动作精化的操作语义(英文)

袁红, 吴尽昭   

  1. 中国科学院成都计算机应用研究所, 成都 610041
  • 收稿日期:2003-05-12 修回日期:2004-04-12 发布日期:2004-07-10

Operational Semantics Modelling SemanticAction Refinement for Processes with Interrupt

YUAN Hong, WU Jin-Zhao   

  1. Chengdu Institute of Computer Applications, Chinese Academy of Sciences, Chengdu 610040, China
  • Received:2003-05-12 Revised:2004-04-12 Published:2004-07-10

摘要:

以SOS规则的方式定义了含中断和精化算子的进程代数LOTOS的操作语义,使得这一操作语义与指称语义相对应,即 :由指称语义导出的传输系统和操作语义定义的传输系统双模拟.操作语义的基本思想是 :重新命名被精化的动作并且使所有与之相关的选择都被激发.

关键词: 动作精化, 指称语义, 操作语义, 传输系统

Abstract:

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

Key words: action refinement, enotat ional semantics, operational semantics, transition system

中图分类号: