Browsing by Author "Cofer, Darren"

Now showing 1 - 13 of 13
  • Thumbnail Image
    Item
    Architecture Modeling and Analysis for Safety Engineering
    (Springer, 2017) Stewart, Danielle; Whalen, Michael; Cofer, Darren; Heimdahl, Mats
    Architecture description languages such as AADL allow systems engineers to specify the structure of system architectures and perform several analyses over them, including schedulability, resource analysis, and information flow. In addition, they permit system-level requirements to be specified and analyzed early in the development process of airborne and ground-based systems. These tools can also be used to perform safety analysis based on the system architecture and initial functional decomposition. Using AADL-based system architecture modeling and analysis tools as an exemplar, we extend existing analysis methods to support system safety objectives of ARP4754A and ARP4761. This includes extensions to existing modeling languages to better describe failure conditions, interactions, and mitigations, and improvements to compositional reasoning approaches focused on the specific needs of system safety analysis. We develop example systems based on the Wheel Braking System in SAE AIR6110 to evaluate the effectiveness and practicality of our approach.
  • Thumbnail Image
    Item
    Circular Hierarchical Reasoning using Past Time LTL
    (University of Minnesota, 2011) Cofer, Darren; Gacek, Andrew; Whalen, Michael
    We describe a composition rule for hierarchically composed components that may involve circular reasoning between the components. It is similar to previous work by McMillan, specialized to component level reasoning. In contrast to McMillan's work, our composition rule can be used in provers that only support safety properties (e.g. k-induction model checkers) as long as the system and component contracts consist of state invariants. The composition rule still holds for richer contracts, but the resulting verification conditions then require a general purpose model checker.
  • Thumbnail Image
    Item
    Compositional Verification of Architectural Models
    (Springer-Verlag, 2012) Cofer, Darren; Gacek, Andrew; Miller, Steven; Whalen, Michael
    This paper describes a design flow and supporting tools to significantly improve the design and verification of complex cyber-physical systems. We focus on system architecture models composed from libraries of components and complexity-reducing design patterns having formally verified properties. This allows new system designs to be developed rapidly using patterns that have been shown to reduce unnecessary complexity and coupling between components. Components and patterns are annotated with formal contracts describing their guaranteed behaviors and the contextual assumptions that must be satisfied for their correct operation. We describe the compositional reasoning framework that we have developed for proving the correctness of a system design, and provide a proof of the soundness of our compositional reasoning approach. An example based on an aircraft flight control system is provided to illustrate the method and supporting analysis tools.
  • Thumbnail Image
    Item
    Hierarchical Circular Compositional Reasoning
    (University of Minnesota, 2014) Gacek, Andrew; Katis, Andreas; Whalen, Michael; Cofer, Darren
    We describe a composition rule for hierarchically composed components that may involve circular reasoning between the components. It is similar to previous work by McMillan, specialized to component level reasoning. In contrast to McMillan's work, our composition rule can be used in provers that only support safety properties (e.g. k-induction model checkers) as long as the system and component contracts consist of state invariants. The composition rule still holds for richer contracts, but the resulting verification conditions then require a general purpose model checker.
  • Thumbnail Image
    Item
    Hierarchical Circular Compositional Reasoning
    (2014-03-31) Gacek, Andrew; Katis, Andreas; Cofer, Darren
    We describe a composition rule for hierarchically composed components that may involve circular reasoning between the components. It is similar to previous work by McMillan, specialized to component level reasoning. In contrast to McMillan's work, our composition rule can be used in provers that only support safety properties (e.g. k-induction model checkers) as long as the system and component contracts consist of state invariants. The composition rule still holds for richer contracts, but the resulting verification conditions then require a general purpose model checker.
  • Thumbnail Image
    Item
    Integration of Formal Analysis into a Model-Based Software Development Process
    (Springer-Verlag, 2007) Whalen, Michael; Cofer, Darren; Miller, Steven; Krogh, Bruce; Storm, Walter
    The next generation of military aerospace systems will include advanced control systems whose size and complexity will challenge current verification and validation approaches. The recent adoption by the aerospace industry of model-based development tools such as Simulink® and SCADE Suite™ is removing barriers to the use of formal methods for the verification of critical avionics software. Formal methods use mathematics to prove that software design models meet their requirements, and so can greatly increase confidence in the safety and correctness of software. Recent advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This paper describes how formal analysis tools can be inserted into a model-based development process to decrease costs and increase quality of critical avionics software
  • Thumbnail Image
    Item
    Requirements Analysis of a Quad-Redundant Flight Control System
    (Springer, 2015) Backes, John; Cofer, Darren; Gacek, Andrew; Whalen, Michael
    In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA’s Transport Class Model (TCM). We use a compositional approach with assume-guarantee contracts that correspond to the requirements for software components embedded in an AADL system architecture model. This approach is designed to exploit the verification effort and artifacts that are already part of typical software verification processes in the avionics domain. Our approach is supported by an AADL annex that allows specification of contracts along with a tool, called AGREE, for performing compositional verification. The goal of this paper is to show the benefits of a compositional verification approach applied to a realistic avionics system and to demonstrate the effectiveness of the AGREE tool in performing this analysis.
  • Thumbnail Image
    Item
    Requirements and Architectures for Secure Vehicles
    (IEEE, 2016) Whalen, Michael; Cofer, Darren; Gacek, Andrew
    In the High-Assurance Cyber Military Systems project, researchers are investigating how to construct complex networked-vehicle software securely. Experiments demonstrated that careful attention to requirements and system architecture, along with formally verified approaches that remove known security weaknesses, can lead to vehicles that can withstand attacks from even sophisticated attackers with access to vehicle design data.
  • Thumbnail Image
    Item
    Resolute: An Assurance Case Language for Architecture Models
    (ACM, 2016) Gacek, Andrew; Backes, John; Cofer, Darren; Slind, Konrad; Whalen, Michael
    Arguments about the safety, security, and correctness of a complex system are often made in the form of an assurance case. An assurance case is a structured argument, often represented with a graphical interface, that presents and supports claims about a system's behavior. The argument may combine different kinds of evidence to justify its top level claim. While assurance cases deliver some level of guarantee of a system's correctness, they lack the rigor that proofs from formal methods typically provide. Furthermore, changes in the structure of a model during development may result in inconsistencies between a design and its assurance case. Our solution is a framework for automatically generating assurance cases based on 1) a system model specified in an architectural design language, 2) a set of logical rules expressed in a domain specific language that we have developed, and 3) the results of other formal analyses that have been run on the model. We argue that the rigor of these automatically generated assurance cases exceeds those of traditional assurance case arguments because of their more formal logical foundation and direct connection to the architectural model.
  • Thumbnail Image
    Item
    Safety Annex for the Architecture Analysis and Design Language
    (2018-03-09) Stewart, Danielle; Liu, Jing (Janet); Heimdahl, Mats; Cofer, Darren; Peterson, Michael
    Model-based development techniques are increasingly being used in the development of critical systems software. Leveraging the artifacts from model based development in the safety analysis process would be highly desirable to provide accurate analysis and enable cost savings. In particular, architectural and behavioral models provide rich information about the system's operation. In this paper we describe an extension to the Architecture Analysis and Design Language (AADL) developed to allow a rich modeling of a system under failure conditions. This emph{Safety Annex} allows the independent modeling of component failure modes and allows safety engineers to weave various types of faults into the nominal system model. The accompanying tool support allows investigation of the propagation of errors from their source to their effect on top level safety properties without the need to add separate propagation specifications; it also supports describing dependent faults that are not captured through the behavioral models, e.g., failures correlated due to the physical structure of the system. We describe the Safety Annex, illustrate its use with a representative example, and discuss and demonstrate the tool support enabling an analyst to investigate the system behavior under failure conditions.
  • Thumbnail Image
    Item
    Software Model Checking Takes Off
    (ACM, 2010) Miller, Steven; Whalen, Michael; Cofer, Darren
    The increasing popularity of model-based development and the growing power of model checkers are making it practical to use formal verification for important classes of software designs. A barrier to doing this in an industrial setting has been the need to translate the commercial modeling languages developers use into the input languages of the verification tools. This paper describes a translator framework that enables the use of model checking and theorem proving on complex avionics systems and describes its use in three industrial case studies.
  • Thumbnail Image
    Item
    Towards Realizability Checking of Contracts using Theories
    (2015) Gacek, Andrew; Katis, Andreas; Whalen, Michael; Backes, John; Cofer, Darren
    Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction. Such proofs build from “leaf-level� assume/guarantee component contracts through architectural layers towards top-level safety properties.The proofs are built upon the premise that each leaf-level component contract is realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. Without engineering support it is all too easy to write leaf-level components that can’t be realized. Realizability checking for propositional contracts has been well-studied for many years, both for component synthesis and checking correctness of temporal logic requirements. However, checking realizability for contracts involving infinite theories is still an open problem. In this paper, we describe a new approach for checking realizability of contracts involving theories and demonstrate its usefulness on several examples.
  • Thumbnail Image
    Item
    Your "What" is My "How": Iteration and Hierarchy in System Design
    (IEEE Computer Society, 2013) Whalen, Michael; Gacek, Andrew; Cofer, Darren; Murugesan, Anitha; Heimdahl, Mats; Rayadurgam, Sanjai
    Systems are naturally constructed in hierarchies, in which design choices made at higher levels of abstraction levy requirements on system components at the lower levels. Thus, whether an aspect of a system is a design choice or a requirement largely depends on your vantage point within the system components' hierarchy. Systems are also often constructed from the middle-out rather than top-down; compatibility with existing systems and architectures and availability of specific components influence high-level requirements. Requirements and architectural design should be more closely aligned: requirements models must account for hierarchical system construction and architectural design notations must better support requirements specification for system components.