This Article 
 Bibliographic References 
 Add to: 
Enhancing Structured Review with Model-Based Verification
November 2004 (vol. 30 no. 11)
pp. 736-753
In this paper, 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.

[1] R.W. Selby and V.R. Basili, “Cleanroom Software Development: An Empirical Evaluation,” IEEE Trans. Software Eng., vol. 13, no. 9, pp. 1027-1037, Sept. 1987.
[2] T. Gilb and D. Graham, Software Inspection. Workingham: Addison-Wesley, 1993.
[3] R.C. Linger, “Cleanroom Process Model,” IEEE Software, vol. 11, no. 2, pp. 50-58, Mar. 1994.
[4] M. Fagan, “Design and Code Inspections to Reduce Errors in Program Development,” IBM Systems J., vol. 15, no. 3, pp. 182-211, 1976.
[5] D. Parnas and D.M. Weiss, “Active Design Reviews: Principles and Practices,” J. Systems and Softwares, pp. 259-265, 1987.
[6] E. van Emden and L. Moonen, “Java Quality Assurance by Detecting Code Smells,” Proc. Ninth Working Conf. Reverse Eng. (WCRE '02), pp. 97-108, Oct. 2002.
[7] M. Heimdahl and N. Leveson, “Completeness and Consistency Analysis of State-Based Requirements,” IEEE Trans. Software Eng., vol. 22, pp. 363-377, Nov. 1996.
[8] S. Easterbrook, R. Lutz, R. Covington, J. Kelly, Y. Ampo, and D. Hamilton, “Experiences Using Lightweight Formal Methods for Requirements Modeling,” IEEE Trans. Software Eng., vol. 24, pp. 4-14, Jan. 1998.
[9] I. Traoré, A. Jeffroy, M. Romdhani, and A.E.K. Sahraoui, “An Experience with a Multiformalism Specification of an Avionics System,” Proc. Int'l Council on Systems Eng. Conf., July 1998.
[10] M. Lawford, P. Froebel, and G. Moum, “Practical Application of Functional and Relational Methods for the Specification and Verification of Safety Critical Software,” Proc. Algebraic Methodology and Software Technology, Eighth Int'l Conf. (AMAST 2000), vol. 1816, pp. 7-88, May 2000.
[11] W. McUmber and B. Cheng, “A General Framework for Formalizing UML with Formal Languages,” Proc. IEEE Int'l Conf. Software Eng. (ICSE '01), May 2001.
[12] OMG, “OMG Unified Modeling Language Specification, version 2.0,” June 2003.
[13] S. Owre, J. Rushby, N. Shankar, and F. Henke, “Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS,” IEEE Trans. Software Eng., vol. 21, no. 2, pp. 107-125, Feb. 1995.
[14] I. Traoré, “An Integrated V&V Environment for Critical Systems Development,” Proc. Fifth IEEE Int'l Symp. Requirements Eng., Aug. 2001.
[15] R.N. Britcher, “Using Inspections to Investigate Program Correctness,” Computer, Nov. 1988.
[16] P. Kruchten, The Rational Unified Process. Addison Wesley, Sept. 1999.
[17] O. Laitenberger, C. Atkison, M. Schlich, and K.E. Emam, “Using Inspection Technology in Object-Oriented Development Projects,” Technical Report NRC/ERB-1077, Nat'l Research Council, Canada, June 2000.
[18] J.B. Warmer and A.G. Kleppe, The Object Constraint Language: Precise Modeling with UML. Addison Wesley Longman Inc., 1999.
[19] C. Jones, Systematic Software Development Using VDM, second ed. Englewood Cliffs, N.J.: Prentice-Hall, 1990.
[20] I. Traoré, “An Outline of PVS Semantics for UML Statecharts,” J. Universal Computer Science, vol. 6, no. 11, pp. 1088-1108, 2000.
[21] D.B. Aredo, “A Framework for Semantics of UML Sequence Diagrams in PVS,” J. Universal Computer Science, vol. 8, no. 7, pp. 674-697, July 2002.
[22] R.B. France, A. Evans, K. Lano, and B. Rumpe, “The UML as a Formal Modeling Notation,” Computer Standards and Interfaces, vol. 19, pp. 325-334, 1998.
[23] A. Evans, “Reasoning with UML Class Diagrams,” Proc. Workshop Industrial-Strength Formal Specification Techniques (WIFT '98), 1998.
[24] M.Y. Liu, “PVS Proof Patterns for UML-Based Verification,” masters thesis, Dept. of Electrical and Computer Eng., Univ. of Victoria, Oct. 2002.
[25] I. Traoré, “A Transition-Based Testing Strategy for Object-Oriented Programs,” Proc. ACM Symp. Applied Computing (SAC '03), Mar. 2003.
[26] I. Traoré, D.B. Aredo, and H. Ye, “An Integrated Framework for Formal Development of Distributed Systems,” Proc. ACM Symp. Applied Computing (SAC '03), Mar. 2003.
[27] D. Kung, N. Suchak, J. Dao, and P. Hsia, “On Object State Testing,” Proc. IEEE COMPSAC '94 Conf., Feb. 1994.
[28] R.-K. Doong and P.G. Frankl, “The ASTOOT Approach to Testing Object-Oriented Programs,” ACM Trans. Software Eng. and Methodology, vol. 3, no. 2, 1994.
[29] P. Stocks and D. Carrington, “A Framework for Specification-Based Testing,” IEEE Trans. Software Eng., vol. 22, no. 11, pp. 777-793, 1996.
[30] L. Briand and Y. Labiche, “A UML-Based Approach to System Testing,” Proc. Fourth UML Int'l Conf. (UML 2001), M. Gogolla and C. Kobryn, eds., Oct. 2001.
[31] Y. Hong, “UML-Based Testing of Object-Oriented Programs,” master's thesis, Dept. of Electrical and Computer Eng., Univ. of Victoria, July 2003.
[32] V. Basili, “Evolving and Packaging Reading Technologies,” Systems and Software, vol. 38, no. 1, pp. 3-12, 1997.
[33] O. Laitenberger, C. Atkison, M. Schlich, and K. El Emam, “An Experimental Comparison of Reading Techniques for Defect Detection in UML Design Documents,” Systems and Software, pp. 183-204, 2000.
[34] A. Dunsmore, M. Roper, and M. Wood, “The Development and Evaluation of Three Diverse Techniques for Object-Oriented Code Inspection,” IEEE Trans. Software Eng., vol. 29, no. 8, Aug. 2003.
[35] A. Dunsmore, M. Roper, and M. Wood, “Systematic Object-Oriented Inspection— An Empirical Study,” Proc. 23rd Int'l Conf. Software Eng. (ICSE '01), pp. 135-144, May 2001.
[36] T. Thelin, P. Runeson, and B. Regnell, “Usage-Based Reading— An Experiment to Guide Reviewers with Use Cases,” J. Information and Software Technology, vol. 43, no. 15, pp. 925-938, 2001.
[37] R.B. France, J.-M. Bruel, M. Larrondo-Petrie, and M. Shroff, “Exploring the Semantics of UML Type Structures with Z,” Proc. Second IFIP Conf. Formal Methods for Open Object-Based Distributed Systems (FMOODS '97), H. Bowman and J. Derrick, eds., 1997.
[38] M. Broy, “On the Meaning of Message Sequence Charts,” Proc. European Conf. Object-Oriented Programming (ECOOP '97), June 1997.
[39] W. Damm and D. Harel, “LSC's: Breathing Life into Message Sequence Charts,” Proc. Conf. Formal Methods for Open Distributed Systems (FMOODS '99), Feb. 1999.
[40] E. Mikk, Y. Lakhnech, and M. Siegel, “Hierarchical Automata as Model for Statecharts,” Proc. Asian Computing Science Conf. (ASIAN '97), pp. 181-196, Dec. 1997.
[41] D. Latella, I. Majzik, and M. Massink, “Towards a Formal Operational Semantics of UML Statechart Diagrams,” Proc. Conf. Formal Methods for Open Distributed Systems (FMOODS '99), Feb. 1999.
[42] D.P. Gluch and C.B. Weinstock, “Model-Based Verification: A Technology for Dependable System Upgrade,” Technical Report CMU/SEI-98-TR-009, Software Eng. Inst., Carnegie Mellon Univ., Pittsburgh, Penn., Sept. 1998.
[43] G. Engels, J.M. Küster, R. Heckel, and M. Lohmann, “Model-Based Verification and Validation of Properties,” Electronic Notes in Theoretical Computer Science, R. Bardohl and H. Ehrig, eds., 2003.
[44] Formal Systems Europe (Ltd), “Failures-Divergence-Refinement: FDR2 User Manual,” 1997.
[45] I. Jacobson, “A Resounding Yes to Agile Processes-But Also to More,” Cutter IT J., vol. 15, no. 1, Jan. 2002.
[46] W. Liu, S. Easterbrook, and J. Mylopoulos, “Rule-Based Detection of Inconsistency in UML Models,” Proc. Workshop Consistency Problems in UML-Based Software Development (UML '02), L. Kurniaz et al., eds., pp. 106-123, 2002.
[47] G. Caplat and J.-L. Sourouille, “Model Mapping in MDA,” Proc. Workshop Software Model Eng. (WISME), 2002.

Index Terms:
Structured review, formal methods, UML, prototype verification system (PVS), OCL, model-based verification, validation and verification.
Issa Traor?, Demissie B. Aredo, "Enhancing Structured Review with Model-Based Verification," IEEE Transactions on Software Engineering, vol. 30, no. 11, pp. 736-753, Nov. 2004, doi:10.1109/TSE.2004.86
Usage of this product signifies your acceptance of the Terms of Use.