1.4.1 Formal Specification

Figure 1.10: Specification of DCharts

The syntax and semantics of DCharts are formally specified in this thesis (Figure 1.10).

Three types of syntaxes are described:

• The abstract syntax is a symbolic language. It gives a symbol to every entity in DCharts. Relations are regarded as functions. This syntax is formal and it allows logical reasoning or inference on DCharts models. It also makes it possible to mathematically transform or simplify DCharts models.

• The textual syntax defines the textual form of the formalism. This form simplifies computer processing of a DCharts model. The textual syntax is implemented in this thesis work with a parser and interpreter.

• The graphical syntax gives a graphical representation for the formalism. It provides a way to design DCharts models in a modeling environment that supports GUI (Graphical User Interface), such as AToM$^3$. In many cases graphical model design is more user-friendly and understandable. Part of the graphical syntax is implemented in a DCharts meta-model in AToM$^3$, so that designers can manipulate DCharts models in this environment.

The semantics of DCharts is formally defined in two different ways:

• Operational semantics defines the meaning of DCharts models with a functional description or pseudo-code. From this description, an interpreter (SVM, Statechart Virtual Machine) and a code synthesizer (SCC, StateChart Compiler) for DCharts are constructed.

• Denotational semantics maps DCharts to other existing formalisms such as statecharts and DEVS. The DCharts semantics is made clear provided that the formalisms that we map onto have well-defined semantics. Denotational semantics provides a way to transform DCharts models into models in other formalisms.