公平转换系统规范及其应用*
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

本文研究得到国家教委博士点基金,江苏省应用基础基金.


FAIR TRANSITIoN SYSTEM SPECIFICATION AND ITS APPLICATIONS
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    本文讨论了用于并发系统规范的2种方法;时序逻辑方法和状态自动机方法.由此,本文提出了一种新的规范形式——公平转换系统规范FTSS(fair transition system specification).此规范方法集成了状态自动机方法和时序逻辑方法的优点,改进了时序逻辑方法通常较复杂、不易理解,特别是它不能用于描述并发系统的局部性质等不足.进一步对FTSS中的每一部分进行了讨论,得到结论;FTSS是机器封闭的,规范过程是相容的且是完全的.一个有丢失传输协议的例子表明作者的方法具有简单、直观、易于理解和便于使用等特点.最后给出了FTSS的一些应用.它为程序验证和并发系统的逐步求精提供了一个统一的框架,已成功地应用于程序验证中.

    Abstract:

    This paper discusses two approaches to the specification of concurrent sys- terns:temporal logic approach and state machine approach.As a result of this discussion, the authors propose a new kind of formalisms of specification:fair transition system speci- fication(FTSS).This specification approach combines the best features of temporal logic and state machine methods and revises these drawbacks that temporal logic approach USU-ally is complicated and not easy to understand,especially,it fails to be used for "local"properties of concurrent systems.The authors further consider each component of FTSS and get conclusions that FTSS is machine closed and the specification process is consistent and complete.An example of a lossy—transmission protocol shows that the presented ap-proach is simple and easy to understand and to use.At the end of the paper,some applica-tions of FTSS are given.The approach provides a unified framework for program verifics-tion and step—wise refinement of concurrent systems.It has been successfully applied to program verification.

    参考文献
    相似文献
    引证文献
引用本文

贾国平,郑国梁.公平转换系统规范及其应用*.软件学报,1996,7(zk):358-366

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:1995-09-25
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号