Modeling and Verifying Concurrent Programs with Finite Chu Spaces
杜旭涛, 邢春晓, 周立柱 · Acta Scientiarum Naturalium Universitatis Sunyatseni · 2010
有限 Chu 空格为建模和并发的节目的确认被建议。以便为不仅典型并发的行为而且现代例外处理和同步机制建模，我们从一个实际观点设计 Chu 空格的充实的进程代数学。为了说明有限 Chu 空格和过程代数学的力量，当提炼离开语言特定的细节时，一种想象的并发的程序语言(ICL ) 被设计。ICL 的 denotational 语义用有限 Chu 空格和充实的进程代数学被介绍。自从小心地设计的操作员做了许多这个工作，估价功能是相当直接的。充实的进程代数学也被用作说明语言 Chu 空格，过程代数学的性质能与被指定。确认算法被介绍，他们的时间复杂性讨论了。