论文部分内容阅读
随着现代化的推进以及通信等技术的发展,计算机软件已广泛应用于各类安全攸关的系统中。在安全攸关实时系统的设计中,系统的复杂性不断的提升,使用传统的软件工程的方法,已经不能满足日益增长的复杂系统设计的需要。目前,通过模型驱动架构(Model Driven Architecture,MDA)的开发方法,利用特殊领域(如航空电子领域)体系结构分析与设计语言(Architecture Analysis and Design Language, AADL)设计各种安全攸关实时软件系统,已经取得了良好的效果。但是,由于AADL工具链本身并不是很完善,在实际的开发应用中,会遇到不能对使用AADL建立的安全攸关实时系统模型进行仿真模拟和性质验证的情况。为此,本文围绕这一问题开展了相关研究与应用。相关的研究工作如下:第一,设计了一种从AADL模型到时间状态机网络模型的转换规则。首先根据最小化原则、可描述性原则、可实现性原则从AADL全集中选择并设计了一个满足安全攸关实时系统设计需求的子集,并基于此子集设计并实现了 AADL模型(含AADL 的行为附件 BA)到时间状态机网络 UPPAAL(UPPSALA University and AALBORG University)工具的转换规则,以利用时间状态机网络丰富的工具与资源对AADL模型进行分析。第二,设计了一种从AADL模型的行为附件BA到时间状态机网络模型的转换规则。首先根据最小化原则、可描述性原则、可实现性原则从已选取的AADL子集的行为附件中选取了一个满足安全攸关实时系统设计需求的子集,并基于此子集.设计并实现了行为附件到时间状态机网络UPPAAL工具的转换规则。第三,针对AADL模型到时间状态机网络模型的转换规则设计中所遇到的转换规则编写过于复杂的问题,提出并实现了能够根据已经设计完成的时间状态机网络模型自动生成ATL (Atlas Transformation Language)转换规则代码的规则生成器。本文根据设计好的AADL子集,按照最小化原则、可描述性原则、可实现性原则对UPPAAL工具的元素进行选择并设计了一个满足安全攸关实时系统设计需求的UPPAAL子集,并基于此子集设计并实现了从UPPAAL状态机模型到ATL转换规则的生成器。第四,基于Eclipse插件技术与XMI等技术,设计并实现了一种AADL模型到UPPAAL模型的转换器。最后,使用所设计的AADL模型到UPPAAL模型的转换工具系统对两个实际案例进行了测试与应用,该系统能够对实际案例的模型进行转换与验证。综上所述,本文设计并实现的AADL到UPPAAL的转换的方法与集成的工具能够转换与验证模型驱动软件开发中模型的设计,在安全攸关实时系统的开发中具有良好的效果。