检索结果-南通市图书馆

基于NuSMV的AADL模型形式化验证技术

在线全文

学校读者我要写书评

暂无评论

航空学报 2022年第3期43卷 443-458页

作者：刘畅蒋永平马春燕张涛中国航空无线电电子研究所上海200233 西北工业大学软件学院西安710072

结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先,覆盖AADL模... 详细信息

结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先,覆盖AADL模型的所有软件构件和行为特征,提出了AADL模型到NuSMV模型的映射规则和转换算法;其次,采用图同构方法分析了转换算法的正确性;然后,在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述,以验证AADL模型中安全性、活性和嵌套模态配置的正确性;最后,以飞行控制系统为例,详细阐释了基于NuSMV的AADL模型形式化验证方法,并给出验证属性的统计信息。

关键词： AADL模型 NuSMV 形式化验证模型转换飞行控制系统

在线全文

学校读者我要写书评

暂无评论

古建筑三维语义模型转换方法研究

测绘科学 2023年第2期48卷 227-236页

作者：张文元刘润桦华中师范大学国家文化产业研究中心武汉430079

针对建筑信息模型(BIM)领域古建筑语义模型缺乏建筑物周围环境信息,不利于建筑模型与地形数据的集成、共享、空间分析等问题,该文提出了一种古建筑工业基础类(IFC)模型转换为城市地理标记语言(CityGML)扩展模型的方法。比较分析IFC和Cit... 详细信息

针对建筑信息模型(BIM)领域古建筑语义模型缺乏建筑物周围环境信息,不利于建筑模型与地形数据的集成、共享、空间分析等问题,该文提出了一种古建筑工业基础类(IFC)模型转换为城市地理标记语言(CityGML)扩展模型的方法。比较分析IFC和CityGML两种标准在建筑物模型实体语义和几何表达方面的差异,在对CityGML标准定义的建筑物模型进行语义扩展的基础上,从语义映射和几何转换两方面实现古建筑室内外几大类典型构件IFC模型到CityGML语义扩展模型的转换方法。实验结果证实了该文方法的有效性,该方法能够实现高精度、语义丰富的古建筑CityGML模型快速构建,有利于促进古建筑文化遗产数字化保护。

关键词：古建筑 IFC CityGML 语义扩展模型转换

一种SysML到SLIM模型的自动构造方法

在线全文

学校读者我要写书评

暂无评论

小型微型计算机系统 2023年

作者：郭沣慧胡军王立松肖曦谷青范软件新技术与产业化协同创新中心中国航空无线电电子研究所南京航空航天大学计算机科学与技术学院

近年来，基于模型的安全性分析（MBSA）是复杂系统建模与分析领域备受关注的分析方法。由于系统架构建模语言SysML缺少形式化的语义语法，不支持MBSA方法，而SLIM语言具备形式化语义和语法，支持安全性分析，所以本文提出了一种基于ATL... 详细信息

近年来，基于模型的安全性分析（MBSA）是复杂系统建模与分析领域备受关注的分析方法。由于系统架构建模语言SysML缺少形式化的语义语法，不支持MBSA方法，而SLIM语言具备形式化语义和语法，支持安全性分析，所以本文提出了一种基于ATL（ATLAS Transformation Language）的SysML模型到SLIM模型的自动构造方法SysML2SLIM。首先，搭建系统的SysML模型并导出为XMI文件格式，根据SysML规约文档以及SLIM的BNF范式构建元模型，并建立模型元素映射规则；其次，设计源模型文件处理算法，在保留必要标签信息的情况下，获得规范的SysML源模型文件；接下来，根据元素映射规则利用ATL编写转换规则文件，调用ATL引擎完成构造；然后，给出模型转换的正确性证明的推导；此外，对集成SysML2SLIM方法的工具MSAT进行介绍；最后，对航天器中的电池传感器系统进行分析，验证了自动构造方法的有效性。

关键词： SysML SLIM 模型转换 ATL

基于UMCS树的UML类图的混合相似性度量

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

计算机应用 2024年第3期44卷 883-889页

作者：袁中臣马宗民沈阳工业大学化工过程自动化学院辽宁辽阳111004 南京航空航天大学计算机科学与技术学院南京211106

软件重用是基于给定条件从存储库中检索以前开发的软件产品,检索基于相似性度量。UML(Unified Modeling Language)类图被广泛应用于软件设计,UML类图重用作为软件设计重用的核心而备受关注。因此,对UML类图的相似性开展研究。类图包含... 详细信息

软件重用是基于给定条件从存储库中检索以前开发的软件产品,检索基于相似性度量。UML(Unified Modeling Language)类图被广泛应用于软件设计,UML类图重用作为软件设计重用的核心而备受关注。因此,对UML类图的相似性开展研究。类图包含语义和结构信息。目前,UML类图的相似性研究主要集中在语义,也有个别讨论结构相似性,但没有考虑将语义和结构相结合。因此,提出一种结合语义和结构的混合相似性度量。鉴于UML类图的非形式化特征,将UML类图转换成图模型,搜索最大公共子图列表,构建了最大公共子图树,提出一个基于最大公共子图序列的混合相似性度量方法。针对概念公共子图和结构公共子图分别定义了语义匹配和结构匹配,并开展了相似性对比和基于相似性的分类质量比较实验,实验结果验证了所提出方法的优势。

关键词： UML类图模型转换混合相似性最大公共子图树语义匹配结构匹配

基于AADL的混合关键系统随机错误与突发错误安全性分析

在线全文

学校读者我要写书评

暂无评论

软件学报 2024年

作者：魏晓敏董云卫孙聪李兴华马建峰西北工业大学计算机学院西安电子科技大学网络与信息安全学院

许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system, MCS). MCS通常需要在指定的关键性(criticality)等级状态下运行,但是它们可能会受到一些危害的影响,这些危害可能会导致随机错误和突发错误,进一步导致执行线程中止,... 详细信息

许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system, MCS). MCS通常需要在指定的关键性(criticality)等级状态下运行,但是它们可能会受到一些危害的影响,这些危害可能会导致随机错误和突发错误,进一步导致执行线程中止,甚至导致系统故障.目前的研究仅集中于对MCS的可调度性分析,未能进一步分析系统安全性,未能考虑线程之间的依赖关系.以随机错误和突发错误为研究对象,提出一种集成故障传播分析的基于架构的MCS安全分析方法.使用架构分析和设计语言(architecture analysis and design language, AADL)刻画构件依赖关系.为了弥补AADL的不足,创建新的AADL属性(AADL突发错误属性),并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程.为了将概率模型检查应用于安全分析,提出模型转换规则和组装方法,从AADL模型推导出PRISM模型.建立了两个公式,分别获得定量安全属性以验证故障发生的概率,以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析.最后,以动力艇自动驾驶仪(power boat autopilot, PBA)系统为例,验证了该方法的有效性.

关键词：混合关键系统突发错误模型转换安全性分析概率模型检验

利用IFC和CityGML进行地下空间模型转换——以城市综合管廊为例

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

武汉大学学报（信息科学版） 2020年第7期45卷 1058-1064页

作者：赵强何陈照杨世植方廷勇朱曙光安徽建筑大学环境与能源工程学院安徽合肥230601 安徽省智慧城市工程技术研究中心安徽合肥230601 中国科学院安徽光学精密机械研究所安徽合肥230031

分析了工业基础类(industry foundation classes,IFC)和城市地理标记语言(city geography markup language, CityGML)在几何表达、语义信息等方面的异同;以综合管廊为对象,建立IFC综合管廊模型转换为CityGML模型的流程和方法,进行语义... 详细信息

分析了工业基础类(industry foundation classes,IFC)和城市地理标记语言(city geography markup language, CityGML)在几何表达、语义信息等方面的异同;以综合管廊为对象,建立IFC综合管廊模型转换为CityGML模型的流程和方法,进行语义提取、几何以及坐标系统的转换。通过六盘水城市综合管廊模型转换进行验证,结果表明,所建立的IFC管廊模型与CityGML管廊模型映射规则可实现IFC管廊模型向CityGML模型的转换,同时转换后的CityGML管廊模型包含由IFC模型提取的属性信息,可用于三维地理信息系统(three dimension geographical information system, 3DGIS)与建筑信息模型(building information modeling,BIM)的集成,有助于促进城市地下管廊全生命周期管理。

关键词： 3DGIS BIM IFC CityGML 综合管廊模型转换

基于ZRM-MDH模型转换的串联机器人运动学参数标定

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

农业机械学报 2021年第3期52卷 382-389页

作者：乔贵方万其吕仲艳康传帅孙大林温秀兰南京工程学院自动化学院南京211167 东南大学仪器科学与工程学院南京210096

运动学参数误差是影响工业机器人绝对定位精度的主要因素,通过误差标定能够有效地提高工业机器人的精度。运动学模型的完整性、连续性与冗余性对运动学参数的辨识精度影响较大。为尽可能地提高机器人的标定精度,并易于实现机器人误差补... 详细信息

运动学参数误差是影响工业机器人绝对定位精度的主要因素,通过误差标定能够有效地提高工业机器人的精度。运动学模型的完整性、连续性与冗余性对运动学参数的辨识精度影响较大。为尽可能地提高机器人的标定精度,并易于实现机器人误差补偿,本文提出一种基于ZRM-MDH模型转换的机器人运动学参数标定方法。首先,基于零参考模型(ZRM)建立TX60型串联工业机器人的位姿误差模型,结合测量位姿误差辨识ZRM的参数;其次,基于圆点分析法将ZRM转换成MDH模型。在TX60型机器人前侧工作区域内任意选择50个测量点,实施运动学参数误差标定。实验表明,基于MDH模型标定后的机器人平均综合定位误差为0.081 mm,而经过ZRMMDH模型转换后的机器人平均综合定位误差为0.062 mm。为验证标定方法的稳定性,在TX60型机器人前侧工作区域内,选择5个区域实施运动学参数误差标定,结果表明,基于ZRM-MDH模型转换获得的标定精度稳定性相对较好。

关键词：串联机器人零参考模型 MDH模型模型转换激光跟踪仪

基于特征分解的半空间构造实体几何模型转换算法

在线全文

学校读者我要写书评

暂无评论

计算机集成制造系统 2021年第5期27卷 1382-1389页

作者：赵瑛峰刘检华武林林马江涛北京理工大学机械与车辆学院数字化制造研究所北京100081

为了解决大型通用粒子输运计算程序MCNP建模困难的问题,提出一种基于特征分解的BRep模型到MCNP半空间构造实体几何(CSG)模型转换算法。该算法定义了半空间转换元的概念,并以此概念为基础,提出以几何特征和拓扑结构为依据的BRep模型识别... 详细信息

为了解决大型通用粒子输运计算程序MCNP建模困难的问题,提出一种基于特征分解的BRep模型到MCNP半空间构造实体几何(CSG)模型转换算法。该算法定义了半空间转换元的概念,并以此概念为基础,提出以几何特征和拓扑结构为依据的BRep模型识别方式;根据不同的特征,算法构造了合适的分解面,将Brep模型分解为半空间转换元组合,并为存在半空间描述歧义的转换元添加了合适的辅助面。通过多个模型的算法测试展示了算法的模型转换能力,通过效率测试验证了算法的计算效率,结果证明所提算法大幅提高了MCNP输入文件的制作效率。

关键词：半空间构造实体几何(CSG)模型模型转换模型分解 MCNP程序

基于限定中文自然语言需求的SysML模型自动生成方法

在线全文

学校读者我要写书评

暂无评论

计算机研究与发展 2021年第4期58卷 706-730页

作者：鲍阳杨志斌杨永强谢健周勇岳涛黄志球郭鹏南京航空航天大学计算机科学与技术学院南京211106 高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学) 南京211106 航空工业计算所西安710065

模型驱动开发方法逐渐成为安全关键信息物理融合系统(safety-critical cyber-physical system,SC-CPS)设计与开发的重要手段.然而,安全关键信息物理融合系统需求往往是通过自然语言描述的,如何自动化或半自动化链接自然语言需求和基于... 详细信息

模型驱动开发方法逐渐成为安全关键信息物理融合系统(safety-critical cyber-physical system,SC-CPS)设计与开发的重要手段.然而,安全关键信息物理融合系统需求往往是通过自然语言描述的,如何自动化或半自动化链接自然语言需求和基于模型驱动的系统设计与开发过程是目前面临的重要挑战.面向安全关键信息物理融合系统,提出基于限定中文自然语言需求的SysML模型自动生成方法RNL2SysML.首先,为了降低自然语言需求表达的二义性,提出一种结构化的限定自然语言需求模板进行需求规约,并通过基于人工智能的(AI)安全关键信息物理融合系统术语提取和推荐方法,对系统需求中的领域术语和数据字典加以自动提取,提高限定自然语言需求规约工作的自动化程度.然后,给出限定自然语言需求规约到SysML系统设计模型的转换方法.最后,基于开源工具Papyrus对所提方法进行了原型工具实现,并通过航空领域的飞机空气增压系统(airplane air compressor system)案例验证了方法的有效性和实用性.

关键词：安全关键信息物理融合系统模型驱动开发方法系统建模语言术语推荐限定自然语言需求模型转换