Browsing by Author "Biatek, Jason"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    Helping System Engineers Bridge the Peaks
    (ACM, 2014) Rungta, Neha; Person, Suzette; Biatek, Jason; Whalen, Michael; Castle, Joseph; Gundy-Burlet, Karen
    In our experience at NASA, system engineers generally follow the Twin Peaks approach when developing safety-critical systems. However, iterations between the peaks require considerable manual, and in some cases duplicate, effort. A significant part of the manual effort stems from the fact that requirements are written in English natural language rather than a formal notation. In this work, we propose an approach that enables system engineers to leverage formal requirements and automated test generation to streamline iterations, effectively "bridging the peaks". The key to the approach is a formal language notation that a) system engineers are comfortable with, b) is supported by a family of automated V&V tools, and c) is semantically rich enough to describe the requirements of interest. We believe the combination of formalizing requirements and providing tool support to automate the iterations will lead to a more effcient Twin Peaks implementation at NASA.
  • Thumbnail Image
    Item
    Improving Symbolic Execution for Statecharts Formalisms
    (ACM, 2012) Balasubramanian, Daniel; Păsăreanu, Corina; Whalen, Michael; Biatek, Jason; Karsai, Gabor; Lowry, Michael
    Symbolic execution is a program analysis technique that attempts to explore all possible paths through a program by using symbolic values rather than actual data values as inputs. When applied to Statecharts, a model-based formalism for reactive systems, symbolic execution can determine all feasible paths through a model up to a specified bound and generate input sequences exercising these paths. The main drawback of this method is its computational expense. This paper describes two efforts to improve the performance of symbolic execution within our previously developed framework for Statechart analysis. One method is a multithreaded symbolic execution engine targeted directly at our framework. A second, orthogonal, method is program specialization with respect to a particular model and Statechart semantics, which uses symbolic execution to rewrite the original code into an equivalent form that has fewer instructions and is easier to analyze.
  • Thumbnail Image
    Item
    Integrating Statechart Components in Polyglot
    (Springer-Verlag, 2012) Balasubramanian, Daniel; Păsăreanu, Corina; Biatek, Jason; Whalen, Michael; Karsai, Gabor; Lowry, Michael; Pressburger, Thomas
    Statecharts is a model-based formalism for simulating and analyzing reactive systems. In our previous work, we developed Polyglot, a unified framework for analyzing different semantic variants of Statechart models. However, for systems containing communicating, asynchronous components deployed on a distributed platform, additional features not inherent to the basic Statecharts paradigm are needed. These include a connector mechanism for communication, a scheduling framework for sequencing the execution of individual components, and a method for specifying verification properties spanning multiple components. This paper describes the addition of these features to Polyglot, along with an example NASA case study using these new features. Furthermore, the paper describes on-going work on modeling Plexil execution plans with Polyglot, which enables the study of interaction issues for future manned and unmanned missions.