Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Author "Miller, Steven"

Now showing 1 - 7 of 7
  • Thumbnail Image
    Item
    A Proposal for Model-Based Safety Analysis
    (2005) Joshi, Anjali; Miller, Steven; Whalen, Michael; Heimdahl, Mats
    System safety analysis techniques are well es-tablished and are used extensively during the design of safety-critical systems. Despite this, most of the techniques are highly subjective and dependent on the skill of the practitioner. Since these analyses are usually based on an informal system model, it is unlikely that they will be complete, consistent, and error free. In fact, the lack of precise models of the system architecture and its failure modes often forces the safety analysts to devote much of their effort to finding undocumented details of the sys-tem behavior and embedding this information in the safety artifacts such as the fault trees. In this paper we propose an approach, Model-Based Safety Analysis, in which the system and safety engineers use the same system models cre-ated during a model-based development process. By extending the system model with a fault model as well as relevant portions of the physical system to be controlled, automated support can be provided for much of the safety analysis. We believe that by using a common model for both system and safety engineering and automating parts of the safety analysis, we can both reduce the cost and improve the quality of the safety analysis. Here we present our vision of model-based safety analysis and dis-cuss the advantages and challenges in making this approach practical.
  • 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
    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
    Mode Confusion Analysis of a Flight Guidance System Using Formal Methods
    (2003) Joshi, Anjali; Miller, Steven; Heimdahl, Mats
    Advancements in digital avionics systems have accounted for much of the improvement in air safety seen over the last few decades. At the same time, the growing complexity of these systems places greater demands on the flight crew and increases the risk of mode confusion, a phenomenon in which pilots become confused about the status of the system and interact with it incorrectly. To fly commercial flights today, pilots must master several complex, dynamically interacting systems, often operating at different levels of automation. These systems typically have many different modes of operation, with different responses to crew actions and the other systems in each mode. Mode confusion occurs when the flight crew believes they are in a mode different than the one they are actually in and consequently make inappropriate requests or responses to the automation. The basis premise behind detecting mode confusion through analysis of system requirements or design specifications is that certain design features or patterns are more likely to cause mode confusion than others. This paper describes the use of automated analysis tools, such as model-checkers and theorem provers, to search for potential sources of mode confusion in a representative specification of the mode logic of a Flight Guidance System. We describe several representative patterns indicative of mode confusion, and show how automated tools can be used to systematically search for such patterns in a requirements or design model.
  • Thumbnail Image
    Item
    Proving the shalls: Early validation of requirements through formal methods
    (2006) Miller, Steven; Tribble, Alan; Whalen, Michael; Heimdahl, Mats
    Incomplete, inaccurate, ambiguous, and volatile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods offers developers of safety-critical systems a powerful new approach for the early validation of requirements. This paper describes a case study conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable cost. Several hundred functional and safety requirements for the mode logic of a typical Flight Guidance System were captured as natural language "shall" statements. A formal model of the mode logic was written in the RSML-e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each "shall" statement was manually translated into a NuSMV or PVS property and proven using these tools. Numerous errors were found in both the original requirements and the RSML-e model. This demonstrates that formal models can be written for realistic systems and that formal analysis tools have matured to the point where they can be effectively used to find errors before implementation.
  • 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
    Specification-Based Prototyping for Embedded Systems
    (1999) Thompson, Jeffrey; Heimdahl, Mats; Miller, Steven
    Specification of software for safety critical, embedded computer systems has been widely addressed in literature. To achieve the high level of confidence in a specification's correctness necessary in many applications, manual inspections, formal verification, and simulation must be used in concert. Researchers have successfully addressed issues in inspection and verification; however, results in the areas of execution and simulation of specifications have not made as large an impact as desired. In this paper we present an approach to specification-based prototyping which addresses this issue. It combines the advantages of rigorous formal specifications and rapid systems prototyping. The approach lets us refine a formal executable model of the system requirements to a detailed model of the software requirements. Throughout this refinement process, the specification is used as a prototype of the proposed software. Thus, we guarantee that the formal specification of the system is always consistent with the observed behavior of the prototype. The approach is supported with the Nimbus environment, a framework that allows the formal specification to execute while interacting with software models of its embedding environment or even the physical environment itself (hardware-in-the-loop simulation).