Architecture-Driven Verification of Concurrent Systems

Download
  1. (PDF, 487 KB)
  2. Get@NRC: Architecture-Driven Verification of Concurrent Systems (Opens in a new window)
AuthorSearch for:
TypeArticle
Journal titleNordic Journal of Computing
Volume4
Issue4
Subjectarchitecture-based verification; architectural specifications; architectural formalisms; model checking; equivalence checking; compositional verification.
AbstractThis paper proposes a method to construct a set of proof obligations from the architectural specification of a concurrent system. The architectural specifications used express correctness requirements of a concurrent system at a high level without any reference to component functionality. Then the proof obligations derived from such specifications are discharged as model checking tasks in a suitable behavioral model where components are assigned their respective functionalities. An experimental extension to the SPIN tool is used as the model checker. The block diagram notation used to specify architectures allows interchangeable components with equivalent intended functionalities to be encapsulated within a representative module. A proof obligation of such a system is discharged as an equivalence checking task in the behavioral model chosen. It is shown how infeasible proof obligations can be decomposed by decomposing the architectural specification. Obligation decomposition relies on assume-guarantee conditions.
Publication date
LanguageEnglish
AffiliationNRC Institute for Information Technology; National Research Council Canada
Peer reviewedNo
NRC number41549
NPARC number5764623
Export citationExport as RIS
Report a correctionReport a correction
Record identifierabb9b207-f404-42d0-8d05-2d95adbf15e9
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)