• DocumentCode
    1164916
  • Title

    Enhancing structured review with model-based verification

  • Author

    Traoré, Issa ; Aredo, Demissie B.

  • Author_Institution
    Dept. of Electr. & Comput. Eng., Victoria Univ., BC, Canada
  • Volume
    30
  • Issue
    11
  • fYear
    2004
  • Firstpage
    736
  • Lastpage
    753
  • Abstract
    We propose a development framework that extends the scope of structured review by supplementing the structured review with model-based verification. The proposed approach uses the Unified Modeling Language (UML) as a modeling notation. We discuss a set of correctness arguments that can be used in conjunction with formal verification and validation (V&V) in order to improve the quality and dependability of systems in a cost-effective way. Formal methods can be esoteric; consequently, their large scale application is hindered. We propose a framework based on the integration of lightweight formal methods and structured reviews. Moreover, we show that structured reviews enable us to handle aspects of V&V that cannot be fully automated. To demonstrate the feasibility of our approach, we have conducted a study on a security-critical system - a patient document service (PDS) system.
  • Keywords
    Unified Modeling Language; formal specification; formal verification; program testing; safety-critical software; Unified Modeling Language; formal validation; formal verification; model-based verification; object constraint language; patient document service system; prototype verification system; security-critical system; structured review; Costs; Formal verification; Guidelines; Helium; Large-scale systems; Prototypes; Quality assurance; Software prototyping; Software quality; Unified modeling language; 65; Index Terms- Structured review; OCL; PVS; UML; formal methods; model-based verification; prototype verification system; validation and verification.;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/TSE.2004.86
  • Filename
    1359768