No Access

A REVIEW APPROACH TO DETECTING VIOLATIONS OF CONSISTENCY BETWEEN SPECIFICATION AND PROGRAM STRUCTURES

YUTING CHEN

Faculty of Computer and Information Sciences, Hosei University, Tokyo 184-8584, Japan

Computer Science and Engineering Department, Shanghai Jiaotong University, Shanghai 200240, P. R. China

State Key Laboratory for Novel Software Technology, Nanjing University, P. R. China

Search for more papers by this author

SHAOYING LIU

Faculty of Computer and Information Sciences, Hosei University, Tokyo 184-8584, Japan

Search for more papers by this author

, and

W. ERIC WONG

Department of Computer Science, University of Texas at Dallas, Richardson, TX 75080, USA

Search for more papers by this author

https://doi.org/10.1142/S0218194008003994Cited by:0 (Source: Crossref)

Abstract

The application of specification-based program verification techniques (e.g., black-box testing, formal proof) faces strong challenges in practice when the gap between the structure of a specification and that of its program is large. This paper describes a view-based program review approach to addressing these challenges. The essential idea of the approach is first to derive comparable views from the specification and program, and then detect and eliminate the violations of structural consistency in the program views on the basis of a set of criteria. We also developed a prototype tool to support the review approach, and conducted a case study to assess the effectiveness of the approach.

This work is supported by the Ministry of Education, Culture, Sports, Science and Technology of Japan under Grant-in-Aid for Scientific Research (No. 18500027). In addition Shaoying Liu is also supported by the NSFC Grant (No. 60433010), and Yuting Chen by the State Key Laboratory for Novel Software Technology (No. KFKT2008B05).

Keywords:

References

B. Beizer , Black Box Testing-Techniques for Functional Testing of Software and Systems ( John Wiley & Sons , New York , 1995 ) . Google Scholar
F. D. Gregory, Software Formal Inspections Standard, NASA Office of Safety and Mission Assurance, Washington, D.C., USA, Tech. Rep. NASA-STD-2202-93, April 1993 . Google Scholar
C. Hoare, Commun. ACM 12(10), 576 (1969), DOI: 10.1145/363235.363259. Crossref, Web of Science, Google Scholar
C. B. Jones , Systematic Software Development Using VDM ( Prentice-Hall , 1990 ) . Google Scholar
I. J. Hayes, C. B. Jones and J. E. Nicholls, ACM SIGSOFT Software Engineering Notes 19(3), 75 (1994), DOI: 10.1145/182824.182843. Crossref, Google Scholar
S. Liu , Formal Engineering for Industrial Software Development Using the SOFL Method ( Springer , Germany , 2004 ) . Crossref, Google Scholar
S. Liu, A Case Study of Modeling an ATM Using SOFL, Faculty of Computer and Information Sciences, Hosei University, Tokyo, Japan, Technical Report HCIS-2003-01, 2003, http://cis.k.hosei.ac.jp/TR/ . Google Scholar
S. Liu, M. Shibata and R. Sato, Applying SOFL to develop a university information system, Proc. 6th Asia-Pacific Software Engineering Conf. (APSEC '99) (IEEE Computer Society Press) pp. 404–411. Google Scholar
S. Liuet al., An automated approach to specification-based program inspection, Proc. 7th Int. Conf. Formal Engineering Methods (ICEEM '05), LNCS 3785 (Springer) pp. 421–434. Google Scholar
F. Nagoya, S. Liu and Y. Chen, An investigation of the approach to specification-based program review through case studies, Proc. 9th IEEE Int. Conf. Engineering of Complex Computer Systems (ICECCS '04) (IEEE Computer Society Press) pp. 249–258. Google Scholar
V. R. Gibson and J. A. Senn, Commun. ACM 32(3), 347 (1989), DOI: 10.1145/62065.62073. Crossref, Web of Science, Google Scholar
S. Liuet al., IEEE Trans. Software Engineering: Special Issue on Formal Methods 24(1), 337 (1998). Web of Science, Google Scholar
W. Brauer , G. Rozenberg and A. Salomaa , Petri Nets: An Introduction ( Springer-Verlag , 1985 ) . Google Scholar
D. L. Parnas and M. Lawford, IEEE Trans. Software Engineering 29(8), 674 (2003), DOI: 10.1109/TSE.2003.1223642. Crossref, Web of Science, Google Scholar
Sun Microsystems Inc., Java Compiler Compiler [tm] (JavaCC [tm]): — The Java Parser Generator, https://javacc.dev.java.net/ . Google Scholar
JGraph Ltd , Java Graph Visualization and Layout ( 2006 ) , http://www.jgraph.com/ . Google Scholar
A. Dunsmore, M. Roper and M. Wood, IEEE Trans. Software Engineering 29(8), 677 (2003), DOI: 10.1109/TSE.2003.1223643. Crossref, Web of Science, Google Scholar
H. Muccini, A. Bertolino and P. Inverardi, IEEE Trans. Software Engineering 30(3), 160 (2004), DOI: 10.1109/TSE.2004.1271170. Crossref, Web of Science, Google Scholar
A. Watson and T. McCabe, Structured Testing: A Testing Methodology Using the Cyclomatic Complexity Metric, August 1996, National Institute of Standards and Technology Special Publication, pp. 500–235 . Google Scholar
J. Nielsen , Usability Engineering ( Morgan Kaufmann , San Diego , 1993 ) . Crossref, Google Scholar
M. Frappier, S. Matwin, and A. Mili, Software Metrics for Predicting Maintainability, Canadian Space Agency, Tech. Rep., 1994 . Google Scholar
J. Lindroos, The Roles of Program Structure in Software Maintenance, February 2005, http://www.cs.helsinki.fi/u/paakki/lindroos.pdf . Google Scholar
B. Beizer , Software Testing Techniques ( Van Nostrand Reinhold , 1990 ) . Google Scholar
P. C. Jorgensen , Software Testing: A Craftsman's Approach ( CRC Press , 1995 ) . Google Scholar
R. L. Krikhaar, Reverse architecting approach for complex systems, Proc. 1997 Int. Conf. Software Maintenance (IEEE Computer Society, 1997) pp. 4–11. Google Scholar
W. Bischofberger, J. Kühl and S. Loffler, Sotograph: A pragmatic approach to source code architecture conformance checking, Proc. First European Workshop on Software Architecture (EWSA '04), LNCS 3047 (Springer, 2004) pp. 1–9. Google Scholar
The Open Group , Architecture Compliance ( The Open Group , 2006 ) , http://www.opengroup.org/architecture/togaf8-doc/arch/ . Google Scholar
G. Florijn , Anaja — Tool support for architecture conformance checks and reviews , Proc. Landelijk Architectuur Congres (LAC'00) . Google Scholar
R. Boerman, On Software Architecture Conformance: In the Context of Evolving Systems, Master's thesis, Delft University of Technology, 2004 . Google Scholar
C. Johansson and L. Wennolf, Software Architecture Verification Tool for Software Platforms, Master's thesis, Lund University, 2002 . Google Scholar
M. Harrold, Testing: A roadmap, Proc. 22nd Int. Conf. Software Engineering (ICSE'00) (2000) pp. 61–72. Google Scholar
M. Harrold, Architecture-based regression testing of evolving systems, Proc. Int. Workshop on the Role of Software Architecture in Testing and Analysis (1998) pp. 73–77. Google Scholar
K. Bogdanov, Automated Testing of Harel's Statecharts, Ph.D. dissertation, University of Sheffield, 2000 . Google Scholar
J. Tretmans, Computer Networks and ISDN Systems 29, 49 (1996), DOI: 10.1016/S0169-7552(96)00017-7. Crossref, Web of Science, Google Scholar
J. C. Fernandezet al., Science of Computer Programming 29(1–2), 123 (1997), DOI: 10.1016/S0167-6423(96)00032-9. Crossref, Web of Science, Google Scholar
L. Wanget al., Generating test cases from UML activity diagram based on gray-box method, Proc. 11th Asia-Pacific Software Engineering Conf. (APSEC'04) (IEEE Computer Society) pp. 284–291. Google Scholar
Y. Fu, Z. Dong and X. He, An approach to validation of software architecture model, Proc. 12th Asia-Pacific Software Engineering Conf. (APSEC '05) (IEEE Computer Society) pp. 375–384. Google Scholar
R. Kazmanet al., IEEE Software 13(6), 43 (1996), DOI: 10.1109/52.542294. Web of Science, Google Scholar
A. Egyed, A scenario-driven approach to traceability, Proc. 23rd Int. Conf. Software Engineering (ICSE '01) (IEEE Computer Society) pp. 123–132. Google Scholar