Welcome to the InfoSci Platform
Architecture-Centered Integrated Verification

Architecture-Centered Integrated Verification

Yujian Fu, Zhijang Dong, Xudong He
Copyright: © 2012 |Pages: 22
ISBN13: 9781613504567|ISBN10: 161350456X|EISBN13: 9781613504574
DOI: 10.4018/978-1-61350-456-7.ch202
Cite Chapter Cite Chapter

MLA

Fu, Yujian, et al. "Architecture-Centered Integrated Verification." Computer Engineering: Concepts, Methodologies, Tools and Applications, edited by Information Resources Management Association, IGI Global, 2012, pp. 201-222. https://doi.org/10.4018/978-1-61350-456-7.ch202

APA

Fu, Y., Dong, Z., & He, X. (2012). Architecture-Centered Integrated Verification. In I. Management Association (Ed.), Computer Engineering: Concepts, Methodologies, Tools and Applications (pp. 201-222). IGI Global. https://doi.org/10.4018/978-1-61350-456-7.ch202

Chicago

Fu, Yujian, Zhijang Dong, and Xudong He. "Architecture-Centered Integrated Verification." In Computer Engineering: Concepts, Methodologies, Tools and Applications, edited by Information Resources Management Association, 201-222. Hershey, PA: IGI Global, 2012. https://doi.org/10.4018/978-1-61350-456-7.ch202

Export Reference

Mendeley
Favorite

Abstract

The approach aims at solving the above problems by including the analysis and verification of two different levels of software development process–design level and implementation level-and bridging the gap between software architecture analysis and verification and the software product. In the architecture design level, to make sure the design correctness and attack the large scale of complex systems, the compositional verification is used by dividing and verifying each component individually and synthesizing them based on the driving theory. Then for those properties that cannot be verified on the design level, the design model is translated to implementation and runtime verification technique is adapted to the program. This approach can highly reduce the work on the design verification and avoid the state-explosion problem using model checking. Moreover, this approach can ensure both design and implementation correctness, and can further provide a high confident final software product. This approach is based on Software Architecture Model (SAM) that was proposed by Florida International University in 1999. SAM is a formal specification and built on the pair of component-connector with two formalisms – Petri nets and temporal logic. The ACV approach places strong demands on an organization to articulate those quality attributes of primary importance. It also requires a selection of benchmark combination points with which to verify integrated properties. The purpose of the ACV is not to commend particular architectures, but to provide a method for verification and analysis of large scale software systems in architecture level. The future research works fall in two directions. In the compositional verification of SAM model, it is possible that there is circular waiting of certain data among different component and connectors. This problem was not discussed in the current work. The translation of SAM to implementation is based on the restricted Petri nets due to the undecidable issue of high level Petri nets. In the runtime analysis of implementation, extraction of the execution trace of the program is still needed to get a white box view, and further analysis of execution can provide more information of the product correctness.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.