| |
Click here for full text:
Model checking Demos using PBI : A Simple Approach
Hayman, Jonathan
HPL-2003-196
Keyword(s): model checking, demos; bunched implications; concurrency
Abstract: '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
Back to Index
|
printable version
