文章基本信息

标题：A Comprehensive Formalization of AADL with Behavior Annex
本地全文：下载
作者：Yu Tan ; Yongwang Zhao ; Dianfu Ma 等
期刊名称：Scientific Programming
印刷版ISSN：1058-9244
出版年度：2022
卷号：2022
DOI：10.1155/2022/2079880
语种：English
出版社：Hindawi Publishing Corporation
摘要：In safety-critical fields, architectural languages such as AADL (Architecture Analysis and Design Language) have been playing an important role, and the analysis of the languages and systems designed by them is a challenging research topic. At present, a formal method has become one of the main practices in software engineering for strict analysis, and it has been applied on the tools of formalization and analysis. The formal method can be used to find and resolve the problems early by describing the system with precise semantics and validating the system model. This article studies the comprehensive formal specification and verification of AADL with Behavior annex by the formal method. The presentation of this specification and semantics is the aim of this article, and the work is illustrated with an ARINC653 model case study in Isabelle/HOL.