摘要：实时系统由于受时间约束,设计和验证具有很高的挑战性。用多个时间自动机来规范模拟道岔自动控制系统,给出了一种自动化的道岔控制模型(TTCQ),并采用uppaal作为模型验证工具,证明了该模型具有安全性、有效性和可控性。所采用的方法避免了积的等价类状态空间的爆炸,减少了验证的搜索空间,为铁路交通提供了一种可行的、安全的、智能的控制机制。

摘要：提出了一种形式方法用于验证TLM-2.0的设计方案.该方法中TLM-2.0设计方案将被转换成定时自动机形式模型.定义若干种属性,验证将根据这些属性执行,并引入一种模拟事务级设计方案差错的故障模型来评估这些属性.然后这些属性通过使用形式uppaal验证工具在系统的定时自动机表示上针对这些故障被验证.最后通过一个实例研究说明该方法的有效性.

摘要：通过对分散控制计算机联锁系统建模与验证分析,提出在设计早期发现系统存在的未知故障,减少软件系统设计错误,可为分散控制计算机联锁软件的设计提供参考和指导。

摘要：AADL近年来在嵌入式实时系统领域得到了广泛的应用,相对于其他语言能够更好地描述系统的非功能属性,同时支持系统软硬件建模,在基于模型驱动的开发方法下对系统进行建模和分析,用形式化的方法对系统的相关属性进行验证,从而可以在设计阶段发现错误,对保证系统的安全运行和开发效率的提高有着重要意义。对于验证AADL模型可调度性的问题,文中利用时间自动机理论,根据AADL调度模型和时间自动机模型的语义相似性,将AADL模型转换成时间自动机模型,并设计转换插件,通过Eclipse插件开发技术将其集成到AADL建模与分析工具OSATE中。最后在uppaal工具中对转换后的时间自动机模型进行模拟和验证,利用相关性质验证语句等价地对原模型的可调度性进行验证。

摘要：基于时间自动机理论,在uppaal这种目前最先进的实时系统建模分析验证工具中,对RBC系统消息收发进行分析、建模及验证。最终对RBC系统控车消息收发流程的特性进行验证,对于保证RBC系统控车流程的安全性、减少系统开发周期及开发成本都有重要的实际意义。

摘要：近年来,汽轮机控制保护系统面临的安全威胁引起了学术界及工业界的广泛重视。不同于以往针对通信协议的攻击,攻击者逐渐将目标转移到控制器本身上来。为了应对这种新的威胁,学者们开始研究如何对控制器建立有效的模型去刻画、分析这种攻击对系统运行的影响,进而设计及时、有效的防御策略。本文在总结相应研究的基础上,提出一种基于时间自动机的形式化方法对汽轮机控制保护系统进行建模,同时借助uppaal软件,对建立的模型进行仿真及验证。研究表明,本文提出的模型可以较好地描述汽轮机控制保护系统的工作过程,为后续安全问题研究奠定基础。

摘要：在计算机技术、网络技术高速发展的今天,随着电脑硬件的发展,多媒体应用已经进入千家万户,所以流媒体服务器的架构也成为当今IT研究者研究的热点。其中流媒体服务器的媒体订阅部分包含有大量的状态,如果按以前的IF-Else结构加Case结构编程的话,使得程序臃肿而庞大,整个工程难以维护。利用有限状态机来建模媒体订阅部分的状态,并用形式化验证工具UP-PAAL验证模型的正确性,最后使用状态模式编码实现了媒体订阅的状态转换。这样不仅在设计层保证了系统的正确性,而且在实现层保证了易扩展性和可维护性。