面向航电系统的形式化建模与验证

发布时间：2017-12-11 12:19

  本文关键词：面向航电系统的形式化建模与验证

  更多相关文章： AADL 数据约束 连续时间 ZIA DT-PZIA 模型检测

【摘要】：结构分析和设计语言(architecture analysis and design language)是嵌入式实时系统的一种体系结构描述语言标准,广泛应用于航空宇航工业中对安全关键应用系统的建模。确保建模的正确性及其可靠性成为当前AADL研究的一大热点领域。AADL在建模过程中对线程、进程、行为附件、连接等进行了一定的语义描述,但对于模型中的状态及状态变迁的数据约束性质的描述略显不足,而形式规格说明语言Z语言在数据约束的描述方面具有显著的作用,通过对AADL进行Z语言扩充,使得建立的模型可以更好的转换为形式化模型,从而使得模型检测这一形式化验证技术可用于转换后的模型。模型检测方法作为一种严格的以数学为基础的验证技术,能够精确、抽象、简明地规范和验证软件系统及其性质,有效的确保软件的安全性和可靠性。本文在AADL的基础上扩展Z,提出了Z-AADL规范,即将Z形式规格说明语言与AADL规范相结合形成一种可以描述带数据约束实时系统的形式化规范—Z-AADL。然后,提出一种描述带数据约束实时系统的形式化规范?基于连续时间的ZIA规范,并将Z-AADL转换为基于连续时间的ZIA规范模型,这样在实现了对基于连续时间的ZIA模型的模型检测的同时,其实质上就是对Z-AADL的模型检测。本文给出了一种模型检测算法,适用于连续时间的ZIA模型,并通过一个实例验证,详细的阐述了文章方法的可行性和有效性。另外,一般意义的ZIA缺乏刻画系统概率约束方面的能力,鉴于此,文章在传统的ZIA上扩展了概率性质提出一种基于离散时间的概率ZIA规范?DT-PZIA,弥补了传统ZIA只能够刻画系统中的行为和状态,而不能刻画概率性质的缺陷。为了解决航电系统中的一个子系统,即概率系统中的概率约束问题,本文还介绍了一个用于表达系统中性质的具体度量值的形式化语言,与传统的时序逻辑相比,这种逻辑不仅可以表达系统的时序性质,而且可以表达系统的度量性质。最后本文同样给出了检测算法,其适用于离散时间的概率系统的模型检测,并给出了实例以证明方法的可行性。
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：V243

【相似文献】

中国期刊全文数据库 前10条

1 王远达;宋笔锋;姬东朝;史彦斌;;军机航电系统实现两级维修的关键技术[J];火力与指挥控制;2009年08期

2 蒋国峰;扈胜超;;航电系统外场保障实习台的设计与研究[J];航空计算技术;2010年05期

3 张U，

本文编号：1278437