Jump to content United States-English
HP.com Home Products and Services Support and Drivers Solutions How to Buy
» Contact HP

hp.com home


Technical Reports


printable version
» 

HP Labs

» Research
» News and events
» Technical reports
» About HP Labs
» Careers @ HP Labs
» Worldwide sites
» Downloads
Content starts here

 
Click here for full text: PDF

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

»Technical Reports

» 2009
» 2008
» 2007
» 2006
» 2005
» 2004
» 2003
» 2002
» 2001
» 2000
» 1990 - 1999

Heritage Technical Reports

» Compaq & DEC Technical Reports
» Tandem Technical Reports
Privacy statement Using this site means you accept its terms Feedback to HP Labs
© 2009 Hewlett-Packard Development Company, L.P.