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

随着互联网和Web应用程序的广泛使用，软件系统在我们的社会中变得越来越普遍。为了确保我们能够以更低的成本生产出高可靠性、安全性和更复杂的软件系统，以满足我们日益增长的需求，我们需要在软件开发过程中应用有效的软件工程方法和技术来保证软件质量。目前先进的方法和技术的进步，我们的软件产品的正确性和可靠性在很大程度上取决于方法上健全的解决方案。在这方面，形式化验证和形式化测试技术在过去的二十年里为软件开发的理论基础的建立做出了重大贡献。然而，尽管我们做了很大的努力，理论和它的实际应用到我们的大多数真实的生活软件系统之间仍然有很大的差距。许多重要问题仍有待解决。拟议的工作是解决这些重要问题，重点是显着提高现有的正式验证和正式测试技术对大型应用程序的适用性。为了应用形式验证和形式测试技术，我们必须对所考虑的系统进行适当的建模。所提出的工作还包括一些广泛使用的和复杂的系统，如Web系统，中间件系统和Web服务的形式化建模。这项工作的困难来自于这样一个事实，即这些系统既复杂又动态演变。另一方面，它们越来越受欢迎，它们的进步确实代表了新兴的新技术。对这些系统应用形式化验证和形式化测试技术是非常重要的，因为它们强烈地影响着我们日常生活的质量。

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.