Advancing the applicability of model checking and FSM-based testing techniques to complex software systems

点击翻译按钮获取中文摘要

With the widespread use of the Internet and web applications, software systems are becoming more and more pervasive in our society. To make sure we can produce highly reliable, secure and more sophisticated software systems to meet our increasing demands and with lower cost, we need effective software engineering methods and techniques applied during the software development for the software quality assurance. The advance of the current state-of-the-art methods and techniques for the correctness and reliability of our software products lies heavily on methodologically sound solutions. In this regard, formal verification and formal testing techniques have made significant contributions to the establishment of the theoretical foundation of software development over the past two decades. However, despite of the great effort we made, there is still a big gap between the theory and its practical application to most of our real life software systems. Many essential issues are still left to be resolved. The proposed work is to address some of these important issues, with focus on significantly improving the applicability of existing formal verification and formal testing techniques towards large-size applications. In order to apply formal verification and formal testing techniques, it is essential that we have the system under consideration properly modeled. The proposed work also includes the formal modeling of some widely used and complex systems such as web systems, middleware systems, and web services. The difficulties of the work come from the fact that these systems are both complex and dynamically evolving. On the other hand, they are gaining increased popularity, and their advances indeed represent the emerging new technologies. Applying formal verification and formal testing techniques on these systems are extremely important as they are strongly affecting the quality of our daily life.