Bộ môn Công Nghệ Phần Mềm xin mời các cán bộ Khoa CNTT, các thày/cô và học viên cao học có quan tâm tham dự seminar khoa học:
– Người trình bày: TS. Phạm Ngọc Hùng
– Đề tài: Assume-Guarantee Verification of Evolving Component-Based Software
– Thời gian: 14h00 ~ 15h00, ngày 30/9/2009 (thứ tư)
– Địa điểm: Phòng 312, E3.
Abstract:
Assume-guarantee verification method has been recognized as a promising approach to verify component-based software (CBS) with model checking. The method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. This method allows us to decompose a verification target into components so that we can model check each of them separately. Model-based verification methods in general and the assume-guarantee verification method in particular of a system are performed with respect to its model which exactly describes the behavior of the system. Thus, we have to obtain the accurate model of the system before applying the verification techniques. However, these methods generally assume that the ways to obtain the model and its correctness are available. This means that the model-based verification methods assume the availability and correctness of the model which describes the behavior of the system under study. Nonetheless, this assumption may not always hold in practice due to the modelling errors, bug fixing, etc. In addition, evolving of the existing components of CBS is a daily and unavoidable activity during the software life cycle. Therefore, even if the assumptions hold, the model could be invalidated when the software is evolved by adding or removing some behaviors. Unfortunately, the consequence of these activities is the whole evolved software must be rechecked. The purpose of this research is to provide an effective approach for modular verification of evolving component-based software systematically in the context of the component evolution. When a component is evolved after adapting some refinements, the proposed approach only focuses on this component and its model in order to update the model and to recheck the whole evolved system. The approach also reuses the previous verification results and the previous models of the evolved components to reduce the number of steps required in the model update and modular verification processes.