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 "Karsai, Gabor"

Now showing 1 - 3 of 3
  • 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.
  • Thumbnail Image
    Item
    Polyglot: Modeling and Analysis for Multiple Statechart Formalisms
    (ACM, 2011) Balasubramanian, Daniel; Păsăreanu, Corina; Whalen, Michael; Karsai, Gabor; Lowry, Michael
    In large programs such as NASA Exploration, multiple systems that interact via safety-critical protocols are already designed with dierent Statechart variants. To verify these safety-critical systems, a unied framework is needed based on a formal semantics that captures the variants of Statecharts. We describe Polyglot, a unied framework for the analysis of models described using multiple Statechart formalisms. In this framework, Statechart models are translated into Java and analyzed using pluggable semantics for different variants operating in a polymorphic execution environment. The framework has been built on the basis of a parametric formal semantics that captures the common core of Statecharts with extensions for dierent variants, and addresses previous limitations. Polyglot has been integrated with the Java Pathnder verication tool-set, providing analysis and test-case generation capabilities. We describe the application of this unied framework to the analysis of NASA/JPL's MER Arbiter whose interacting components were modeled using multiple Statechart formalisms.