检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:李蜜[1] 庄毅[1] LI Mi;ZHUANG Yi(School of Information Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)
出 处:《计算机技术与发展》2019年第12期21-26,共6页Computer Technology and Development
基 金:国家自然科学基金面上项目(61572253);航空基金XXX专项(20128052064)
摘 要:AADL已经广泛应用于嵌入式软件体系结构的建模与分析,并且已有开源平台OSATE为AADL提供建模、验证与分析工具。但AADL作为一种半形式化建模语言,不能满足严格分析评估软件可靠性、安全性等非功能属性的要求。因此需要将AADL可靠性模型转换为形式化模型。Z语言是一种严格的形式化建模语言,在进行严格可靠性评估时具有很好的支持能力,并且已有工具提供Z模型的检测功能。为实现AADL可靠性模型到Z形式化模型的自动转换,文中设计了AADL到形式化语言Z的模型转换规则,并基于XSLT实现了AADL到Z的自动转换工具。最后通过一个自动驾驶子系统的实例,证明了所提出的自动转换方法的有效性,并且通过将AADL模型与转换结果进行对比,说明了转换方法的正确性。AADL has been widely used in the modeling and analysis of embedded software architectures,and the open source platform OSATE has provided modeling,verification and analysis tools for AADL.However,AADL,as a semi-formal modeling language,cannot meet the requirements of rigorous analysis and evaluation of non-functional attributes such as software reliability and security.Therefore,it is necessary to convert the AADL reliability model into a formal model.The Z language is a rigorous formal modeling language that has excellent support for rigorous reliability assessments and tools that provide Z-model detection capabilities.In order to realize the automatic conversion of AADL reliability model to Z formal model,we design the model conversion rules of AADL to formal language Z,and implement the automatic conversion tool of AADL to Z based on XSLT.Finally,an example of an automatic driving subsystem is used to prove the effectiveness of the proposed automatic conversion method.By comparing the AADL model with the conversion results,the correctness of the conversion method is illustrated.
分 类 号:TP301[自动化与计算机技术—计算机系统结构]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:18.222.183.98