%0 Journal Article
%T 公平转换系统规范及其应用*
%A 贾国平？
%A 郑国梁？
%J 软件学报
%P 358-366
%D 1996
%X 本文讨论了用于并发系统规范的2种方法；时序逻辑方法和状态自动机方法．由此，本文提出了一种新的规范形式——公平转换系统规范ftss(fairtransitionsystemspecification)．此规范方法集成了状态自动机方法和时序逻辑方法的优点，改进了时序逻辑方法通常较复杂、不易理解，特别是它不能用于描述并发系统的局部性质等不足．进一步对ftss中的每一部分进行了讨论，得到结论；ftss是机器封闭的，规范过程是相容的且是完全的．一个有丢失传输协议的例子表明作者的方法具有简单、直观、易于理解和便于使用等特点．最后给出了ftss的一些应用．它为程序验证和并发系统的逐步求精提供了一个统一的框架，已成功地应用于程序验证中．
%K 并发系统
%K 规范
%K 时序逻辑
%K 状态自动机
%K 公平转换系统规范
%K 有丢失传输协议
%K 程序验证
%K 并发系统的逐步求精．
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=1996s151&flag=1