18.10.MoDELS.SCTutorial/tutorial_description.tex

%!TEX root = main.tex
The tutorial starts by explaining the causes of complexity in reactive systems, and explains why Statecharts is an appropriate formalism to model their behaviour.
A workflow for specifying, simulating, testing, and deploying Statecharts models is presented, and a running example is used to discuss the features of the Statecharts language and the Yakindu modelling and simulation tool.
As a last step, the system is deployed by generating code from the model.

A more in-depth discussion of the steps presented during the tutorial is provided below.

\begin{itemize}
  \item Explanation of the source of (essential) complexity in engineered systems, which often can be attributed to them having timed, reactive, autonomous behaviour.
  A number of such systems are presented to demonstrate this complexity.
  To effectively develop these systems, traditional approaches based on threads and timeouts add accidental complexity.
  These approaches focus on ``how'' the system's behaviour is implemented, instead of ``what'' the system is supposed to do.
  Instead, a language which has notions of \emph{events}, \emph{timeouts} and \emph{concurrent units} is needed.
  \item Introduction of the notion of discrete-event abstraction, in which a system's autonomous behaviour can be interrupted by external events coming from the environment, and the system can produce output to that environment.
  \item Introduction of Statecharts as an appropriate formalism to model a reactive system's behaviour using a discrete-event abstraction.
  \item Introduction of the running example of the tutorial: a traffic light.
  This example is basic, but has all essential complexity: it is timed, its lights have to switch autonomously, and it is reactive, since its normal execution can be interrupted by a policeman.
  \item Throughout the tutorial, a workflow for designing, testing, and deploying systems using Statecharts is presented:
    \begin{enumerate}
      \item First, a set of requirements are gathered: these are properties the system's behaviour needs to satisfy, and are typically described in text.
      \item Then, an initial design is created as a Statecharts model.
      The model implements (part of) the system's specification.
      \item The model needs to be verified (i.e., we need to check whether its behavioural properties are satisfied).
      To do this, the model can be \emph{simulated} (in which the user defines a simulation scenario and checks the outcome of the simulation manually) or it can be \emph{tested} (in which the user defines a number of test cases, which consist of a set of timed inputs that are supplied to the model, and an automatic checker or ``oracle'' that verifies whether the test succeeds).
      If a simulation or test results in a \emph{failure} (i.e., one of the system's properties is not satisfied), the system's model needs to be revised.
      \item When the system's design has gone through several simulation and testing phases, and its behaviour is properly verified, code can be generated to deploy it.
    \end{enumerate}
  \item With the workflow in mind, an explanation follows of the basic building blocks of Statecharts: \emph{states} and \emph{transitions} (which are triggered by \emph{events} and optionally have a constraint that needs to be satisfied).
  \item Progressively introduce new elements of the Statecharts language: hierarchy, orthogonality, and history.
  For each concept, both the syntax and the semantics of the concept is explained and applied to the example.
  And, a demonstration of each concept (including simulation to demonstrate semantics) in the Yakindu modelling and simulation tool.
  \item Demonstration of the testing of Statecharts models.
  Since a test consists of an input event trace, and an ``oracle'' which checks the output event trace, a test can be seen as a timed, reactive system as well.
  The tests in this tutorial, therefore, are modelled with Statecharts as well.
  They can either be modelled as three communicating Statecharts (the input Statechart, the model under test, and the oracle), or in a single Statechart model in orthogonal components.
  \item Demonstration of code generation (to Java).
  For this, the code generation capabilities of the Yakindu tool are used.
  A generic visualization for the traffic light example is built, with which the generated code from the behavioural model communicates through the interface of the model (input/output events).
\end{itemize}