The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - Sept.-Oct. (2012 vol.38)
pp: 1100-1122
Shaoying Liu , Dept. of Comput. Sci., Hosei Univ., Koganei, Japan
Yuting Chen , Software Sch., Shanghai Jiaotong Univ., Shanghai, China
F. Nagoya , Grad. Sch. of Int. Manage., Aoyama Gakuin Univ., Sagamihara, Japan
J. A. McDermid , Dept. of Comput. Sci., Univ. of York, York, UK
ABSTRACT
Software inspection is a static analysis technique that is widely used for defect detection, but which suffers from a lack of rigor. In this paper, we address this problem by taking advantage of formal specification and analysis to support a systematic and rigorous inspection method. The aim of the method is to use inspection to determine whether every functional scenario defined in the specification is implemented correctly by a set of program paths and whether every program path of the program contributes to the implementation of some functional scenario in the specification. The method is comprised of five steps: deriving functional scenarios from the specification, deriving paths from the program, linking scenarios to paths, analyzing paths against the corresponding scenarios, and producing an inspection report, and allows for a systematic and automatic generation of a checklist for inspection. We present an example to show how the method can be used, and describe an experiment to evaluate its performance by comparing it to perspective-based reading (PBR). The result shows that our method may be more effective in detecting function-related defects than PBR but slightly less effective in detecting implementation-related defects. We also describe a prototype tool to demonstrate the supportability of the method, and draw some conclusions about our work.
INDEX TERMS
formal verification, formal specification, prototype tool, formal specification based inspection, program verification, software inspection, defect detection, automatic generation, systematic generation, perspective based reading, PBR, DH-HEMTs, High definition video, Three dimensional displays, program verification, Specification-based program inspection, software inspection, formal specification
CITATION
Shaoying Liu, Yuting Chen, F. Nagoya, J. A. McDermid, "Formal Specification-Based Inspection for Verification of Programs", IEEE Transactions on Software Engineering, vol.38, no. 5, pp. 1100-1122, Sept.-Oct. 2012, doi:10.1109/TSE.2011.102
REFERENCES
[1] C.A. Toman, A.A. Porter, H. Siy, and L.G. Votta, "An Experiment to Assess the Cost-Benefits of Code Inspections in Large Scale Software Development," IEEE Trans. Software Eng., vol. 23, no. 6, pp. 329-346, June 1997.
[2] J.R. Abrial, The B-Book: Assigning Programs to Meanings. Cambridge Univ. Press, 1996.
[3] A. Aurum, H. Petersson, and C. Wohlin, "State-of-the-Art: Software Inspections after 25 Years," Software Testing, Verification and Reliability, vol. 12, no. 3, pp. 133-154, 2002.
[4] G. Babin and F. Lustman, "Application of Formal Methods to Scenario-Based Requirements Engineering," Int'l J. Computers and Applications, vol. 23, no. 3, pp. 141-151, 2001.
[5] R.-J. Back and J. von Wright, Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.
[6] C. Baier and J.P. Katoen, Principles of Model Checking. The MIT Press, 2008.
[7] J. Barnard and A. Price, "Managing Code Inspection Information," IEEE Software, vol. 11, no. 2, pp. 59-69, Mar. 1994.
[8] V.R. Basili, S. Green, O. Laitenberger, F. Lanubile, F. Shull, S. Sorumgard, and M. Zelkowitz, "The Empirical Investigation of Perspective-Based Reading," Empirical Software Eng., vol. 2, no. 1, pp. 133-164, 1996.
[9] V.R. Basili and R.W. Selby, "Comparing the Effectiveness of Software Testing Strategies," IEEE Trans. Software Eng., vol. 13, no. 12, pp. 1278-1296, Dec. 1987.
[10] G. Bernot, M.C. Gaudel, and B. Marre, "Software Testing Based on Formal Specifications: A Theory and a Tool," Software Eng. J., vol. 6, no. 6, pp. 387-405, 1991.
[11] A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. Mcpeak, and D. Engler, "A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World," Comm. ACM, vol. 53, no. 2, pp. 66-75, Feb. 2010.
[12] D.B. Bisant and J.R. Lyle, "A Two-Person Inspection Method to Improve Programming Productivity," IEEE Trans. Software Eng., vol. 15, no. 10, pp. 1294-1304, Oct. 1989.
[13] W. Bush, J. Pincus, and D. Sielaff, "A Static Analyzer for Finding Dynamic Programming Errors," Software Practice and Experience, vol. 30, no. 7, pp. 775-802, June 2000.
[14] M. Chechik and J.D. Gannon, "Automatic Analysis of Consistency between Requirements and Designs," IEEE Trans. Software Eng., vol. 27, no. 7, pp. 651-672, June 2001.
[15] E.M. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2000.
[16] J. Dawes, The VDM-SL Reference Guide. Pitman, 1991.
[17] J. Dick and A. Faivre, "Automating the Generation and Sequencing of Test Cases from Model-Based Specifications," First Int'l Symp. Formal Methods Europe Industrial-Strength Formal Methods, pp. 268-284, Apr. 1993.
[18] E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics. Springer-Verlag, 1990.
[19] A. Dunsmore, M. Roper, and M. Wood, "Practical Code Inspection Techniques for Object-Oriented Systems: An Experimental Comparison," IEEE Software, vol. 20, no. 4, pp. 21-29, July/Aug. 2003.
[20] M.E. Fagan, "Design and Code Inspections to Reduce Errors in Program Development," IBM Systems J., vol. 15, no. 3, pp. 182-211, 1976.
[21] H.N. Gabow, S.N. Maheshwari, and L.J. Osterweil, "On Two Problems in the Generation of Program Test Paths," IEEE Trans. Software Eng., vol. 2, no. 3, pp. 227-231, May 1976.
[22] T. Gilb and D. Graham, Software Inspection. Addison Wesley, 1993.
[23] A. Hall, "Realising the Benefits of Formal Methods," Proc. Seventh Int'l Conf. Formal Eng. Methods, pp. 1-4, Nov. 2005.
[24] C.L. Heitmeyer, "Software Cost Reduction," Encyclopedia of Software Eng., J.J. Marciniak, ed., second ed., pp. 1374-1380, John Wiley & Sons, 2002.
[25] C.L. Heitmeyer, J. Kirby, and B. Labaw, "Applying the SCR Requirements Method to a Weapons Control Panel: An Experience Report," Proc. Second Workshop Formal Methods in Software Practice, pp. 92-102, 1998.
[26] C.A.R. Hoare and J. He, Unifying Theories of Programming. Prentice Hall, 1998.
[27] C.A.R. Hoare and N. Wirth, "An Axiomatic Definition of the Programming Language PASCAL," Acta Informatica, vol. 2, no. 4, pp. 335-355, 1973.
[28] Coverity Static Analysis, http://www.coverity.com/products static-analysis.html , 2012.
[29] IEEE Standard for Software Rev., IEEE Standard 1028-1997, IEEE CS, 1997.
[30] D. Jackson, "Alloy: A Lightweight Object Modeling Notation," ACM Trans. Software Eng. and Methodology, vol. 11, no. 2, pp. 256-290, 2002.
[31] D. Jackson, I. Schechter, and I. Shlyakhter, "Alcoa: The Alloy Constraint Analyzer," Proc. 22nd Int'l Conf. Software Eng., pp. 730-733, June 2000.
[32] P. Jalote, A.K. Mittal, and R.G. Prajapat, "On Optimum Module Size for Software Inspections," Int'l J. Reliability, Quality and Safety Eng., vol. 14, no. 3, pp. 283-295, 2007.
[33] X.H. Jin, "Use of Tabular Expressions in the Inspection of Concurrent Programs," SQRL Report No. 25, Univ. of Limerick, 2005.
[34] C.B. Jones, Systematic Software Development Using VDM, second ed. Prentice Hall, 1990.
[35] D. Kelly and T. Shepard, "Task-Directed Software Inspection Technique: An Experiment and Case Study," Proc. Conf. Centre for Advanced Studies on Collaborative Research, p. 6, Nov. 2000.
[36] R.A. Kemmerer, "Testing Formal Specifications to Detect Design Errors," IEEE Trans. Software Eng., vol. 11, no. 1, pp. 32-43, Jan. 1985.
[37] J.C. Knight, C.L. DeJong, M.S. Gibble, and L.G. Nakano, "Why Are Formal Methods Not Used More Widely?" Proc. Fourth NASA Langley Formal Methods Workshop, C.M. Holloway and K.J. Hayhurst, eds., pp. 1-12, 1997.
[38] J.C. Knight and E.A. Myers, "An Improved Inspection Technique," Comm. ACM, vol. 36, no. 11, pp. 51-61, 1993.
[39] S. Kollanus and J. Koskinen, "Survey of Software Inspection Research: 1991-2005," Computer Science and Information Systems Reports Working Papers WP-40, Univ. of Jyvaskyla, Finland, 2007.
[40] D.R. Kuhn, "Fault Classes and Error Detection Capability of Specification-Based Testing," ACM Trans. Software Eng. and Methodology, vol. 8, no. 4, pp. 411-424, Oct. 1999.
[41] T. Kurita, M. Chiba, and Y. Nakatsugawa, "Application of a Formal Specification Language in the Development of the Mobile FeliCa IC Chip Firmware for Embedding in Mobile Phones," Proc. Int'l Symp. Formal Methods, J. Cuellar, T. Maibaum, and K. Sere, eds., pp. 425-429, May 2008.
[42] O. Laitenberger, "A Survey of Software Inspection Technologies," Handbook of Software Eng. and Knowledge Eng., pp. 517-556, World Scientific Publishing, 2002.
[43] O. Laitenberger, K.E. Emam, and T.G. Harbich, "An Internally Replicated Quasi-Experimental Comparison of Checklist and Perspective-Based Reading of Code Documents," IEEE Trans. Software Eng., vol. 27, no. 5, pp. 387-421, May 2001.
[44] P.G. Larsen, J. Fitzgerald, and T. Brookes, "Applying Formal Specification in Industry," IEEE Software, vol. 13, no. 3, pp. 48-56, May 1996.
[45] S. Liu, Formal Engineering for Industrial Software Development Using the SOFL Method. Springer-Verlag, 2004.
[46] S. Liu, M. Asuka, K. Komaya, and Y. Nakamura, "An Approach to Specifying and Verifying Safety-Critical Systems with the Practical Formal Method SOFL," Proc. Fourth IEEE Int'l Conf. Eng. of Complex Computer Systems, pp. 100-114, Aug. 1998.
[47] S. Liu and Y. Chen, "A Relation-Based Method Combining Functional and Structural Testing for Test Case Generation," J. Systems and Software, vol. 81, no. 2, pp. 234-248, Feb. 2008.
[48] S. Liu, F. Nagoya, Y. Chen, M. Goya, and J.A. McDermid, "An Automated Approach to Specification-Based Program Inspection," Proc. Seventh Int'l Conf. Formal Eng. Methods, K.K. Lau and R. Banach, eds., pp. 421-434, Nov. 2005.
[49] J. McDonald and P. Strooper, "Translating Object-Z Specifications to Passive Test Oracles," Proc. Second Int'l Conf. Formal Eng. Methods, J. Staples, M.G. Hinchey, and S. Liu, eds., pp. 165-174, Dec. 1998.
[50] T. Miller and P. Strooper, "Model-Based Specification Animation Using Testgraphs," Proc. Fourth Int'l Conf. Formal Eng. Methods, C. George and H. Miao, eds., pp. 192-203, Oct. 2002.
[51] C. Morgan, Programming from Specifications, second ed. Prentice Hall, 1994.
[52] I. Morrey, J. Siddiqi, R. Hibberd, and G. Buckberry, "A Toolset to Support the Construction and Animation of Formal Specifications," J. Systems and Software, vol. 41, no. 3, pp. 147-160, June 1998.
[53] Software Formal Inspections Standard, NASA-STD-2202-93, technical report, NASA, 1993.
[54] D.L. Parnas, "Tabular Representation of Relations," CRL Report 260, McMaster Univ., Comm. Research Laboratory, TRIO (Telecomm. Research Inst. of Ontario), Oct. 1992.
[55] D.L. Parnas, G. Asmis, and J. Madey, "Assessment of Safety-Critical Software in Nuclear Power Plants," Nuclear Safety, vol. 32, no. 2, pp. 189-198, Apr.-June 1991.
[56] D.L. Parnas and M. Lawford, "The Role of Inspection in Software Quality Assurance," IEEE Trans. Software Eng., vol. 29, no. 8, pp. 674-676, Aug. 2003.
[57] D.L. Parnas, J. Madey, and M. Iglewski, "Precise Documentation of Well-Structured Programs," IEEE Trans. Software Eng., vol. 20, no. 12, pp. 948-976, Dec. 1994.
[58] D.L. Parnas and D.M. Weiss, "Active Design Reviews: Principles and Practices," J. Systems and Software, vol. 7, no. 4, pp. 259-265, 1987.
[59] A.A. Porter, H.P. Siy, and L.G. Votta, "A Review of Software Inspections," Advances in Computers, vol. 42, pp. 39-76, 1996.
[60] A. Reuys, S. Reis, E. Kamsties, and K. Pohl, "Derivation of Domain Test Scenarios from Activity Diagrams," Proc. Workshop Product Line Eng.-The Early Steps, K. Schmid and B. Geppert, eds., pp. 35-41, Dec. 2003.
[61] S. Sahara, "An Experience of Applying Formal Method on a Large Business Application (in Japanese)," Proc. Symp. Science and Technology on System Verification, pp. 93-100, Feb. 2004.
[62] M. Shannon, G. Miller, R.J. Prewitt, and S. Loveland, Software Testing Techniques: Finding the Defects that Matter, Charles River Media, 2004.
[63] D.I.K. Sjoberg, J.E. Hannay, O. Hansen, V.B. Kampenes, A. Karahasanovic, N.K. Liborg, and A.C. Rekdal, "A Survey of Controlled Experiments in Software Engineering," IEEE Trans. Software Eng., vol. 31, no. 9, pp. 733-753, Sept. 2005.
[64] S.A. Stelting and O.M. Leeuwen, Applied Java Patterns. Prentice Hall, 2001.
[65] S. Stepney, "A Tale of Two Proofs," Proc. BCS-FACS Third Northern Formal Methods Workshop, Sept. 1998.
[66] P. Stocks and D. Carrington, "A Framework for Specification-Based Testing," IEEE Trans. Software Eng., vol. 22, no. 11, pp. 777-793, Nov. 1996.
[67] R.H. Thayer, Software Reviews, Inspections and Audits: A Standards-Based Guide, Software Eng. Standards Series. IEEE CS Press, June 2010.
[68] T. Thelin, P. Runeson, and B. Regnell, "Usage-Based Reading—An Experiment to Guide Reviewers with Use Cases," Information and Software Technology, vol. 43, no. 15, pp. 925-938, 2001.
[69] T. Thelin, P. Runeson, and C. Wohlin, "An Experimental Comparison of Usage-Based and Checklist-Based Reading," IEEE Trans. Software Eng., vol. 29, no. 8, pp. 687-704, Aug. 2003.
[70] G. Travassos, F. Shull, M. Fredericks, and V.R. Basili, "Detecting Defects in Object-Oriented Designs: Using Reading Techniques to Increase Software Quality," Proc. 14th ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages and Applications, pp. 47-56, 1999.
[71] M.E. Vieira, M.S. Dias, and D.J. Richardson, "Object-Oriented Specification-Based Testing Using UML Statechart Diagrams," EFoCS-33-98, Univ. of California, 2000.
[72] J. Warmer and A. Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley, 2003.
[73] A. Wassyng and M. Lawford, "Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project," Proc. Int'l Symp. Formal Methods Europe, K. Araki, S. Gnesi, and D. Mandriioli, eds., pp. 133-153, Aug. 2003.
[74] A. Wassyng and M. Lawford, "Software Tools for Safety-Critical Software Development," Int'l J. Software Tools for Technology Transfer, vol. 8, no. 4, pp. 337-354, 2006.
[75] D.A. Wheeler, B. Brykczynski, and R.N. Meeson, Software Inspection: An Industry Best Practice for Defect Detection and Removal. IEEE CS Press, 1996.
[76] K.E. Wiegers, Peer Review in Software: A Practical Guide. Addison-Wesley, 2002.
[77] D. Winkler, Improvement of Defect Detection with Software Inspection Variants: A Large-Scale Empirical Study on Reading Techniques and Experience. VDM Verlag, May 2008.
[78] C. Wohlin, P. Runeson, M. Host, M.C. Ohlsson, B. Regnell, and A. Wesslen, Experimentation in Software Engineering: An Introduction. Kluwer Academic Publishers, 2000.
[79] J. Woodcock and J. Davies, Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.
[80] J. Woodcock, P.G. Larsen, J. Bicarregui, and J. Fitzgerald, "Formal Methods: Practice and Experience," ACM Computing Surveys, vol. 41, no. 4, pp. 1-39, 2009.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool