cleaned up text not being used

proposal.tex

@@ -92,13 +92,12 @@ Past experience, with a tutorial on a-causal modelling (and Modelica in particul
 a proper explanation takes time and (2) that the topic of (PID) control is the ``missing link'': it demonstrates where code gets generated
 and deployed (or conversely, where the code running in modern software-intensive systems comes from).
 
-The proposal has two main parts. The first three hour part covers modelling of physical systems down to computational causality assignment
-resulting in Causal Block Diagrams (CBDs). The second three hour part starts by explaining the semantics of CBDs. This makes the link between
-the models of physical systems and their ultimate realization in simulation software (as used in the Functional Mockup Interface standard).
+The proposal has two main parts. 
+The first three hour part covers modelling of physical systems down to computational causality assignment resulting in Causal Block Diagrams (CBDs). 
+The second three-hour part starts by explaining the semantics of CBDs. This makes the link between the models of physical systems and their ultimate realization in simulation software (as used in the Functional Mockup Interface standard).
 The second link between physical systems and software comes from the introduction of controllers which steer a physical system (known as ``plant'') to a desired behaviour. It is these controllers that are first modelled as CBDs and subsequently discretized and realized as software.
 
-The two parts can be followed independently, but for full understanding of the CBD/PID part, it is best taken after the part focusing on the
-physics.
+The two parts can be followed independently, but for full understanding of the CBD/PID part, it is best taken after the part focusing on the physics.
 
 \subsection*{Level of the Tutorial}
 Introductory: 
@@ -126,7 +125,6 @@ It goes to the essence of the following language families, sorted from the lowes
     and
   \item black-box causal discretized (e.g., Functional Mockup Units);
   \item untimed ``algebraic'' block diagrams (and their link with synchronous data flow).
-
 \end{enumerate}
 
 Note that the first three topics are covered in the first three hour part of the tutorial.
@@ -176,135 +174,4 @@ A number of sample slides of the previous versions of the tutorial are attached
 
 \includepdf[pages={1-},angle=90]{slides.pdf}
 
-\end{document}
-
-The tutorial is divided in five parts, discussing different topics related to Statecharts:
-\begin{enumerate}
-	\item An introduction that explains the origins of the Statecharts formalism (both the syntax, coming from state diagrams, and the semantics, coming from state automata), and what classes of system it is good at representing (30 minutes).
-	\item The main part that deals with the different Statecharts constructs (syntax and semantics), how to \textbf{model} with them, and how to \textbf{simulate} them (using \textsc{Yakindu}) (3 hours).
-	\item A part on how to test models: first conceptually (building a generator and an oracle model), then using the testing framework implementation of \textsc{Yakindu} (30 minutes).
-	\item A part on how to deploy Statecharts models on different platforms: code generated for a virtual application or onto hardware (controller software for controlling a physical plant) (30 minutes).
-	\item The final part, explaining advanced concepts such as semantic options for configuring Statecharts, real-time execution of Statecharts, and how code generated from Statecharts can interact with different platforms, such as (graphical) user interfaces and games (1,5 hour).
-\end{enumerate}
-
-Throughout the different parts of the tutorial, the ``conceptual'' or ``theoretical'' explanation of Statecharts is followed by a practical application in \textsc{Yakindu}.
-This ensures diversity for the participants: they will learn about a particular Statechart construct and be able to immediately use it in a modeling and simulation environment.
-We have three presenters: Simon Van Mierlo and Hans Vangheluwe from the Univerity of Antwerp will be the presenters of the conceptual parts, and Axel Terfloth, from itemis, will lead the practical parts.
-As such, we can bring expertise both from the academic side and the tool builder side to offer a tutorial where participants can optimally be introduced to all aspects of Statecharts.
-
-In the following subsections, we give detailed information on the content of the five parts of the tutorial.
-
-\subsection{Introduction}
-In the introduction, we start by explaining the causes of complexity in reactive systems; such systems
-\begin{itemize}
-	\item interact with the environment (by processing \textit{events} coming from the environment continuously);
-	\item exhibit autonomous behavior;
-	\item exhibit concurrent behavior.
-\end{itemize}
-We explain that this type of behavior is fundamentally different from ``transformational'' programs typically encoded using a high-level programming language, and explain why Statecharts is an appropriate formalism to model their behavior by abstracting the system's behavior using the discrete-event paradigm.
-To effectively develop reactive systems, traditional approaches based on threads and timeouts add accidental complexity, as they focus on ``how'' the system's behavior 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.
-
-Statechart models are usually specified in a visual syntax (an extension of state diagrams), allowing developers to efficiently create and maintain large-scale models.
-The notation is based on higraphs: a combination of hypergraphs with Euler diagrams for adding depth and orthogonality.
-We explain the notation's origins of and look at it from a set theoretical perspective; this is important to fully understand the notion of hierarchical states and orthogonal regions in Statecharts.
-
-We also explain the running example: a traffic light, which autonomously switches between its lights using timeouts.
-Its autonomous behavior can be interrupted and restored by a policeman that pushes a button.
-In autonomous mode, a timer shows the time left until the light switches.
-This example has the necessary complexity: reactivity, orthogonality, and timing behavior.
-Moreover, we can deploy this example on multiple platforms and will bring a hardware prototype based on the Arduino platform to demonstrate this.
-
-A workflow for specifying, simulating, testing, and deploying Statecharts models is presented that guides developers through the different phases of system development.
-In the next part(s) of the tutorial, we use the following workflow:
-\begin{enumerate}
-  \item First, a set of requirements are gathered: these are properties the system's behavior needs to satisfy, and are typically described in text.
-  \item Then, an initial design (a Statechart model) is created.
-  The model implements (a part of) the system's requirements.
-  \item The model needs to be verified (i.e., we need to check whether its behavioral 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 iterations, and its behavior is properly verified, code can be generated to deploy it.
-\end{enumerate}
-
-\subsection{Modeling and Simulating with Statecharts}
-In this second part, we explain the language elements that the Statecharts language offers.
-We start by explaining the basic concepts of \emph{states} and \emph{transitions}.
-This allows us to model a simple system, such as an autonomous traffic light that switches between its lights autonomously.
-It requires us, however, to touch on a number of fundamental concepts of Statecharts:
-\begin{itemize}
-	\item The \emph{configuration} of a Statechart, represented by its \emph{current state} and the values of variables that are stored in its \emph{data store}.
-	\item The \emph{initialization} of a Statechart (by \emph{entering} the \emph{initial state}).
-	\item The \emph{triggering} of a transition by evaluating its \emph{triggering condition}, consisting of a \emph{triggering event} and a \emph{constraint} over the variable values.
-	\item The \emph{selection} of a transition if multiple transitions are triggered at the same time (leading to non-determinism!), by for example assigning priorities.
-	\item The \emph{execution} of a transition by \emph{leaving} the source state and \emph{entering} the target state of the transition, as well as execution the \emph{transition action} (which can generate an event, and/or assign values to variables).
-\end{itemize}
-We will explain these fundamental concepts in-depth, as they are necessary to understand the rest of the tutorial.
-With these concepts, the participants can already get familiar with many of the features of \textsc{Yakindu} as well.
-
-Next, we look at \emph{hierarchy}: states can be \emph{nested}.
-For correct initialization, we need to specify a default state at each level of the hierarchy.
-We need to revisit transition execution as well: when a transition is executed, we need to leave not a single state, but a hierarchy of states, and enter not a single state, but a hierarchy of states.
-For both these points, we can describe the semantics of Statecharts by a \emph{flattening} procedure: we can transform to a ``basic'' Statechart model with no hierarchy.
-This can lead to issues, however, since now transitions on higher levels of the hierarchy are also defined on any state that is lower in the hierarchy.
-This can lead to (unwanted) non-determinism, if multiple transitions are triggered in the hierarchy at the same time: different options for managing this non-determinism are discussed.
-
-Next, we discuss history states, which allow for the current configuration (excluding the values of variables in the store) to be remembered and restored.
-We approach this from an implementation view: when a transition is executed and it leaves a state that contains a history state, the current configuration has to be remembered.
-When a history state is the target of a transition, that configuration is restored by entering the remembered states.
-We explain the difference between deep history and shallow history.
-
-Last, we explain orthogonality: states can not only be combined by nesting them hierarchically, but also by combining them in orthogonal regions.
-This requires us to completely revisit the execution algorithm for finding triggering transitions, selecting one, and executing it: now this process has to be done for each orthogonal region.
-This gives rise to ``steps'': in each step, each orthogonal region gets the chance to execute a transition.
-Regions can communicate by raising events (that are stored in an internal event queue, ready to be consumed in the next step) or by constraining the execution of a transition based on the current state of another orthogonal region.
-This leads to many potential interactions that have to be managed by the modeler.
-We will spend a significant amount of time on the conceptual explanation, as well as the practical hands-on in \textsc{Yakindu}, to explain orthogonality in Statecharts properly.
-
-At the end of this part of the tutorial, the participants will have modeled an interruptible traffic light in \textsc{Yakindu} and have used the simulation capabilities of \textsc{Yakindu} to verify that the correct behavior has been implemented.
-
-\subsection{Testing Statecharts}
-Once the Statechart model of the traffic light system has been constructed, it can be tested to check whether it satisfies the requirements.
-A test consists of an input event trace, and an ``oracle'' that checks whether the output event trace satisfies the behavioral property.
-This means that a test can be seen as a timed, reactive system as well.
-The tests in this tutorial, therefore, are first modeled with Statecharts as well.
-They can either be modeled as three communicating Statecharts (the input Statechart, the model under test, and the oracle -- corresponding to a black-box approach), or in a single Statechart model in orthogonal components (corresponding to a white-box approach).
-Both approaches will be covered, and their advantages and disadvantages will be discussed.
-
-For the practical part, \textsc{Yakindu}'s \emph{SCTUnit} will be used to model the test cases for our example system.
-The testing framework allows a modeler to define an input trace (generating events), to advance the \emph{virtual time} of the test execution, and to check (through \emph{assertions}) whether the Statechart reacts correctly.
-The participants will construct a number of test cases, corresponding to a number of requirements (use cases).
-
-\subsection{Deploying Statecharts}
-The last step in system development is the deploying of the software on a \emph{platform}.
-This is an interesting step as its complexity is often overlooked: code is generated in a particular high-level programming language (such as C++, Java, or Python) and executed on a (possibly real-time) operating system; we need to ensure that the semantics of the running system corresponds to the behavior observed in the simulations and in the tests.
-While we will not go into all the details of deploying real-time systems, we will cover two platforms to demonstrate that the Statechart model can be used to implement the same behavior on very different platforms:
-\begin{enumerate}
-	\item A Java GUI application allows for a ``gentle'' transition from the simulations in \textsc{Yakindu} to a deployed (virtual) application: the generated code of the Statechart is coupled to a GUI (displaying the state of the system and allowing for the user to interact through button presses).
-	\item A hardware prototype based on the Arduino platform allows the participants to see a ``real'' deployment onto embedded hardware, used to control a physical ``plant'' (the traffic light, in this case represented by three led-lights and a push button).
-\end{enumerate}
-These deployments illustrate the platform-independent nature of Statecharts; it is only when the code is generated and \emph{bound} to platform-specific functions that a choice for the implementation is made.
-
-\subsection{Advanced Concepts}
-The last part of the tutorial is used to cover a number of advanced concepts: \emph{semantic choices} related to Statecharts execution semantics, the \emph{real-time} execution of Statechart models, the binding to execution \emph{platforms} such as a UI or a game engine, and the \emph{coordination} of multiple Statecharts.
-
-For the semantic options, we will base the discussion on the work of Esmaeilsabzali et al.~\cite{Esmaeilsabzali_BigStepModellingLanguages}.
-This will require us to break the ``stepping'' semantics of Statecharts down to a series of big steps, combo steps, and small steps.
-We explain the semantic choices arising from this: \emph{big step maximality}, \emph{combo step maximality}, \emph{internal event lifeline}, \emph{input event lifeline}, \emph{transition priority} and \emph{small step concurrency}.
-This illustrates the fact that Statecharts is not a single language: it is a \emph{family} of languages; a tool can allow for users to configure the simulator/code generator to suit the needs of the application.
-
-Real-time execution of Statecharts is important from a conceptual point of view, and for participants that are interested in how a Statechart simulator/executor is implemented.
-Naively, the delays encoded in the Statechart transition can be taken as the values for a \emph{sleep} call in the operating system to implement the waiting periods in the execution of a Statechart model.
-This does not take into account, however, the time it takes for the action code to complete.
-In certain cases, this can make the clock \emph{drift} significantly.
-The tutorial will cover methods to ensure this does not happen, with a practical implementation.
-This method also allows to scale up or slow down the execution (\emph{scaled} real-time execution).
-
-Different platforms, such as game loops and user interfaces, can be ``in control'' of the application (they implement a ``main loop'' that the generated code of the Statechart model has to interact with).
-This is different from stand-alone applications generated from a Statechart model, that implement their own ``main loop'': an (infinite) while-loop that listens for input events and produces output events to the environment.
-We discuss such platforms, and in particular show how generated Statechart code can integrate with the event loop of a UI platform (where Statecharts events are interleaved with UI events) and the game loop of a game engine (where the Statechart execution algorithm is only called at a certain \emph{polling interval)}.
-
-Last, we discuss the coordination of multiple Statechart instances.
-We will look at SCCD~\cite{VanMierlo_SCCD}, a hybrid formalism that combines Statecharts with class diagrams to implement dynamic-structure systems consisting of a set of objects (that conform to classes), whose behaviour is specified in Statecharts.
-The objects can communicate (using events) by creating \emph{links} to other objects (that conform to associations).
-For the practical part, we will demonstrate how multiple traffic light models can be coordinated using \textsc{Yakindu}.
+\end{document}