tailieunhanh - A Framework for Modeling and Modular Verification of Component-Based System Designs

This paper introduces a framework for modeling and verifying safety properties of component-based systems (CBS) by extracting their models from designs in the form of UML sequence diagrams. Given UML sequence diagrams of a CBS, the framework extracts regular expressions exactly describing behaviors of the system. | VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 2 (2016) 31–42 A Framework for Modeling and Modular Verification of Component-Based System Designs✩ Chi-Luan Le1,2,∗ , Hoang-Viet Tran1 , Pham Ngoc Hung1 1 Faculty of Information Technology, VNU University of Engineering and Technology, E3 Building, 144 Xuan Thuy Street, Cau Giay, Hanoi, Vietnam 2 Faculty of Information Technology, University of Transport Technology, H1 Building, 54 Trieu Khuc Street, Thanh Xuan, Hanoi, Vietnam Abstract This paper introduces a framework for modeling and verifying safety properties of component-based systems (CBS) by extracting their models from designs in the form of UML sequence diagrams. Given UML sequence diagrams of a CBS, the framework extracts regular expressions exactly describing behaviors of the system. From these expressions, the proposed framework then generates accurate operation models represented by labeled transition systems (LTSs). After that, these models are used to modular check whether given designs satisfy required safety properties by using the assume-guarantee reasoning paradigm. This framework is not only useful for modeling and verifying designs at design phase, but also for effectively rechecking the correctness of CBS in the context of software evolution. Implemented tools and experimental results are also presented in order to show the feasibilities and effectiveness of the proposed framework. Received 01 December 2015, revised 13 January 2016, accepted 14 January 2016 Keywords: Software Modeling, Sequence Diagram Analysis, Assume-Guarantee Verification, Model Checking. 1. Introduction difficult to be applied in practice because generating models for systems is a hard problem. The method presented in [12] had mentioned a way of using the model generated from the design artifacts to check safety properties of the system implementation. However, the paper did not describe in details how to use and what kind of artifacts of design