%0 Journal Article
%T 基于时间抽象状态机的aadl模型验证
%A 杨志斌？
%A 胡凯？
%A 赵永望？
%A 马殿富？
%A Jean-Paul
%A BODEVEIX？
%J 软件学报
%P 202-222
%D 2015
%R 10.13328/j.cnki.jos.004776
%X 提出了一种基于时间抽象状态机(timedabstractstatemachine,简称tasm)的aadl(architectureanalysisanddesignlanguage)模型验证方法.分别给出了aadl子集和tasm的抽象语法,并基于语义函数和类ml的元语言形式定义转换规则.在此基础上,基于aadl开源建模环境osate(opensourceaadltoolenvironment)设计并实现了aadl模型验证与分析工具aadl2tasm,并基于航天器导航、制导与控制系统(guidance,navigationandcontrol)进行了实例性验证.
%K aadl(architecture
%K analysis
%K and
%K design
%K language)
%K tasm(timed
%K abstract
%K state
%K machine)
%K 模型转换
%K 形式验证
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4776&flag=1