An engineering process for the verification of real-time systems

The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses delay and deadline to define temporal behaviour, notions of rely and guarantee to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.     

基于时间扩展的ASEHA建模与验证

为了有效地分析实时系统,在原计算模型的基础上,引入了时钟变量,在迁移上增加了时钟约束,扩展了异步扩展层次自动机的语义.运用基于时间扩展的ASEHA,分析了ATM系统,建立了用户和ATM的模型,并使用模型检测工具UPPAAL对模型进行验证,从无死锁、活性及可达性性质出发,验证了ATM系统的安全性.实验表明,提出的基于时间...     

多处理器实时系统可调度性分析的UPPAAL模型

随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用UPPAAL验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息.     

一种基于UPPAAL的Web服务组合模型检测方法

Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYG/ADL对Web服务组合进行描述的基础上,将其实时描述部分XYZ/RE转换至时间自动机模型,组合后系统应满足的性质用分支时序逻辑CTL公式表示,最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证。     

基于时间自动机的实时系统建模及验证

实时系统必须在一个事先定义好的时间限制内对来自外部或内部的事件进行响应,如何有效验证实时模型的正确性和安全性是一个难点.文章通过多个时间自动机来模拟实时系统中的各个对象,并用UPPAAL对模型进行验证,减少了模型验证的状态搜索空间,为实时嵌入式系统开发和验证提供了一种可行、安全的控制机制.实验结果显示了系统的有效性.     

混杂系统的扩展时间自动机模型及验证研究

混杂系统复杂度高且涉及领域广,没有通用的方法来解决分析、设计等问题。为解决一类工业控制混杂系统的建模和验证问题,对时间自动机进行了语义扩展,使其含有连续变量以及映射在其上的约束,使用扩展后的时间自动机对此类混杂系统进行建模,采用验证工具UPPAAL进行模型分析模拟,并使用简化的CTL对系统需求规范进行验证。具体实例研究表明,该方法对于分析设计一类混杂系统具有可行性和有效性。     

基于UPPAAL在线支付系统的安全性验证

随着电子商务的不断发展,消费者对于在线支付系统的服务质量要求越来越高,支付系统不仅要高速完成每笔交易,更要保证支付过程的安全性。在线支付是电子商务的核心功能模块,而这个核心模块又由各个地理位置上分离的各个子模块组成,在该文中会对四个主要子模块进行建模,分析各模块之间的依赖关系及超时的扩散效应,通过UPPAAL对建模后的系统进行模型检测。经实验验证,所设计的支付系统模型可以在产生某个模块的超时后依然能满足安全性。     

RASA的多Agent交互协议研究

RASA是2007年Tim Miller提出的一个MAS（Multi-agent System）交互协议框架,这个框架已被证明可以更好地促进MAS的交互,但此框架并不支持MAS的并发。利用了一种冲突优先方式,引入了效益评价函数来解决其状态无法确定的问题,并扩展了RASA的定义来支持其并发,随后采用了一种基于时间自动机的自动验证工具UPPAAL,利用一个简单的拍卖协议来验证这种方法的可行性。最后利用RASA语言描述了一个简单的协商协议和一个拍卖协议,以显示RASA协议的良好特性。     

基于 UPPAAL 的手机功耗流量建模方法研究

由于智能手机电池容量有限,应用程序的功耗是其主要消耗之一,因为应用程序可能会产生意外功耗或能源错误,其中 大多数是设计错误。 为分析应用程序功耗和通信流量特性,提出使用基于模型检测的功耗流量分析方法。 把手机各硬件组件 作为研究对象,对时间自动机模型进行扩展,使用模型检测工具 UPPAAL 构建模型。 该方法可以在开发的早期阶段使用,为应 用程序的设计和分析提供了异步功耗的形式化模型。 设计 WiFi 省电模式实例进行研究分析,验证分析该模型的主要属性,然 后用手机应用 QQ 进行了实验对比。 分析结果表明,该模型符合一般模型验证需求,与 PowerTutor 的测量结果相比,其相对误 差均低于 7%,能为复杂手机系统提供可参考的建模分析思路。     

基于模型检测的不可靠环境下电子商务协议分析

随着网络的大规模应用,电子商务协议的运行环境越来越不可靠。本文用模型检测的方法分析了不可靠环境下电子商务协议的安全性质。结果表明：安全的电子商务协议在不 可靠环境下运行时有可能不再保持安全性质。当安全性质违背时,借助由自动验证工具UPPAAL生成的消息序列查找原因并对协议进行修改。经验证,修改后的协议在不可靠的环
境下保持安全性质。