Description:
TECHNOLOGY AREA(S): Air Platform
OBJECTIVE: Develop unified behavior formalisms and tools for virtual integration of architectural models and tools from segmented behavior specifications of embedded computing systems using multiple formalisms.
DESCRIPTION: Cost overruns are a persistent problem with complex cyber-physical systems such as modern aircraft, automobiles, and medical devices. Aviation systems, in particular, demonstrate significant complexity given complex patterns of real-time interaction between mission system software components interacting across complex hardware architectures with safety and cybersecurity critical operation. The development of these systems must support nominal interaction behavior and be resilient to errors with the ability to safely switch to fault tolerant recovery modes. Due to their complexity, these systems are required to be modular, with different subcomponents developed by teams or subcontractors working largely with minimal interaction. In avionics systems, this modular approach is being enhanced by open architectures and standards such as Joint Communications Architecture (JCA), Open Mission Systems (OMS), Hardware Open System Technologies (HOST), Vehicular Integration for C4ISR/EW Interoperability (VICTORY), and Future Airborne Capabilities Environment (FACE). To a large degree the software based standards and frameworks like FACE and JCA encourage reuse and portability across systems to reduce cost; however, with the reuse of the software across various systems the resulting component interactions and behavior must be known and analyzed else failures that have been seen in complex safety critical systems may result (e.g., THERAC-25, Ariane 5 rocket, Mars Polar Lander failure, V-22 Osprey [1]). These standards provide a framework for common operating environment for software components and define the channels of interaction, but do not currently address the behavior of these components. To address these issues, software component developers use high level functional requirements and design specifications to guide their work. These specifications use multiple formalisms, such as state machines, first order logic, and fault propagations to express multiple views of behavior. Specifications often contain subtle errors and unstated assumptions regarding the overall behavior, error handling, and interaction of subcomponents that are challenging to detect because of the multiple formalisms used to express behavior. Because of the difficulty detecting behavioral error, hidden in the specification, these errors are only detected at integration time, contributing significantly to cost overruns. The Architecture-Centric Virtual Integration Process (ACVIP) using the Architecture Analysis and Design Language (AADL) [5] provides a model based system engineering methodology to detect errors early in the development process and reduce the costs associated with late stage rework. In ACVIP, hardware and software components are specified as AADL models with semantics that include interfaces, connections, and real-time performance details. These subcomponent models can then be virtually integrated into a common architectural model for formal analysis. This methodology has been useful at detecting errors including system scheduling, real-time performance, and safety [2,3] at design time and is now being evaluated and matured for Army Aviation and potentially for Future Vertical Lift (FVL) for the results it can produce in cost efficiencies and safer, more secure cyber physical systems. Despite these successes, virtual integration is still a developing technique, with significant gaps in analysis capabilities. One such analysis gap is in behavioral modeling and specification, which has proven challenging using AADL. As an architectural model, behavioral specifications are not part of the core AADL semantics, but are spread across the core and multiple non-overlapping AADL annexes, including the Error Modeling Annex (EMV2) [6] and the Behavior Annex (BA) [7]. Furthermore, the AADL core provides no mechanism for assertion of correctness. To include correctness assertions, additional third party AADL annexes have been written, including Assumed Guarantee Reasoning Environment (AGREE) [4, 8, 9, 10] and Behavior Language for Embedded Systems with (BLESS) [3, 11]. These third-party annexes have proven effective in formal verification of architectural models, but further complicate unified behavioral analysis by adding additional “silos” for behavior specification. Methods of expressing a unified view of behavior that supports correctness assertions would enable virtual integration techniques that incorporate behavioral reasoning with correctness checking. Supporting this unified behavioral specification, there is a need for tools and methodologies that can extract and specify the behavior of a system expressed in AADL containing multiple subcomponents, each with behavior specifications spread across multiple AADL annexes, including the BA and the EMV2 and synthesize assertions of correctness based on the overall architecture. Methodologies should specify system level behavior at a level of detail sufficient to detect requirement and design errors early in the development process. Envisioned approaches should unify the state machine semantics of the BA, the error states of EMV2, the mode changes of core AADL, and assume/guarantee methods of AGREE and BLESS into a single unified framework that can be analyzed in a computationally tractable manner. Proposer should create user friendly tools that could assist in the analysis within the avionics domain yet are sufficiently general to apply to non-avionics domains such as automotive and medical devices.
PHASE I: Provide a reference architecture and a software component specification, including mode changes, behavior specifications, and error models, define a unified model for the behavior of the composite system, demonstrate with a prototype tool that the unified model can be extracted from the Architecture Analysis and Design Language (AADL) specifications, and that the formal semantics are rich enough to discover design phase errors that would be undetected with existing methods. Proposers are expected to provide scenarios of interest including software component specifications and examples of errors that can only be detected using a unified behavior model. These scenarios are to be defined in AADL models with the modes, execution and error behavior. These models are to be provided to the government before the final delivery of the prototype tool(s). The models are to clearly represent the behavior that the analysis is intended to represent for the nominal and off nominal case(s). The government may provide models back to the prototype developer with errors that can demonstrate the prototype unified modeling tool can detect. The Phase I tool(s) will at minimum able to work with one component integrated in a reference architecture and interworking with the system architecture. The products of Phase I will include the prototype tool(s), the component model(s) clearly identifying the errored conditions, a report and briefing including a demonstration. At minimum a technical readiness level of 3 (TRL 3) should be the objective.
PHASE II: Extend the tool(s) developed on Phase I to create more formal verification artifacts. Demonstrate that techniques will scale to realistic problem sizes with the tool(s) having user feedback mechanisms to aid the users in understand the results of analysis. Tools should not require understanding of formal methods analyses for effective use (input and output) and should possess an intuitive graphical user interface (GUI) with online help. The tool(s) should support a system integration analysis of at least 3-6 modular software components, with behavior descriptions of each software component to be integrated in a system. For this scaled up demonstration the AADL models of the modes, error and execution behavior should again be provided to the government. The models should clearly identify nominal and off-nominal behavior. Again, the government may present back models to verify the ability of the capability of the unified behavior analysis tool detect and clearly demonstrate errant behavior can be detected. The products of Phase II will include the prototype tool(s), the component model(s) clearly identifying the errored conditions, a report and briefing including a demonstration.
PHASE III: Apply techniques and tools developed in Phases I and II to a realistic scale System Architectures chosen in conjunction with program technical point of contact. This could include an aviation mission computing system or subsystem architectures of interest. Extend tooling to support multiple open system architectures, and refine formal artifacts and feedback mechanisms based on feedback from users. Potential architectural framework of interest for aviation includes the Joint Common Architecture (JCA) and Future Airborne Capability Environment (FACE). A TRL of 7 is the objective.
REFERENCES:
1: Ogheneovo, Edward E., "Why Does Software Fail", published online April 2014 in SciRes. http://www.scirp.org/journal/jcc
2: A. Boydston, P. Feiler, S. Vestal, B. Lewis, "Joint Common Architecture (JCA) Demonstration Architecture Centric Virtual Integration Process (ACVIP) Shadow Effort", AHS 71st Annual Forum (2015).
3: B.R. Larson, Y. Zhang, S.C. Barrett, J. Hatcliff, P.L. Jones, "Enabling Safe Interoperation by Medical Device Virtual Integration", IEEE Design and Test 32(5):74-88, October 2015
4: M. Whalen, D. Cofer, A. Gacek. "Requirements and Architectures for Secure Vehicles", IEEE Software 33(4):22-25, June 201
5: AS-2 Embedded Computing Systems Committee SAE. Architecture Analysis & Design Language (AADL). SAE Standards no. AS5506C (2017)
6: AS-2 Embedded Computing Systems Committee SAE. Architecture Analysis & Design Language (AADL) Annex Document containing Error Model Annex. SAE Standards no. AS5506/1A (2015)
7: AS-2 Embedded Computing Systems Committee SAE. Architecture Analysis & Design Language (AADL) Behavior Annex. SAE Standards no. AS5506/2A (2017)
8: D. Cofer, J. Backes, "Compositional Analysis of Avionics Architectures in AADL", DARPA TTO META, 16 April 2012
9: J. Backes, A. Gacek, D. Cofer: Rockwell Collins, M. Whalen: University of Minnesota, "AGREE: Compositional Reasoning for AADL Models", S5 Symposium Briefing, 10 June 2014
10: K. Fisher, R. Richards, J. Launchbury, "The HACMS program: using formal methods to eliminate exploitable bugs", https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/, 2017 Oct 13
11: B. Larson, P. Chalin, J. Hatcliff, "BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software", Springer, NFM 2013: NASA Formal Methods pp 276-290
KEYWORDS: Behavior, Modeling, Analysis, Formal Methods, AADL, Error, Safety, Security
CONTACT(S):
Linda Taylor
(256) 876-2883
linda.k.taylor38.civ@mail.mil
