Cyber-physical systems, such as avionics, must be tolerant to cyber-attacks in the same way they are tolerant to random faults: they either gracefully recover or safely shut down as requirements dictate. The DARPA Cyber Assured Systems Engineering program is developing tools for design, analysis, and verification that enable systems engineers to design-in cyber-resiliency in a Model-Based Systems Engineering environment. This paper describes automated model transformations that introduce high-assurance cyber-resiliency components into a system, in particular filters and monitors that prevent malicious input and detect supply chain attacks, respectively. A formal specification defines each high-assurance component, and is used to verify that the component addresses system level cyber requirements. Implementations for these high-assurance components are directly synthesized from their specifications, and are automatically proven to preserve the exact meaning of the specifications all the way down to the binary code level. The model transformations are integrated into the Open Source AADL Tool Environment (OSATE). The paper further reports on a case study applying security-enhancing model transformations to a UAV system that uses the Air Force Research Laboratory's OpenUxAS services for route planning. In the case study, the model transformations add filters to guard against malformed input, as well as monitors to guard against ground station spoofing and malicious flight plans from OpenUxAS.

Pattern solutions for software and architectures have significantly reduced design, verification, and validation times by mapping challenging problems into a solved generic problem. In the paper, we present an architecture pattern for ensuring synchronous computation semantics using the PALS protocol. We develop a modeling framework in AADL to automatically transform a synchronous design of a real-time distributed system into an asynchronous design satisfying the PALS protocol. We present a detailed example of how the PALS transformation works for a dual-redundant system. From the example, we also describe the general transformation in terms of intuitively defined AADL semantics. Furthermore, we develop a static analysis checker to find necessary conditions that must be satisfied in order for the PALS transformation to work correctly. The transformations and static checks that we have described are implemented in OSATE using the generated EMF metamodel API for model manipulation.

The hardware and software in modern aircraft control systems are good candidates for verification using formal methods: they are complex, safety-critical, and challenge the capabilities of test-based verification strategies. We have previously reported on our use of model checking to verify the time partitioning property of the Deos/spl trade/ real-time operating system for embedded avionics. The size and complexity of this system have limited us to analyzing only one configuration at a time. To overcome this limit and generalize our analysis to arbitrary configurations we have turned to theorem proving. This paper describes our use of the PVS theorem prover to analyze the Deos scheduler. In addition to our inductive proof of the time partitioning invariant, we present a feature-based technique for modeling state-transition systems and formulating inductive invariants. This technique facilitates an incremental approach to theorem proving that scales well to models of increasing complexity, and has the potential to be applicable to a wide range of problems.

Technology transfer is an especially difficult proposition for real-time control. To facilitate it, we need to complement the “high-performance” orientation of control research with an emphasis on establishing “high confidence” in real-time implementation. Two particular problems are discussed and recent research directed at their solutions is presented. First, the use of anytime algorithms requires dynamic resource management technology that generally is not available today in real-time systems. Second, complex algorithms have unpredictable computational characteristics that, nevertheless, need to be modeled; statistical verification is suggested as a possible approach. In both cases, a synthesis of control engineering and computer science is required if effective solutions are to be devised. Simulation-based demonstrations with uninhabited aerial vehicles (UAVs) serve to illustrate the research efforts. © 2004 Wiley Periodicals, Inc.

This paper describes our work modeling key portions of the safety-critical software infrastructure in an integrated modular avionics (IMA) platform in an effort to analytically establish correctness of important aspects of its design. In particular, we use model checking to verify timing properties of the Deos/spl trade/ real-time operating system in the presence of various advanced scheduling features. We focus here on the addition of scheduler overhead processing time to the Deos model and analyzing its effect on the time partitioning property and the internal assertions (function preconditions) in the model. Our model includes advanced scheduling features (dynamic threads, slack recovery, aperiodic interrupts) and explicitly models the scheduler operations at the same level of detail as the source code. Our findings support the use of formal methods to verify key properties of safety-critical systems that would be difficult or impossible to establish otherwise.