基于场景规约的中断驱动系统的建模与验证技术研究

In recent years, with the popularity of intelligent terminal products, interrupt-driven systems have become increasingly widespread. The correctness guarantee of interrupt-driven system has turned into an urgent need. However, interrupt uncertainty, preemption and priority queuing pose great challenges to the modeling and verification of interrupt-driven systems, and so far there is no satisfactory solution. Thus, this project plans to focus on modeling and verification techniques for interrupt-driven systems. Scenario-based specification is a modeling language widely used in industry. Through the research on the modeling of interrupt-driven systems with scenario-based specification, the description language for system properties, and the design and implementation of verification algorithms, this project intends to achieve concise and perspicuous modeling, flexible and easy-to-use property description, and automatic and efficient verification, thus providing a theoretical reference and technical support for the correctness guarantee of interrupt-driven systems.

近年来，随着以嵌入式系统为特征的智能终端产品的普及，中断驱动系统的应用变得越来越广泛，中断驱动系统的正确性保障成为了一个迫切的需求。中断的不确定性、抢占性和优先级排队等特点使得中断驱动系统建模和验证的问题十分困难，目前国内外尚无较好的解决方案。本项目重点研究中断驱动系统的建模与验证技术。场景规约是工业界广泛使用的建模语言，本项目拟通过基于场景规约的中断驱动系统的建模、中断驱动系统性质的描述语言和系统验证的算法设计实现等方面的研究，实现中断驱动系统简明易懂的建模、灵活易用的性质描述和自动高效的验证，从而为中断驱动系统的正确性保障提供理论参考和技术支持。

近年来，随着以嵌入式系统为特征的智能终端产品的普及，中断驱动系统的应用变得越来越广泛，中断驱动系统的正确性保障成为了一个迫切的需求。中断的不确定性、抢占性和优先级排队等特点使得中断驱动系统建模和验证的问题十分困难，目前国内外尚无较好的解决方案。本项目重点研究了中断驱动系统的建模与验证技术。基于UML2序列图提出了中断序列图，可直观有效第对中断驱动系统建模；基于线性时序逻辑提出了可统一描述中断驱动系统时序与时间性质的描述语言；基于模型转换和SMT理论，实现了对系统模型的全模型和有界验证算法。对现有文献和航天领域的实际案例进行了研究，取得了满意的效果。