Seminars

Semantics of Statecharts pdf slides
Mike Whalen,  Software Engineering Center, University of Minnesota

04/09/2010, 2pm, GHC-4405

Abstract

Statecharts are an important formalism for behavioral modeling of complex reactive systems. There are several popular dialects of Statecharts that have achieved broad use: UML Statecharts, Stateflow (part of the MATLAB tool suite), IBM Rhapsody, Esterel Technologies SyncCharts, and iLogix STATEMATE. The syntax for these notations is very similar -- in some cases identical – but there are key semantic differences. These differences cause simple charts to yield radically different behaviors depending on the semantic dialect chosen for interpretation and can cause misunderstandings between developers using different dialects. For example, UML Statecharts, Rhapsody Statecharts, and Stateflow are all being used for development of software for the NASA Constellation program.

In this talk, we describe discrepancies between different Statecharts dialects with illustrative examples. We also describe current research into analyses that can, given a statechart diagram, determine whether:

1. the semantics of the diagram are potentially non-deterministic within a dialect e.g., due to the unspecified evaluation order in UML Statecharts for parallel state machines,
   
   
2. the semantics of a diagram will be the same across multiple dialects, e.g., due to semantic differences between dialects, and
   
   
3. whether or not functional and safety properties hold across multiple dialects.
   
   These determinations are important for projects utilizing multiple Statecharts tools, and also provide insight into the semantic relationships between multiple dialects.

Biography

Dr. Michael Whalen is the Program Director at the University of Minnesota Software Engineering Center.  Dr. Whalen is interested in formal analysis, compilers, testing, and requirements engineering.  He has developed simulation, translation, testing, and formal analysis tools for MBD languages including Simulink, Stateflow, Lustre, and RSML-e, and has published over 25 papers on these topics.  He has led successful formal verification projects on large industrial avionics models, including displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program).  His PhD dissertation involved using higher-order abstract syntax as a basis for a provably-correct code generation tool from the RSML-e specification language into a subset of C.