【摘 要】
：
结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用.为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法.首先,覆盖AADL模型的所有软件构件和行为特征,提出了 AADL模型到NuSMV模型的映射规则和转换算法;其次,采用图同构方法分析了转换算法的正确性;然后,在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述,以验证AADL模型中安全性、活性和嵌套模态配置的正确性;最后
【机 构】
：
中国航空无线电电子研究所,上海 200233;西北工业大学软件学院,西安 710072
论文部分内容阅读
结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用.为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法.首先,覆盖AADL模型的所有软件构件和行为特征,提出了 AADL模型到NuSMV模型的映射规则和转换算法;其次,采用图同构方法分析了转换算法的正确性;然后,在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述,以验证AADL模型中安全性、活性和嵌套模态配置的正确性;最后,以飞行控制系统为例,详细阐释了基于NuSMV的AADL模型形式化验证方法,并给出验证属性的统计信息.
其他文献
利用FDS数值模拟,研究火源位于支路隧道时,交叉隧道间夹角对主隧道内烟气蔓延的影响,分析了主隧道的烟气浓度、烟气层高度和顶棚最高温度分布状况.结果表明,随着角度由90.减小至30°,主隧道交叉口两侧的烟气浓度呈现非对称特点,钝角方向的烟气浓度大于锐角方向的烟气浓度,但是交叉角度对两个方向的烟气层高度的影响不明显.主隧道内钝角方向顶棚下方烟气最高温度大于锐角方向最高温度,钝角方向最高温度随夹角的减小而增大,锐角方向最高温度随夹角的减小而减小.基于烟气蔓延过程的质量和动量守恒分析,揭示了主隧道内烟气浓度、顶棚
针对珠海市某隧道穿越富水地层断层破碎带防水技术难题,基于MIDAS GTS/NX软件对注浆圈厚度、注浆圈范围对隧道位移的影响进行了三维有限元数值分析.结果表明:①随着注浆圈厚度的增加,拱顶沉降和拱脚收敛呈线性降低,注浆厚度为3 m时约能减低50％的拱顶沉降和拱脚收敛;②随着增加注浆圈范围的扩大,隧道沉降和收敛也趋向一致,整体性增强.在此基础上对注浆措施提出了优化建议.
随着我国农业产业结构的调整,玉米的种植面积不断扩大.玉米生产过程中会产生大量的秸秆,如何处置秸秆已经成为当前种植户需要重点解决的一个问题.随着科技水平的进步,一些机械化技术被应用于农业生产,利用机械设备收获玉米秸秆不仅可以提高劳动效率,同时能够减轻农民的负担,实现对秸秆的有效处理.
随着市政排水管网的信息化管理需求日益增强,城市地下排水管网探测技术对提升排水设施的管理水平具有重要意义.通过文献调研,对地下管线探测方法及其适用性研究分析,结合RTK、全站仪管线测量研究现状,认为城市地下排水管网探测数据采集与建库一体化工作的发展需求不可忽视.一体化作业的发展结合云计算和大数据技术,可以实现作业效率的提升以及保证作业流程的标准化,有效保障城市地下排水管网探测作业的开展.
某大桥桥长192 m,上部结构采用6 m×30m装配式预应力混凝土先简支后连续小箱梁,分两联布置,每联3～30 m,共18片预制小箱梁.采用架桥机架设小箱梁,为了研究架桥机过首孔后施工关键工序的可行性,通过对受载箱梁的结构验算、箱梁受纵向水平力的计算和箱梁横向抗倾覆验算,证明架桥机过孔后运梁车在已架设的箱梁上运梁喂梁是安全可行并可以实施的,采取相应的保证措施后,架梁施工更加安全可靠、便捷快速.
地铁隧道在花岗岩全强风化带施工过程中,由于地层强度低、承载力差、抗变形能力弱,若不对其进行有效加固则会使得开挖风险极大.为增强隧道围岩特性,对广州地铁22号线某区间暗挖工程进行了 WSS帷幕注浆加固.工程实践结果表明:注浆形成的浆脉使岩土体的压缩模量增强、渗透系数降低,注浆压力对土体的挤压作用则提高了岩土体的整体性和自稳能力;开挖监测得到拱顶竖向最大沉降为+5.7 mm,地表最大沉降为-27.12 mm,达到了施工安全的目标.现场所采用的加固措施对类似地层的注浆加固治理具有一定的参考意义.
在上承式钢管混凝土结构运营发展过程中,桥梁的破环原因之一为结构失稳破环.拱上立柱上接盖梁下连主拱圈,作为桥梁承上启下的构件,发挥着重要的作用.利用Midas Civil建立有限元模型,研究立柱横向联系型式、立柱刚度、立柱倾斜度对上承式拱桥的稳定性影响,表明增加立柱刚度可以大幅提高全桥稳定性,横向联系型式、立柱倾斜度对全桥稳定性影响较小.同时分析了与立柱相连接盖梁的弯矩、应力变化,当立柱倾斜度为1.5.时,盖梁为最优受力状态.为今后拱桥的设计、施工提供指导.
基于毛细孔含水量变化的混凝土内部相对湿度理论计算模型,建立了考虑内养护剂动态释水的混凝土自干燥计算模型,并与试验结果进行对比.结果表明:该模型实现了对内养护剂动态释水过程的计算,且计算结果与试验结果吻合较好;混凝土强度越高,内养护对自干燥效应改善越显著;采用本模型精确分析可指导内养护混凝土配合比设计.
为提高设计精度并制备具有目标性能的透水混凝土,选择实际工程中的2种典型骨料,用Image Pro-Plus图像表征了骨料球形度,同时测试并计算了透水混凝土骨架结构参数;基于骨料球形度对透水混凝土配合比设计方法进行了修正.结果表明,基于骨料球形度的透水混凝土配合比设计方法可适用于粒形较差的宽级配骨料,能显著提升透水混凝土配合比设计方法的精确性和可靠性,对透水混凝土实际工程应用具有重要指导意义.
通过对硬度异常钢板的生产工艺进行分析发现,钢板中铌含量过高是造成同一生产工艺下钢板硬度异常的主要原因.利用冷轧退火模拟试验装置,模拟了 3种不同铌含量低碳钢板在不同温度条件下的退火过程,通过对比分析样板显微组织和力学性能,研究微量铌对低碳钢退火再结晶组织和性能的影响.结果表明,当钢中含有微量铌元素时,低碳钢的再结晶完成温度显著提升.含铌0.0012％和0.0023％的低破钢要满足T5料的性能要求,退火温度应提高至650℃.