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

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

• 批准号: 203248-2006
• 负责人: Chen, XiaoJun(Jessica)
• 金额: $ 1.81万
• 依托单位: University of Windsor
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2008
• 资助国家: 加拿大
• 起止时间: 2008-01-01 至 2009-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=392757
• 关键词: 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 服务。这项工作的困难在于这些系统既复杂又动态发展。另一方面，它们越来越受欢迎，它们的进步确实代表了新兴技术。在这些系统上应用形式验证和形式测试技术非常重要，因为它们强烈影响我们的日常生活质量。