|
|
软件学报 2015
基于时间抽象状态机的aadl模型验证DOI: 10.13328/j.cnki.jos.004776, PP. 202-222 Keywords: aadl(architecture,analysis,and,design,language),tasm(timed,abstract,state,machine),模型转换,形式验证 Abstract: 提出了一种基于时间抽象状态机(timedabstractstatemachine,简称tasm)的aadl(architectureanalysisanddesignlanguage)模型验证方法.分别给出了aadl子集和tasm的抽象语法,并基于语义函数和类ml的元语言形式定义转换规则.在此基础上,基于aadl开源建模环境osate(opensourceaadltoolenvironment)设计并实现了aadl模型验证与分析工具aadl2tasm,并基于航天器导航、制导与控制系统(guidance,navigationandcontrol)进行了实例性验证.
|
