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

提高模型检查和基于 FSM 的测试技术对复杂软件系统的适用性

• 批准号: 203248-2006
• 负责人: Chen, XiaoJun
• 金额: $ 1.81万
• 依托单位: University of Windsor
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2007
• 资助国家: 加拿大
• 起止时间: 2007-01-01 至 2008-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=366638
• 关键词: Advancing; applicability; model; checking; FSM

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.

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