AADL进程子集行为语义研究

J4 ›› 2012, Vol. 34 ›› Issue (7): 93-98.

AADL进程子集行为语义研究

苗德成1,2,奚建清2,苏锦钿2

(1.韶关学院数学与信息科学学院,广东韶关 512005;
2.华南理工大学计算机科学与工程学院,广东广州 510006)

收稿日期:2011-12-09 修回日期:2012-03-18 出版日期:2012-07-25 发布日期:2012-07-25
基金资助:
国家自然科学基金资助项目(61103038);广东省教育部产学研结合项目(2010B050800038);韶关学院科研项目(201020704).

Research on Behavioral Semantics for the Subset of the AADL Process

MIAO Decheng1,2,XI Jianqing2,SU Jindian2

(1.School of Mathmatics and Information Science,Shaoguan University,Shaoguan 512005;
2.School of Computer Engineering and Science,
South China University of Technology,Guangzhou 510006,China)

Received:2011-12-09 Revised:2012-03-18 Online:2012-07-25 Published:2012-07-25

摘要/Abstract

摘要：

AADL是一种基于组件的半形式化建模语言,采用结构化方法对大型复杂软件系统的软硬件进行统一建模,有效描述系统的功能行为、非功能属性以及运行时的体系结构动态演化,但其许多问题需要进一步研究与完善。本文首先分析了AADL形式语义研究现状,然后定义了AADL进程子集的形式语言,建立了AADL进程子集通信模型,通过对事件的形式化定义和分析体现了事件在系统状态转变过程中的重要作用,对AADL进程子集行为语义进行了研究。与相关研究成果的对比说明了本文的优势。本文为AADL语言及其形式语义的发展提供了一种有益的参考,进一步完善大型复杂软件系统体系结构建模与分析技术。

关键词: 行为语义, 形式语言, AADL, 事件, 体系结构

Abstract:

AADL is a semiformal modeling language based on components, which models software and hardware for largescale complex software systems uniformly by structured description, and describes effectively system functional behaviors, nonfunctional attributes and architecture dynamic evolution in runtime, but some questions of AADL are required to further stduy and improve. This paper analyzes firstly the status quo of research for the AADL formal semantics, defines the formal language for the subset of the AADL process, makes a communication model for the subset of the AADL process, defines the concept of event formally, and clarifies the important role of event during the system status transformation, studies the behavioral semantics for the subset of the AADL process, and finally illustrates our advantages by contrasting with other literatures. This paper provides beneficial consultation for the development of AADL and its formal semantics and further improves the technology of architecture modeling and analysing for largescale complex software systems.

Key words: behavioral semantics;formal language;AADL;event;architecture

苗德成1,2,奚建清2,苏锦钿2. AADL进程子集行为语义研究[J]. J4, 2012, 34(7): 93-98.

MIAO Decheng1,2,XI Jianqing2,SU Jindian2. Research on Behavioral Semantics for the Subset of the AADL Process[J]. J4, 2012, 34(7): 93-98.

参考文献

［1］Feiler P H,Lewis B A,Vestal S.The SAE Architecture Analysis & Design Language(AADL)—A Standard for Engineering Performance Critical Systems［C］∥Proc of the IEEE Conf on Computer Aided Control Systems Design, 2006:12061211.
［2］SAE Aerospace. SAE AS5506A:Architecture Analysis and Sesign Language v2.0［EB/OL］.［20111117］.http://www.sae.org/technical/standards/AS5506A.
［3］Clavel M, Duran F, Eker S, et al. All about Maude—A HighPerformance Logical Framework［M］.Berlin:SpringerVerlag,How to Specify, Program and Verify Systems in Rewriting Logic,2007.
［4］杨志斌,皮磊,湖凯,等.复杂嵌入式实时系统体系结构设计与分析语言:AADL［J］.软件学报,2010,21(5):899915.
［5］董云卫,王广仁,张凡,等. AADL模型可靠性分析评估工具［J］.软件学报,2011,22(6):12521266.
［6］Olveczky P C, Boronat A, Meseguer J. Formal Semantics and Analysis of Behavioral AADL Models in RealTime Maude［R］. UrbanaChampaign,USA:Department of Computer Science, University of Illinois at UrbanaChampaign, 2010:138.
［7］Romero J R, Rivera J E, Duran F,et al. Formal and Tool Support for Model Driven Engineering with Maude［J］.Journal of Object Technology,2007,6(9):187207.
［8］Clavel M, Egea M. ITP/OCL: A RewritingBased Validation Tool for UML+OCL Static Class Diagrams［C］∥Proc of AMAST,2006:368373.
［9］Yang Z B, Hu K, Boderveix J P,et al.Two Formal Semantics of a Subset of the AADL［C］∥Proc of the 16th IEEE International Conf on Engineering of Complex Computer Systems, 2011:344349.
［10］Pi L, Yang Z B, Bodeveix J P,et al. A Comparative Study of FIACRE and TASM to Define AADL Real Time Concepts［C］∥Proc of the 14th IEEE International Conf on Engineering of Complex Computer Systems, 2009:347352.
［11］Berthomieu B, Bodeveix J P, Farail P,et al. Fiacre:An Intermediate Language for Model Verification in the TOPCASED Environment［C］∥Proc of the 4th European Congress on Embedded RealTime Software, 2008:18.
［12］Abdoul T, Champeau J, Dhaussy P,et al. AADL Execution Semantics Transformation for Formal Verification［C］∥Proc of the 13th IEEE International Conf.on Engineering of Complex Computer Systems, 2008:263268.
［13］Farail P, Gaufillet P, Canals A,et al.The TOPCASED Project:A Toolkit in Open Source for Critical Aeronautic Systems Design［C］∥Proc.of the 3rd European Congress Embedded RealTime Software, 2006:5559.
［14］任洪敏,钱乐秋. 构件组装及其形式化推导研究［J］.软件学报,2003,14(6):10661074.
［15］Xu R Z, Wu Q S, Gong H Q, et al. Research on Component Composition with Formal Semantics［C］∥Proc of the 3rd International Symposium on Intelligent Information Technology and Security Informatics, 2010:118124.
［16］Wang C W, Davies J, Welch J. A Guarded Workflow Language and Its Formal Semantics［C］∥Proc the of the 4th International Symposium on Theoretical Aspects of Software Engineering, 2010:2534.
［17］屈延文. 形式语义学基础与形式说明［M］. 北京:科学出版社, 2010.
［18］Rivera J E, Vallecillo A. Adding Behavioral Semantics to Models［C］∥Proc fo the 11th IEEE International Enterprise Distributed Object Computing Conference, 2007:169180.

[1]	胡庆孟, 王红斌, 王俊钟. 基于NPN融入词性注意力机制的中文事件探测[J]. 计算机工程与科学, 2023, 45(08): 1490-1497.
[2]	濮子俊, 张寿明. 基于特征融合与Transformer模型的声音事件定位与检测算法研究[J]. 计算机工程与科学, 2023, 45(06): 1097-1105.
[3]	白先平, 姚袭欣, 陈香兰, 刘翀, 李曦. 基于时间自动机的AADL端到端流规约验证方法[J]. 计算机工程与科学, 2023, 45(05): 810-819.
[4]	张立, 黎铁军, 张建民. 一种面向蒙特卡洛程序的128核可扩展体系结构[J]. 计算机工程与科学, 2023, 45(04): 590-598.
[5]	王玉琢, 刘海涛, 袁昊劼, 张志华. 一种基于构件的软件系统的薄弱构件确定方法[J]. 计算机工程与科学, 2023, 45(04): 630-637.
[6]	杜洁, 骆力明, 孙众. 基于ALBERT预训练模型的事件抽取技术研究[J]. 计算机工程与科学, 2023, 45(04): 711-717.
[7]	吕鹤轩, 黄山, 艾力卡木·再比布拉, 吴思衡, 段晓东, . Flink水位线动态调整策略[J]. 计算机工程与科学, 2023, 45(02): 237-245.
[8]	杨昊, 赵刚, 王兴芬. 基于混合模型的事件触发词抽取[J]. 计算机工程与科学, 2023, 45(01): 171-180.
[9]	杨慧慧, 方贤文, 邵叱风. 基于Petri网的并发事件流程模型修复分析[J]. 计算机工程与科学, 2021, 43(10): 1773-1780.
[10]	陈香兰, 李曦, 汪超, 周学海. 实时机模型及时间语义指令集研究[J]. 计算机工程与科学, 2021, 43(04): 571-578.
[11]	李仁刚, 任智新, 黄广奎, 孙颉, 王峰, 张闯, . 面向数据库查询加速的异构体系结构设计与实现[J]. 计算机工程与科学, 2020, 42(12): 2169-2178.
[12]	方旭东, 吴俊杰. 基于忆阻器的计算存储融合体系结构研究进展[J]. 计算机工程与科学, 2020, 42(11): 1929-1940.
[13]	韩哲, 姜晶菲, 乔林波, 窦勇, 许金伟, 阚志刚. 基于FPGA的事件抽取模型与加速器的设计实现[J]. 计算机工程与科学, 2020, 42(11): 1941-1948.
[14]	王耀华, 郭阳. 面向HPC的高性能微处理器研究进展[J]. 计算机工程与科学, 2020, 42(10高性能专刊): 1742-1748.
[15]	崔莹. 基于相似义原和依存句法的政外领域事件抽取方法[J]. 计算机工程与科学, 2020, 42(09): 1632-1639.