کد مقاله کد نشریه سال انتشار مقاله انگلیسی ترجمه فارسی نسخه تمام متن
461062 696540 2014 27 صفحه PDF سفارش دهید دانلود رایگان
عنوان انگلیسی مقاله ISI
From AADL to Timed Abstract State Machines: A verified model transformation
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
سفارش ترجمه تخصصی
با تضمین قیمت و کیفیت
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر شبکه های کامپیوتری و ارتباطات
پیش نمایش صفحه اول مقاله
From AADL to Timed Abstract State Machines: A verified model transformation
چکیده انگلیسی


• We propose a verified transformation from a subset of AADL to TASM.
• We give a reference semantics of the subset of AADL which is formalized in TTS.
• We give a formal translational semantics of the subset of AADL by translating it to TASM.
• We present a mechanized proof of the semantics preservation of the transformation from the subset of AADL to TASM.

Architecture Analysis and Design Language (AADL) is an architecture description language standard for embedded real-time systems widely used in the avionics and aerospace industry to model safety-critical applications. To verify and analyze the AADL models, model transformation technologies are often used to automatically extract a formal specification suitable for analysis and verification. In this process, it remains a challenge to prove that the model transformation preserves the semantics of the initial AADL model or, at least, some of the specific properties or requirements it needs to satisfy. This paper presents a machine checked semantics-preserving transformation of a subset of AADL (including periodic threads, data port communications, mode changes, and the AADL behavior annex) into Timed Abstract State Machines (TASM). The AADL standard itself lacks at present a formal semantics to make this translation validation possible. Our contribution is to bridge this gap by providing two formal semantics for the subset of AADL. The execution semantics provided by the AADL standard is formalized as Timed Transition Systems (TTS). This formalization gives a reference expression of AADL semantics which can be compared with the TASM-based translation (for verification purpose). Finally, the verified transformation is mechanized in the theorem prover Coq.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Systems and Software - Volume 93, July 2014, Pages 42–68
نویسندگان
, , , , , ,
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
سفارش ترجمه تخصصی
با تضمین قیمت و کیفیت