Definition of the formal semantics of control state diagrams and implementation of a graphical editor

Abstract

Abstract State Machines (ASM) are a formal specification language which is used in the software and system engineering. Different to UML2 diagrams, which are another well-known, graphical, formal specification language, ASMs are mostly used for scientific work and are textual based. Control State ASMs are a special class of ASMs which are similar to Finite State Machines, but extends them by parallelism and data structure manipulation.

To give a better overview of their Control State ASM specifications, flowchart-like charts are often made. They also help the reader understand the ASMs. Such graphical representation are then called Control State Diagrams (CSD). Because these CSDs are yet not fully specified, they often lead to confusion and misunderstandings, because often nothing is said about the behavior of CSDs and there is no full list of possible shapes of them.

This work will take the actual literature, analyzes the existing CSDs and the corresponding ASMs and derive a full definition of the syntax and semantics of CSDs in the form of a formal specification. Additionally a prototype of a graphical editor is implemented, with which CSDs can be created and transformed to CoreASM, a special ASM tool which is used to run ASMs on a computer.