并发系统的模型和自动验证

AUTOMATIC VERIFICATION OF CONCURRENT SYSTEMS USING TEMPORAL LOGIC

时序逻辑可以很好地应用于描述和验证并发系统的动态特性。AMC(Model Checker for Asynchronous concurrent systems)代替传统的从公理出发的形式推导,将并发系统描述转换为系统状态模型,然后应用模型实现对系统时序特性的自动验证。AMC能处理一般形式的合理性问题,并能对大的并发系统进行层次结构模型验证。

Temporal logic has been extensively investigated for specifying and proving properties of concurrent systems. Instead of the traditional verification technique using axioms and inference rules, the model checker for asynchronous concurrent systems (AMC) is designed to mechanically determine if a. system meets its temporal specifications.