Verifying Semantic Relations in SPIN

Download
  1. (PDF, 323 KB)
AuthorSearch for:
TypeArticle
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
LanguageEnglish
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)