This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Specification-Based Inspection for Verification of Programs
Sept.-Oct. 2012 (vol. 38 no. 5)
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
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
Usage of this product signifies your acceptance of the Terms of Use.