PS系统的一种精确语义描述

摘要：

规约模式系统SPS是根据性质的语义抽象而成的描述程序性质的表达模式,既能方便程序员使用,又有对应的时序逻辑表达式.但是,它现有的语义描述不够精确.首先介绍了规约模式系统及其现有的语义,并用它描述了实例的性质,接着采用模型检测工具SPIN验证了该系统表达的性质,通过对比验证结果及现有语义,给出了系统精确的语义描述.

关键词：规约模式系统、程序性质、形式化方法、SPIN

所属期刊栏目：35

分类号：TP3;TN9

资助基金：重庆市自然科学基金2006BB2259;江苏省高校自然科学基金08KJB520010

在线出版日期：2009-01-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：284-287