|
|
@@ -1,6 +1,12 @@
|
|
|
%!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 Discovery of the complexity in engineerd systems, which often can be attributed to them having timed, reactive, autonomous behaviour.
|
|
|
+ \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.
|
|
|
@@ -8,25 +14,25 @@
|
|
|
\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, since its lights have to switch autonomously, and it is reactive, since its normal execution can be interrupted by a policeman.
|
|
|
+ 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 (\emph{i.e.}, we need to check whether its behavioural properties are satisfied).
|
|
|
+ \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, explanation 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 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 communication Statecharts (the input Statechart, the model under test, and the oracle), or in a single Statechart model in orthogonal components.
|
|
|
+ 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).
|
