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

随着Internet和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.