English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

AADL along with its Behavior Annex is an architecture and behavior description language for safety-critical domains, e.g. avionics, aerospace, and defence. In order to formally analyze behavior properties of AADL models, it is necessary to transform the AADL language into formal languages supported by formal verification tools. Moreover, comprehensive formal verification of AADL models highly requires that the transformation supports larger subset of the AADL language, as well as verification tools are able to capture various behavior of AADL, such as concurrency and timing. As an extended communicating sequential process (CSP), stateful timed CSP with its model checker-PAT provide an strongly expressive language and verification tool for real-time systems, distributed systems, and concurrent systems. This paper introduces a model transformation approach from a comparatively complete subset of AADL to stateful timed CSP, in particular supporting major components of AADL Behavior Annex. We propose a comprehensive set of transformation rules for AADL to stateful timed CSP. Then, we perform formal verification in PAT to analyze concurrent behavior properties of AADL models, such as safety, liveness, and trace refinement with various fairness assumptions, in which we consider time capacities, deadlines, periods of AADL threads and durations of AADL processes. As a study case, we develop an AADL model of F-16 &#x201C;Auto Pilot Controller&#x201D;and transform the model into Stateful Timed CSP. We specify a set of critical properties of the model and perform formal verification in PAT.

Formal Verification of Behavioral AADL Models by Stateful Timed CSP