The Community for Technology Leaders
Green Image
Issue No. 05 - Sept.-Oct. (2012 vol. 38)
ISSN: 0098-5589
pp: 1100-1122
F. Nagoya , Grad. Sch. of Int. Manage., Aoyama Gakuin Univ., Sagamihara, Japan
Yuting Chen , Software Sch., Shanghai Jiaotong Univ., Shanghai, China
Shaoying Liu , Dept. of Comput. Sci., Hosei Univ., Koganei, 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
F. Nagoya, Yuting Chen, Shaoying Liu, J. A. McDermid, "Formal Specification-Based Inspection for Verification of Programs", IEEE Transactions on Software Engineering, vol. 38, no. , pp. 1100-1122, Sept.-Oct. 2012, doi:10.1109/TSE.2011.102
116 ms
(Ver 3.1 (10032016))