题目：基于Event-B的实时特性描述及精化方法研究

把形式化方法融入到软件开发过程的各个阶段已经成为近年来的一个研究热点。采用形式化技术，可以极大地减少软件开发早期阶段的错误，进而提高软件开发效率。这对安全关键软件非常重要。目前形式化方法的主要研究内容是形式规约，即用具有精确语义的形式语言书写的程序功能描述作为验证程序是否正确的依据。本文研究的Event-B方法是一种系统级建模分析的形式化方法。它使用集合论作为建模语言，通过精化在不同的抽象等级来描述系统，同时使用数学方法来验证精化过程间的一致性。Event-B是B方法的扩充，更加适用于大型的、分布式、并行的软件系统。同时，Event-B方法相较于其他形式化方法的优势在于它有Rodin工具作为建模支持。 时间特性是实时系统的重要属性，系统的可靠性很大程度上取决于实时性。然而，现阶段在使用Event-B进行实时系统建模的过程中，还没有形成统一的实时特性描述和精化方法，如果对时间特性的描述没有统一规范，那么会导致模型不易读，容易产生不一致，重用性差等一系列问题。 本文首先介绍了Event-B方法以及实时特性形式化建模的发展现状，指出了基于Event-B的实时特性建模是未来的重要发展方向。其次，本文结合了UML-B状态图的表示法建立基于Event-B的实时特性描述，探索了两种不同的状态表示法，选用适合Event-B描述和精化的方式并完成对六类常见的实时约束和时序关系的描述。而后本文借鉴了Event-B事件精化的建模思想，确定了基于Event-B实时特性精化的三种精化模式（顺序、并发和复合状态精化）并分别对各类实时特性完成这三种精化。最后，针对TCAS防撞系统案例，结合本文研究成果对TCAS的告警功能及其实时特性在Rodin平台下进行描述和精化，并验证方法的正确性和易用性。