Experimenting an AADL Behavioural Annex and a Verification Method-猫眼课题宝

DOI：

发表时间：

2006-07

期刊：

影响因子：

通讯作者：

中科院分区：

其他

文献类型：

作者：

J. Bodeveix;M. Filali;Miloud Rached;D. Chemouil;Pierre Gaufillet

空中客车法国1。本文提出了体系结构分析和设计语言的一个扩展，该语言支持属性和抽象行为的表达，以便执行具有帐户数据依赖行为的定时验证ﬁ阳离子。为此，使用了AADL的附件扩展机制来附加行为、子程序和线程。在进行模型检验时，使用了实时proper-tiesoftheenvironmentareﬁrstspeciﬁedwithatimedlogic，，然后用Tableau方法综合了它的自动机。我们描述了这种验证ﬁ计算方法在Simpliﬁedﬁﬂight软件的验证中的应用。AADL及其执行模块2.1。AADL语言AADL是一种用于描述系统的软件和硬件组件以及这些组件之间的接口的语言。语言可以描述组件的功能接口，如数据输入和输出，以及非功能方面，如时序属性。该语言可以说明组件的组合，例如，如何连接数据输入和输出，或者如何将软件组件分配给硬件组件。关于这种语言的更多详细信息可以在www.aadl.info.上找到。虽然一些行为方面可以用AADL描述(例如，静态线性控制ﬂOWS)，但应用行为主要依赖于用目标语言(C、Ada等)编写的源代码。本文给出了一个依赖于性质的行为扩展和一个指定的附件。它使更好地分析行为成为可能。这些扩展试图尽可能多地重用现有的AADL概念，例如模式转换。我们的建议的主要特点涉及：·高级组成范例：我们研究了如何在AADL中引入HRT-Hood[1]复合范例。·与子程序和线程行为相关的动态方面。我们采用了类似于AADL模式转换的基于自动机的描述。·所提出的附件的语义与AADL.2.2的执行模型兼容。AADL执行模型AADL支持同步和异步执行模型。AADL的同步子集由周期性线程组成。它们在分派时接收数据，进行一些计算，并在完成或截止日期将数据传输到目标线程。数据可以在同一时间段内传输到目标线程，这称为立即传输，对应于抽象同步模型的零时间计算。该模型增加了异步特性：可能与数据相关的事件可以随时通过RAISE_EVENT系统调用发送，并可能导致目标线程的调度；通过AADL属性声明的时间方面用于验证AADLspeciﬁ阳离子与抽象同步模型之间的充分性，并可用于合成静态调度器。行为描述和行为描述本节介绍了拟议的行为附件的要素以及表达财产时使用的语言。__________________________________________________

AIRBUS France1. INTRODUCTIONThis paper presents an extension of the ArchitectureAnalysis and Design Language (AADL) supportingthe expression of properties and abstract behaviors inorder to perform timed veriﬁcations that take into ac-countdata dependantbehaviors. Forthispurpose, theannex extension mechanism of AADL has been usedtoattachbehaviorstosubprogramsandthreads. Inor-der to perform model checking, the real time proper-tiesoftheenvironmentareﬁrstspeciﬁedwithatimedlogic, then a tableau method for synthesizing its au-tomaton is used. We sketch the use of such a veriﬁca-tion methodology on the veriﬁcation of a simpliﬁedﬂight software.2. AADL AND ITS EXECUTION MODEL2.1. The AADL languageThe AADL is a language used to describe the soft-ware and hardware components of a system and theinterfaces between those components. The languagecan describe functional interfaces of components,such as data inputs and outputs, and non-functionalaspects, such as timing properties. The language candescribehowcomponentsarecombined,forinstance,how data inputs and outputs are connected or howsoftware components are allocated to hardware com-ponents. More detailed information about this lan-guage may be found at: www.aadl.info.Although some behavioural aspects can be describedin AADL (e.g. static linear control ﬂows), applica-tion behaviours rely mainly on source code written ina target language (C, Ada, ...). This paper presents abehaviour extension relying on properties and a ded-icated annex. It makes possible a better analysis ofbehaviours. These extensions try to reuse as much aspossible existing AADL concepts, e.g., mode transi-tions. The main features of our proposal concern:• High level composition paradigms: we havestudied how to introduce HRT-HOOD [1] com-position paradigms within AADL.• Dynamic aspects related to subprogram andthread behaviors. We have adopted an automa-ton based description similar to AADL modetransitions.• The semantics of the proposed annex is compat-ible with the execution model of AADL.2.2. The AADL execution modelAADL supports synchronous as well as asyn-chronous execution models. The synchronous sub-set of AADL consists of periodic threads. They re-ceive data at dispatch time, make some computa-tion and transmit data to destination threads at com-pletion or at deadline. Data may be transfered todestination threads within the same period, whichis called immediate transmission and corresponds tozero time computation of the abstract synchronousmodel. To this model are added asynchronous fea-tures: events which may be associated with data canbe send through the Raise_Event system call atany time and may result in the dispatch of destinationthreads.Timing aspects declared through AADL propertiesare used to verify the adequation between AADLspeciﬁcations and the abstract synchronous modeland can be used to synthesize a static scheduler.3. BEHAVIOURAL DESCRIPTIONS ANDPROPERTIESThis section introduces elements of the proposed be-havioural annex and the language used to expressproperties. __________________________________________________

Experimenting an AADL Behavioural Annex and a Verification Method

文献摘要

被引文献

相似文献