| 摘要: |
| 本文讨论了用于并发系统规范的2种方法；时序逻辑方法和状态自动机方法．由此，本文提出了一种新的规范形式——公平转换系统规范FTSS(fair transition system specification)．此规范方法集成了状态自动机方法和时序逻辑方法的优点，改进了时序逻辑方法通常较复杂、不易理解，特别是它不能用于描述并发系统的局部性质等不足．进一步对FTSS中的每一部分进行了讨论，得到结论；FTSS是机器封闭的，规范过程是相容的且是完全的．一个有丢失传输协议的例子表明作者的方法具有简单、直观、易于理解和便于使用等特点．最后给出了FTSS的一些应用．它为程序验证和并发系统的逐步求精提供了一个统一的框架，已成功地应用于程序验证中． |
| 关键词: 并发系统，规范，时序逻辑，状态自动机，公平转换系统规范，有丢失传输协议,程序验证，并发系统的逐步求精． |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家教委博士点基金,江苏省应用基础基金. |
|
| FAIR TRANSITIoN SYSTEM SPECIFICATION AND ITS APPLICATIONS |
|
Jia Guoping,Zheng Guoliang
|
| 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． |
| Key words: Concurrent system,specification,temporal logic,state machine,fair transi-tion system specification,lossy—transmission protocol,program verification,step—wise refinement of concurrent systems． |
