Verifying Semantic Relations in SPIN

  1. (PDF, 323 KB)
AuthorSearch for:
Proceedings titleINRS-Telecommunications
ConferenceProceedings of the First SPIN Workshop, October 16, 1995., Verdun, Québec
AbstractSpin is a general verification tool for proving correctness properties of concurrent/distributed systems specified in the CSP-like modeling language Promela. We extended Promela's syntax to differentiate between external and internal transitions in a given model and the Spin tool with the ability to verify a particular class of semantic relations between two Promela models. This document describes this extension and gives an overview of the relevant theoretical foundations.
Publication date
AffiliationNRC Institute for Information Technology; National Research Council Canada
Peer reviewedNo
NRC number39182
NPARC number5765355
Export citationExport as RIS
Report a correctionReport a correction
Record identifiercc0c86b1-43f4-4114-ad96-0cc8db85493e
Record created2009-03-29
Record modified2016-05-09
Bookmark and share
  • Share this page with Facebook (Opens in a new window)
  • Share this page with Twitter (Opens in a new window)
  • Share this page with Google+ (Opens in a new window)
  • Share this page with Delicious (Opens in a new window)
Date modified: