Browsing by Author "Whalen, Michael"

Now showing 1 - 20 of 68
  • Thumbnail Image
    Item
    A DSL for cross-domain security
    (High Integrity Language Technology ACM SIGAda’s Annual International Conference (HILT 2012), 2012) Hardin, David; Slind, Konrad; Whalen, Michael; Pham, Hung T.
  • Thumbnail Image
    Item
    A flexible and non-intrusive approach for computing complex structural coverage metrics
    (ACM, 2015) Whalen, Michael; Person, Suzette; Rungta, Neha; Staats, Matt; Grijincu, Daniella
    Software analysis tools and techniques often leverage structural code coverage information to reason about the dynamic behavior of software. Existing techniques instrument the code with the required structural obligations and then monitor the execution of the compiled code to report coverage. Instrumentation based approaches often incur considerable runtime overhead for complex structural coverage metrics such as Modified Condition/Decision (mcdc). Code instrumentation, in general, has to be approached with great care to ensure it does not modify the behavior of the original code. Furthermore, instrumented code cannot be used in conjunction with other analyses that reason about the structure and semantics of the code under test. In this work, we introduce a non-intrusive preprocessing approach for computing structural coverage information. It uses a static partial evaluation of the decisions in the source code and a source-to-bytecode mapping to generate the information necessary to efficiently track structural coverage metrics during execution. Our technique is flexible; the results of the preprocessing can be used by a variety of coverage-driven software analysis tasks, including automated analyses that are not possible for instrumented code. Experimental results in the context of symbolic execution show the efficiency and flexibility of our non-intrusive approach for computing code coverage information.
  • Thumbnail Image
    Item
    A Parametric Structural Operational Semantics for Stateflow, UML Statecharts, and Rhapsody
    (UMSEC Technical Report 2010-1, 2010) Whalen, Michael
    In this report, we define a parametric structural operational semantics that can be used to define the behavior of three Statecharts variants: Stateflow from the Mathworks, Inc., UML Statecharts from the Object Management Group, and Rhapsody from Rational/IBM Corporation. These dialects are the most commonly used variants of Statecharts in industrial applications, and are increasingly used to construct safety-critical applications. We believe that our semantics for each dialect is more complete than prior research and matches the informal documentation of each notation more closely than other approaches. In the formalization process, we have discovered deep similarities between the semantics, and we are able to create a parametric operational semantics that factors out the variabilities between the dialects in a modular way.
  • 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
    Abstractions in Decision Procedures for Algebraic Data Types
    (University of Minnesota, 2013) Pham, Hung T.; Whalen, Michael
    Reasoning about algebraic data types and functions that operate over these data types is an important problem for a large variety of applications. In this paper, we present an unrolling-based decision procedure for reasoning about data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types into values in a decidable domain. We show that the procedure is sound and complete for a class of monotonic catamorphisms. Our work extends previous work in catamorphism-based reasoning in a number of directions. First, we propose the categories of monotonic catamorphisms and associative-commutative catamorphisms, which we argue provide a better formal foundation than previous categorizations of catamorphisms. We use monotonic catamorphisms to fix an incompleteness in a previous unrolling algorithm (and associated proof). We then use these notions to address two open questions from previous work: (1) we provide a bound on the number of unrollings necessary for completeness, showing that it is exponentially small with respect to formula size for associative-commutative catamorphisms, and (2) demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness.
  • Thumbnail Image
    Item
    An Approach to Automatic Code Generation for Safety-Critical Systems
    (1999) Whalen, Michael; Heimdahl, Mats
    Although formal requirements specifications can provide rigorous and unambiguous description of a safety-critical software system, designing and developing production quality code from high-level specifications can be a time-consuming and error-prone process. Automated translation, or code generation, of the specification to production code can alleviate many of the problems associated with design and implementation. In this report we outline the requirements of such code generation to obtain a high level of confidence in the correctness of the translation process. We then describe a translator for a state-based modeling language called RSML that largely meets these requirements. The process is based on the denotational semantics of both RSML and a simplified imperative target language (SIMPL), which are used to prove that the translator correctly implements the RSML semantics in SIMPL. The SIMPL code can then trivially be translated to any popular imperative language. The translation process also provides for informal arguments of the correctness of the code and traceability information.
  • Thumbnail Image
    Item
    An Improved Unrolling-Based Decision Procedure for Algebraic Data Types
    (Springer, 2013) Pham, Hung T.; Whalen, Michael
    Reasoning about algebraic data types and functions that operate over these data types is an important problem for a large variety of applications. In this paper, we present a decision procedure for reasoning about data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types into values in a decidable domain. We show that the procedure is sound and complete for a class of monotonic catamorphisms. Our work extends a previous decision procedure that solves formulas involving algebraic data types via successive unrollings of catamorphism functions. First, we propose the categories of monotonic catamorphisms and associative-commutative catamorphisms, which we argue provide a better formal foundation than previous categorizations of catamorphisms. We use monotonic catamorphisms to fix an incompleteness in the previous unrolling algorithm (and associated proof). We then use these notions to address two open problems from previous work: (1) we provide a bound on the number of unrollings necessary for completeness, showing that it is exponentially small with respect to formula size for associative-commutative catamorphisms, and (2) we demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness.
  • 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
    Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites
    (Springer, 2015) Murugesan, Anitha; Whalen, Michael; Rungta, Neha; Tkachuk, Oksana; Person, Suzette; Heimdahl, Mats; You, Dongjiang
    Structural coverage metrics have traditionally categorized code as either covered or uncovered. Recent work presents a stronger notion of coverage, checked coverage, which counts only statements whose execution contributes to an outcome checked by an oracle. While this notion of coverage addresses the adequacy of the oracle, for Model-Based Development of safety critical systems, it is still not enough; we are also interested in how much of the oracle is covered, and whether the values of program variables are masked when the oracle is evaluated. Such information can help system engineers identify missing requirements as well as missing test cases. In this work, we combine results from checked coverage with results from requirements coverage to help provide insight to engineers as to whether the requirements or the test suite need to be improved. We implement a dynamic backward slicing technique and evaluate it on several systems developed in Simulink. The results of our preliminary study show that even for systems with comprehensive test suites and good sets of requirements, our approach can identify cases where more tests or more requirements are needed to improve coverage numbers.
  • Thumbnail Image
    Item
    AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification
    (Springer-Verlag, 2002) Whalen, Michael; Fischer, Bernd; Schumann, Johann
    Code certication is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be dened and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satises these quality properties. The proofs serve as certicates which can be checked independently, by the code consumer or by certication authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code. Code certication can be viewed as a more practical version of traditional Hoare-style program verication. The properties to be veried are fairly simple and regular so that it is often possible to use an automated theorem prover to automatically discharge all emerging proof obligations. Usually, however, the programmer must still splice auxiliary annotations (e.g., loop invariants) into the program to facilitate the proofs. For complex properties or larger programs this quickly becomes the limiting factor for the applicability of current certication approaches. Our work combines code certication with automatic program synthesis which makes it possible to automatically generate both the code and all necessary annotations for fully automatic certication. By generating detailed annotations, one of the biggest obstacles for code certication is removed and it becomes possible to automatically check that synthesized programs obey the desired safety properties.
  • Thumbnail Image
    Item
    Automated Oracle Data Selection Support
    (2015-11) Gay, Gregory; Staats, Matt; Whalen, Michael; Heimdahl, Mats
    The choice of test oracle—the artifact that determines whether an application under test executes correctly—can significantly impact the effectiveness of the testing process. However, despite the prevalence of tools that support test input selection, little work exists for supporting oracle creation. We propose a method of supporting test oracle creation that automatically selects the oracle data—the set of variables monitored during testing—for expected value test oracles. This approach is based on the use of mutation analysis to rank variables in terms of fault-finding effectiveness, thus automating the selection of the oracle data. Experimental results obtained by employing our method over six industrial systems (while varying test input types and the number of generated mutants) indicate that our method—when paired with test inputs generated either at random or to satisfy specific structural coverage criteria—may be a cost-effective approach for producing small, effective oracle data sets, with fault finding improvements over current industrial best practice of up to 1,435% observed (with typical improvements of up to 50%).
  • Thumbnail Image
    Item
    Automated Oracle Data Selection Support
    (IEEE, 2015-06) Gay, Gregory; Staats, Matt; Whalen, Michael; Heimdahl, Mats
    The choice of test oracle—the artifact that determines whether an application under test executes correctly—can significantly impact the effectiveness of the testing process. However, despite the prevalence of tools that support test input selection, little work exists for supporting oracle creation. We propose a method of supporting test oracle creation that automatically selects the oracle data—the set of variables monitored during testing—for expected value test oracles. This approach is based on the use of mutation analysis to rank variables in terms of fault-finding effectiveness, thus automating the selection of the oracle data. Experimental results obtained by employing our method over six industrial systems (while varying test input types and the number of generated mutants) indicate that our method—when paired with test inputs generated either at random or to satisfy specific structural coverage criteria—may be a cost-effective approach for producing small, effective oracle data sets, with fault finding improvements over current industrial best practice of up to 1,435% observed (with typical improvements of up to 50%).
  • Thumbnail Image
    Item
    Certificate Management: A Practitioner's Perspective
    (ACM, 2005) Whalen, Michael
    Standards for critical avionics software development, such as DO178B, place a strong emphasis on process issues: ensuring traceability between different development artifacts and proper configuration management of these artifacts. Certification Management (CM) systems formalize many of the relationships between different artifacts and hold the promise of both streamlining the management of the artifacts and ensuring that relationships between the artifacts are formally justified. However, to be useful in an industrial context, the definition and scope of CM systems must be better understood, and several open issues must be addressed. This paper describes issues and potential uses of CM systems in industrial practice.
  • Thumbnail Image
    Item
    Certification Support for Automatically Generated Programs
    (IEEE Computer Society, 2003) Schumann, Johann; Fischer, Bernd; Whalen, Michael
    Although autocoding techniques promise large gains in software development productivity, their "real-world" application has been limited, particularly in safety-critical domains. Often, the major impediment is the missing trustworthiness of these systems: demonstrating — let alone formally certifying — the trustworthiness of automatic code generators is extremely difficult due to their complexity and size. We develop an alternative product-oriented certification approach which is based on five principles: (1) trustworthiness of the generator is reduced to the safety of each individual generated program; (2) program safety is defined as adherence to an explicitly formulated safety policy; (3) the safety policy is formalized by a collection of logical program properties; (4) Hoare-style program verification is used to show that each generated program satisfies the required properties; (5) the code generator itself is extended to automatically produce the code annotations required for verification. The approach is feasible because the code generator has full knowledge about the program under construction and about the properties to be verified. It can thus generate all auxiliary code annotations a theorem prover needs to discharge all emerging verification obligations fully automatically. Here we report how this approach is used in a certification extension for AUTOBAYES, an automatic program synthesis system which generates data analysis programs (e.g., for clustering and time-series analysis) from declarative specifications. In particular, we describe how a variable-initialization-before-use safety policy can be encoded and certified.
  • Thumbnail Image
    Item
    Certifying Synthesized Code
    (Springer-Verlag, 2002) Whalen, Michael; Fischer, Bernd; Schumann, Johann
    Code certication is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satises certain quality properties. These proofs serve as certicates that can be checked independently. Since code certication uses the same underlying technology as program verication, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone. We address this problem by combining code certication with automatic program synthesis. Given a high-level specication, our approach simultaneously generates code and all annotations required to certify the generated code. We describe a certication extension of AutoBayes, a synthesis tool for automatically generating data analysis programs. Based on built-in domain knowledge, proof annotations are added and used to generate proof obligations that are discharged by the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator- and memory-safety on a data-classication program. For this program, our approach was faster and more precise than PolySpace, a commercial static analysis tool.
  • Thumbnail Image
    Item
    Challenges in Testing Next Generation CPS Systems
    (2017) Whalen, Michael
    Testing cyber-physical systems presents a unique set of testing challenges: heterogeneity, timing, and, especially, observability. In particular, some of the mechanisms that are designed to make embedded software robust are the same mechanisms that present challenges for automated testing techniques: e.g., rate limiting, fault masking, and debounce logic, which can lead to long lags between problematic inputs and their manifestation in system outputs. In addition, much of the control behavior of CPS is mathematically intensive more than "branchy". For such systems, traditional coverage metrics, which focus on reaching program statements or mutants (as in weak mutation), rather than observing their affect on system outputs, are likely to lead to poor fault-finding in practice. I will describe some recent work in the area of test generation and code metrics that begins to address these issues. I then argue that this mismatch will become significantly worse for when examining CPS systems that incorporate machine learning: the complexity of the non-linear mathematics used defeats all known symbolic techniques and the lack of a traditional branching structure renders traditional code coverage metrics fairly meaningless when using search-based testing. In fact, a recent paper abstract claims: "We propose a novel control flow obfuscation design based on the incomprehensibility of artificial neural networks to fight against reverse engineering tools including concolic testing." Traditional testing of such systems has focused on checking their behavior against a large corpus of examples; unfortunately, it is known that such systems are often not robust against malicious inputs even after extensive training and testing. I hope to challenge participants to focus research into such mathematically intensive systems and to begin to create rigorous metrics that are applicable to such systems.
  • 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 a Medical Device System
    (ACM, 2013) Murugesan, Anitha; Whalen, Michael; Rayadurgam, Sanjai; Heimdahl, Mats
    Complex systems are by necessity hierarchically organized; they are decomposed into subsystems for intellectual control as well as the ability to have the subsystems created by several distinct teams. This decomposition affects both requirements and architecture; the architecture describes the structure and this affects how requirements are ``flowed down'' to each subsystem, and discoveries in the design process may affect the requirements. Demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem. In this paper, we present a medical device case example where we apply an iterative approach to architecture and verification based on software architectural models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe the requirements at different levels of abstraction for compositional verification. The component-level behavior for the model is described in Simulink/Stateflow. We assemble proofs of system level properties by using the Simulink Design Verifier to establish component-level properties and an open-source plug-in for the OSATE AADL environment to perform the compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design, verification, and detailed behavioral models, and to scale formal analysis to large software systems.
  • 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
    Coverage Metrics for Requirements-Based Testing
    (ACM, 2006) Whalen, Michael; Rajan, Ajitha; Heimdahl, Mats
    In black-box testing, one is interested in creating a suite of tests from requirements that adequately exercise the behavior of a software system without regard to the internal structure of the implementation. In current practice, the adequacy of black box test suites is inferred by examining coverage on an executable artifact, either source code or a software model. In this paper, we define structural coverage metrics directly on high-level formal software requirements. These metrics provide objective, implementation-independent measures of how well a black-box test suite exercises a set of requirements. We focus on structural coverage criteria on requirements formalized as LTL properties and discuss how they can be adapted to measure finite test cases. These criteria can also be used to automatically generate a requirements-based test suite. Unlike model or code-derived test cases, these tests are immediately traceable to high-level requirements. To assess the practicality of our approach, we apply it on a realistic example from the avionics domain.