This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Checking Compliance of AADL Models with Modeling Guidelines using Resolint
Technical Paper
2023-01-0995
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Event:
2023 AeroTech
Language:
English
Abstract
Certification standards for high-assurance systems include objectives for
demonstrating compliance of process artifacts such as requirements and code with
style guidelines and other standards. With the emergence of model-based
development, similar objectives have been specified that apply to models.
Demonstration of compliance is often achieved by employing a static analysis
linter tool. This paper describes Resolint, an open-source,
lightweight linter tool for checking compliance of Architecture Analysis and
Design Language (AADL) models with modeling guidelines. AADL enables engineers
to describe the key elements of distributed, real-time, embedded system
architectures with a sufficiently rigorous semantics. In addition, AADL provides
an annex mechanism for extending the base language, enabling new kinds of
analyses and tool support. Resolint uses the AADL annex capability to provide a
language for specifying style guide rule sets. It is implemented as a plugin for
the Eclipse-based Open Source AADL Tool Environment (OSATE) and includes an
engine for evaluating whether an AADL model complies with the specified rule
sets. Results of the Resolint analysis are displayed to the user and can even be
automatically incorporated as evidence in a system assurance case using the
companion Resolute tool. To illustrate the features of Resolint, we present
three use cases involving the assurance of embedded avionics applications. We
further describe how we applied Resolint in the evaluation, synthesis, and
assurance of a cyber-resilient UAV surveillance application developed on the
DARPA Cyber Assured Systems Engineering (CASE) program.
DISTRIBUTION STATEMENT A. Approved for public release: distribution
unlimited.
Authors
Topic
Citation
Amundson, I., "Checking Compliance of AADL Models with Modeling Guidelines using Resolint," SAE Technical Paper 2023-01-0995, 2023, https://doi.org/10.4271/2023-01-0995.Also In
References
- RTCA DO-178C 2011
- RTCA DO-331 2011
- MISRA Consortium 2012
- The MathWorks Advisory Board 2022 https://www.mathworks.com/solutions/mab-guidelines.html
- IEEE 2008
- Feiler , P.H. and Gluch , D.P. Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language 1st Addison-Wesley Professional 2012
- SAE AS5506D 2022
- Gacek , A. , Backes , J. , Cofer , D. , Slind , K. et al. Resolute: An Assurance Case Language for Architecture Models Feldman , M. and Tucker Taft , S. Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT 2014 Portland, Oregon, USA 2014 19 28
- Johnson , S.C. Lint, a C Program Checker Murray Hill Bell Telephone Laboratories 1977
- Wikipedia 2022 https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis
- Vector Informatik 2022 https://pclintplus.com/pc-lint-plus/
- The MathWorks 2022 https://www.mathworks.com/products/simulink-check.html
- MES 2022 https://model-engineers.com/en/quality-tools/mxam/
- Dassault Systemes 2022 https://www.3ds.com/products-services/catia/products/no-magic/cameo-systems-modeler/
- Ansys 2022 https://www.ansys.com/products/embedded-software/ansys-scade-suite
- Ellidiss Technologies https://www.ellidiss.com/products/aadl-inspector/
- Cofer , D. , Amundson , I. , Babar , J. , Hardin , D. et al. Cyber Assured Systems Engineering at Scale IEEE Security and Privacy 2022
- Mercer , E. , Slind , K. , Amundson , I. , Cofer , D. , et al. Synthesizing Verified Components for Cyber Assured Systems Engineering 24th International Conference on Model-Driven Engineering Languages and Systems (MODELS 2021) 2021
- Cofer , D. , Gacek , A. , Miller , S. , Whalen , M. , et al. Compositional Verification of Architectural Models Goodloe , A.E. and Person , S. NASA Formal Methods Berlin, Heidelberg Springer Berlin Heidelberg 2012 126 140
- Hatcliff , J. , Belt , J. , and Carpenter , T. HAMR: An AADL Multi-platform Code Generation Toolset 10th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), ser. LNCS 13036 2021 274 295
- Klein , G. , Elphinstone , K. , Heiser , G. , Andronick , J. , et al. seL4: Formal Verification of an OS Kernel Matthews , J.N. and Anderson , T.E. Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009 (SOSP 2009) Big Sky, Montana, USA 2009 207 220
- The Assurance Case Working Group SCSC-141B 2011
- RTCA DO-330 2011