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.