University of Minnesota
Software Engineering Center

You are here

Gabor Karsai

Recent Publications

Improving Symbolic Execution for Statecharts Formalisms

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.

Integrating Statechart Components in Polyglot

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,

Polyglot: Modeling and Analysis for Multiple Statechart Formalisms

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.