首页 | 本学科首页   官方微博 | 高级检索  
     

SPS系统的一种精确语义描述
引用本文:戎玫.SPS系统的一种精确语义描述[J].计算机科学,2008,35(10):284-287.
作者姓名:戎玫
作者单位:暨南大学深圳旅游学院,深圳518053
基金项目:重庆市自然科学基金(2006BB2259); 江苏省高校自然科学基金(08KJB520010)
摘    要:规约模式系统SPS是根据性质的语义抽象而成的描述程序性质的表达模式,既能方便程序员使用,又有对应的时序逻辑表达式。但是,它现有的语义描述不够精确。首先介绍了规约模式系统及其现有的语义,并用它描述了实例的性质,接着采用模型检测工具SPIN验证了该系统表达的性质,通过对比验证结果及现有语义,给出了系统精确的语义描述。

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

Exact Semantic of Specification Patterns System
RONG Mei.Exact Semantic of Specification Patterns System[J].Computer Science,2008,35(10):284-287.
Authors:RONG Mei
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,its semantic is inexplicit.In order to make it explicit,the article first introduces specification patterns system and its existing semantic,and describes an example's properties in it,then verifies properties expressed in the system by SPIN.Contrasting verifying r...
Keywords:SPS  Program properties  Formal method  SPIN  
本文献已被 CNKI 维普 等数据库收录!
点击此处可从《计算机科学》浏览原始摘要信息
点击此处可从《计算机科学》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号