Formal Verification Based on Relation Checking in SPIN: A Case Study

Download
  1. (PDF, 363 KB)
AuthorSearch for: ; Search for: ; Search for:
TypeArticle
ConferenceProceedings of the First Workshop on Formal Methods in Software Practice, January 11, 1996., San Diego, California, USA
AbstractA case study in formal verification of concurrent/distributed software is presented. The study concerns the modular specification and verification of a remote task protocol. The verification methodology used is based on semantic equivalence checking and is applicable to systems with hierarchical architectures. To support the methodology, we extended the verification tool Spin with the ability to check a particular class of semantic relations,and the language Promela upon which Spin is based with a simple mechanism to specify external operations. The foundations of semantic equivalence checking are also discussed briefly.
Publication date
LanguageEnglish
AffiliationNRC Institute for Information Technology; National Research Council Canada
Peer reviewedNo
NRC number39183
NPARC number5765210
Export citationExport as RIS
Report a correctionReport a correction
Record identifier2236c9d2-5c5a-4e38-a247-c782e780e4a0
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)