Some computational aspects of statecharts formal modeling of reactive systems

Grzegorz Łabiak · Common Library Network (Der Gemeinsame Bibliotheksverbund) · 2010

The paper presents a graphical notation for modeling of complex behavior of reactive systems.This notation, called statechart diagrams and invented by David Harel, features state-based description, concurrency and hierarchy.Other very essential characteristic of the diagrams is their very strict and formal definition, which allows to apply formal methods (e.g. based on state space characteristic function).This formal definition makes that, on one hand, statechart diagram can be directly implemented in programmable structure, and, on the other hand, their behavior can be analyzed against deadlock detection or can be transformed into other computational model (e.g.FSM).The paper concentrates on relations between some statechart semantic structures and their influence on the number of computational resources, what is very important for the implementation of formal methods algorithms.

Read the paper · More papers on PaperTik