基于活性顺序图的形式化验证方法及工具研究

Research on Formal Verification Method and Verification Tool Based on Live Sequence Chart

摘要:

近年来,形式化验证方法在软件开发过程的作用越来越大；如何充分利用形式化验证方法提高软件系统的可靠性已成为软件开发者及使用者主要关注的问题；总结了近年来基于活性顺序图的形式化验证方法的研究进展,首先介绍活性顺序图的语言及其表达能力与复杂性,然后深入分析现有的基于活性顺序图的形式化验证的关键技术及其典型应用,最后实现一种基于活性顺序图的运行时验证工具,实验证明使用本验证工具进行形式化验证的可行性。

Abstract:

In recent years, the role of formal verification technology in the software development process is growing more and more important. How to use formal verification technology to improve the reliability of software systems is a major concerned problem of software developers and users. This paper summarizes the progress of formal verification method based on Live Sequence Chart recently. In this paper, the language of live sequence chart, its expressive power and complexity are first introduced. Then the existing key technologies and their application of formal verification method based on live sequence chart are analyzed. Finally, the runtime verification tool based on live sequence chart is implemented, experiments show the feasibility of using this verification tool to formal verification.