Browsing by Author "Miller, Steven P."

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    FGS Partitioning Final Report
    (2005-12-14) Miller, Steven P.; O'Brien, Dan; Heimdahl, Mats; Joshi, Anjali
    Partitioning a system consists of dividing it into components that can be physically isolated from each other while preserving the essential behavior of the system. In this report, we describe a methodology for developing and reasoning about such systems. This approach allows a developer to start from an ideal system specification and refine it along two axes. Along one axis, the system can be refined one component at a time toward an implementation. Along the other axis, the behavior of the system can be relaxed to produce a more cost effective but still acceptable solution. We illustrate this process by applying it to the synchronization logic of a Dual Fight Guidance System, evolving the system from an ideal case in which the components do not fail and communicate synchronously to one in which the components can fail and communicate asynchronously. For each step, we show how the system requirements have to change if the system is be implemented and prove that each implementation meets the revised system requirements through model-checking.
  • Thumbnail Image
    Item
    Requirements-Based Testing in a Model-Based World
    (2005-05-09) Heimdahl, Mats; Miller, Steven P.
    Model-based software development offers new opportunities and challenges for validation and verification of safety-critical software. In this report, we describe an approach for validating the artifacts generated in a model-based development process. Our approach divides the traditional testing process into two parts: one that validates the formal model implements the high-level requirements and another that determines whether the code generated from the model is behaviorally equivalent. The focus in this report is on validation testing; in particular, we present a framework that enables objective measures of requirements coverage and provides the ability to achieve a high degree of automation.
  • Thumbnail Image
    Item
    Specification-based Prototyping for Embedded Systems
    (1999-03-02) Thompson, Jeffrey M.; Heimdahl, Mats; Miller, Steven P.
    Specifiction of software for safety critical, embedded computer systems has been widely addressed in literture. 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. This approach combines the advantages of rigourous formal specifications and rapid systems prototyping. We base our work on a modeling language using hierarchical state machines. 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 issued as a prototype of the proposed software. By using the formal specification as the prototype, 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 and interact with software models of its embedding environment or even the physical environment itself (hardware-in-the-loop simulatioan.