论文部分内容阅读
嵌入式实时系统多数应用在安全性要求较高的场合，因此需要保证系统的正确性。复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质。如何为嵌入式实时系统的开发人员提供界面友好、易于使用，又能对设计模型进行精确验证的工具一直是软件工程研究中的难点。
现有许多研究都试图通过结合UML与形式化方法的优点，提供一种兼备易用性和精确性的软件开发方法，这些方法一般先使用UML对系统进行建模，然后将UML图形转换成相应的形式化规范语言，并使用相应工具进行验证。现有的研究中大部分都是对静态属性的验证，在动态属性方面的研究比较少。而嵌入式实时系统的两大特点是反应性和实时性，因此研究动态属性的验证更有意义。
本文研究了将UML励态属性模型转换到时间自动机映射方法和基于时间自动机的模型检验技术，具体分为两部分：第一部分建立了从UML状态图和顺序图转换到时间自动机的映射规则。首先用扩展的UML状态图描述系统个体行为，并用扩展的UML，顺序图描述系统对象间的交互。再将UML状态图转换为时间自动机，同时借助时间Petri网将顺序图转换为自动机，从而实现系统的严格建模。
第二部分是实时系统的形式验证工作，讨论了时序逻辑和模型检验的基本理论和方法，分析比较了实时系统的验证工具，最后选用实时系统验证工具UPPAAL，实现了门禁系统实例的安全性和活性的验证。