Model checking Demos using PBI : A Simple Approach

Hayman, Jonathan

HP Development Company

关键词: model checking;    demos;    bunched implications;    concurrency;   

RP-ID  :  HPL-2003-196

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

'The application of a resource logic to the non- temporal analysis of processes acting on resources,' Hayman 2003. This defines the non-temporal semantics of simulation language, Demos, in order to be able to model processes acting on shared resources. It also defines the semantics of a logic, PBI, an extension of the Logic of Bunched Implications, to query these models. This document describes a simple model checker capable of checking a subclass of PBI formulae against Demos models. It is assumed that the reader is familiar with, 'The application of a resource logic to the non-temporal analysis of processes acting on resources,' Hayman 2003. 13 Pages