A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV)

This report presents the results of a case study into practice issues involved in using the Symbolic Model Verifier (SMV) for model checking software systems. The case study is of a Simplex implementation-the Simplex coordinated demonstration system for reliable system upgrade. The investigation con...

Full description

Saved in:
Bibliographic Details
Main Authors: Srinivasan, Grama R, Gluch, David P
Format: Report
Language:English
Subjects:
COMPUTER PROGRAM RELIABILITY
COMPUTER PROGRAM VERIFICATION
Computer Programming and Software
MATHEMATICAL MODELS
SMV(SYMBOLIC MODEL VERIFIER)
SOFTWARE ENGINEERING
SYMBOLIC PROGRAMMING
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This report presents the results of a case study into practice issues involved in using the Symbolic Model Verifier (SMV) for model checking software systems. The case study is of a Simplex implementation-the Simplex coordinated demonstration system for reliable system upgrade. The investigation consisted of generating a system model (using both statechart and SMV notations), specifying claims (expected properties) of the system as temporal logic formulae, and checking those formulae with respect to the SMV model. The various steps involved in the modeling process are described. Examples of the claims, their results, and a description of how the SMV tool analyzed them are detailed. Key engineering decisions made during the modeling process and a work breakdown of the effort are also presented.