University of Minnesota
Software Engineering Center

You are here

Jason Biatek

Student/Research Assistant
Office Location: 
6-248 Keller Hall
Current: Computer Science doctoral student, University of Minnesota
B.A. Computer Science with distinction, University of Minnesota Morris, 2010
When designing safety-critical software, being completely sure of its correctness is vital. I am interested in formal methods such as model checking techniques and applying them to real-world software to verify its correctness. I have worked on Simulink/Stateflow and Rational Rhapsody models, using tools such as Reactis and Java PathFinder to perform analysis on them, as well as writing a translator from the Plexil language into Java and Rhapsody.

Recent Publications

Helping System Engineers Bridge the Peaks

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".

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,