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

计算机科学 ›› 2008, Vol. 35 ›› Issue (10): 284-287.

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

戎玫

暨南大学深圳旅游学院,深圳518053

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
基金项目：重庆市自然科学基金（2006BB2259）,江苏省高校自然科学基金（08KJB520010）.

RONG Mei （Shenzhen Tourism College,Jinan University,Shenzhen 518053,China）

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

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

Abstract: Specification patterns system is a pattern system, which is abstracted from program properties according to property＇s semantic. It is used to describe program properties. Programmers can easily use it. And it has corresponding LTL formula. At present, it

Key words: SPS, Program properties,Formal method,SPIN

戎玫. SPS系统的一种精确语义描述[J]. 计算机科学, 2008, 35(10): 284-287. https://doi.org/

RONG Mei （Shenzhen Tourism College,Jinan University,Shenzhen 518053,China）. [J]. Computer Science, 2008, 35(10): 284-287. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed