基于时间抽象状态机的AADL模型验证

来源 :软件学报 | 被引量 : 0次 | 上传用户：ren_lian

【摘要】

：

提出了一种基于时间抽象状态机（timed abstract state machine，简称TASM）的AADL（architecture analysis and design language）模型验证方法．分别给出了AADL子集和TASM的抽象语法，并

【作者】

：

杨志斌胡凯赵永望马殿富 Jean-Paul BODEV

【机构】

：

InstitutdeRechercheenInformatiquedeToulouse,北京航空航天大学计算机学院

【出处】

：

软件学报

【发表日期】

：

2015年2期

【关键词】

：

AADL(architecture analysis and design language) TASM(timed ABSTRACT state machin

【基金项目】

：

法国航空航天基金,软件开发环境国家重点实验室自主课题（SKLSDE-2014ZX-09,SKLSDE-2013ZX-30）

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

提出了一种基于时间抽象状态机（timed abstract state machine，简称TASM）的AADL（architecture analysis and design language）模型验证方法．分别给出了AADL子集和TASM的抽象语法，并基于语义函数和类ML的元语言形式定义转换规则．在此基础上，基于AADL开源建模环境OSATE（open source AADL tool environment）设计并实现了AADL模型验证与分析工具AADL2TASM，并基于航天器导航、制导与控制系统

其他文献

混合指标量子群智能社会网络事件检测方法

社会网络错综复杂，如果能够及时发现和预测当前网络可能发生的重大事件并采取有效的处置策略，将具有重大意义．链路预测的理论框架和评价方法为社会网络事件检测提供了一条有效途

期刊

量子粒子群事件检测链路预测社会网络网络演化网络波动性评价quantum particle swarm event detection link

地方债务化解的破产法路径分析--以城投公司为视角

城投债是安全处理地方政府债务的关键。城投公司具有法人的一般属性,能够适用《企业破产法》。但其资产构成具有多元性,因此在破产程序启动条件、申请主体和程序选择上均具有

期刊

地方债务城投公司破产路径

性交导致阴茎海绵体断裂一例报告

男患,40岁,农民。因性交时突感阴茎疼痛肿胀10小时,于93年6月1日8:00时入院。患者于10小时前性交时(男下女上位),突然听到有器物折断样声音,瞬间即感阴茎剧痛、变软,中止性交

期刊