Browse Source

initial version

Simon Van Mierlo 7 years ago
commit
2e6698c052
15 changed files with 10459 additions and 0 deletions
  1. 2417 0
      IEEEtran.bst
  2. 6347 0
      IEEEtran.cls
  3. 12 0
      abstract.tex
  4. 1025 0
      bibliography.bib
  5. 29 0
      main.aux
  6. 51 0
      main.bbl
  7. 8 0
      main.blg
  8. 472 0
      main.log
  9. 1 0
      main.out
  10. BIN
      main.pdf
  11. BIN
      main.synctex.gz
  12. 62 0
      main.tex
  13. 2 0
      make_total.sh
  14. BIN
      submission.pdf
  15. 33 0
      tutorial_description.tex

File diff suppressed because it is too large
+ 2417 - 0
IEEEtran.bst


File diff suppressed because it is too large
+ 6347 - 0
IEEEtran.cls


+ 12 - 0
abstract.tex

@@ -0,0 +1,12 @@
+%!TEX root=./main.tex
+Statecharts, introduced by Harel~\cite{Harel_Statecharts}, is used to specify complex, timed, reactive, autonomous discrete-event systems.
+It is an extension of Timed Finite State Automata which adds depth, orthogonality, broadcast communication and history.
+Its visual representation is based on higraphs, which combine graphs and Venn diagrams~\cite{Harel_VisualFormalisms}.
+This representation is most suited to represent Statecharts models, and many tools offer visual editing and simulation support for the Statecharts formalism.
+Examples include STATEMATE~\cite{Harel1996}, Rhapsody~\cite{Harel_Rhapsody}, Yakindu~\footnote{\url{https://www.itemis.com/en/yakindu/statechart-tools/}}, and Stateflow~\footnote{\url{https://www.mathworks.com/products/stateflow.html}}.
+
+This tutorial introduces Statecharts modelling, simulation, and testing.
+As a running example, the behaviour of a simple timed, autonomous, reactive system is modelled: a traffic light.
+We start from the basic concepts of states and transitions and explain the more advanced concepts of Statecharts by extending the example incrementally.
+We discuss several semantics options, such as STATEMATE and Rhapsody semantics.
+We use Yakindu to model the example system.

File diff suppressed because it is too large
+ 1025 - 0
bibliography.bib


+ 29 - 0
main.aux

@@ -0,0 +1,29 @@
+\relax 
+\providecommand\hyper@newdestlabel[2]{}
+\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
+\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
+\global\let\oldcontentsline\contentsline
+\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
+\global\let\oldnewlabel\newlabel
+\gdef\newlabel#1#2{\newlabelxx{#1}#2}
+\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
+\AtEndDocument{\ifx\hyper@anchor\@undefined
+\let\contentsline\oldcontentsline
+\let\newlabel\oldnewlabel
+\fi}
+\fi}
+\global\let\hyper@last\relax 
+\gdef\HyperFirstAtBeginDocument#1{#1}
+\providecommand\HyField@AuxAddToFields[1]{}
+\providecommand\HyField@AuxAddToCoFields[2]{}
+\citation{Harel_Statecharts}
+\citation{Harel_VisualFormalisms}
+\citation{Harel1996}
+\citation{Harel_Rhapsody}
+\bibstyle{IEEEtran}
+\bibdata{bibliography}
+\bibcite{Harel_Statecharts}{1}
+\bibcite{Harel_VisualFormalisms}{2}
+\bibcite{Harel1996}{3}
+\bibcite{Harel_Rhapsody}{4}
+\@writefile{toc}{\contentsline {section}{References}{2}{section*.11}}

+ 51 - 0
main.bbl

@@ -0,0 +1,51 @@
+% Generated by IEEEtran.bst, version: 1.12 (2007/01/11)
+\begin{thebibliography}{1}
+\providecommand{\url}[1]{#1}
+\csname url@samestyle\endcsname
+\providecommand{\newblock}{\relax}
+\providecommand{\bibinfo}[2]{#2}
+\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
+\providecommand{\BIBentryALTinterwordstretchfactor}{4}
+\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
+\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
+  \fontdimen4\font\relax}
+\providecommand{\BIBforeignlanguage}[2]{{%
+\expandafter\ifx\csname l@#1\endcsname\relax
+\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
+\typeout{** loaded for the language `#1'. Using the pattern for}%
+\typeout{** the default language instead.}%
+\else
+\language=\csname l@#1\endcsname
+\fi
+#2}}
+\providecommand{\BIBdecl}{\relax}
+\BIBdecl
+
+\bibitem{Harel_Statecharts}
+D.~Harel, ``Statecharts: a visual formalism for complex systems,''
+  \emph{Science of Computer Programming}, vol.~8, no.~3, pp. 231--274, June
+  1987.
+
+\bibitem{Harel_VisualFormalisms}
+\BIBentryALTinterwordspacing
+------, ``On visual formalisms,'' \emph{Commun. ACM}, vol.~31, no.~5, pp.
+  514--530, May 1988. [Online]. Available:
+  \url{http://doi.acm.org/10.1145/42411.42414}
+\BIBentrySTDinterwordspacing
+
+\bibitem{Harel1996}
+\BIBentryALTinterwordspacing
+D.~Harel and A.~Naamad, ``{The STATEMATE Semantics of Statecharts},'' \emph{ACM
+  Trans. Softw. Eng. Methodol.}, vol.~5, no.~4, pp. 293--333, oct 1996.
+  [Online]. Available: \url{http://doi.acm.org/10.1145/235321.235322}
+\BIBentrySTDinterwordspacing
+
+\bibitem{Harel_Rhapsody}
+D.~Harel and H.~Kugler, \emph{Integration of Software Specification Techniques
+  for Applications in Engineering: Priority Program SoftSpez of the German
+  Research Foundation (DFG), Final Report}.\hskip 1em plus 0.5em minus
+  0.4em\relax Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, ch. The
+  Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML),
+  pp. 325--354.
+
+\end{thebibliography}

+ 8 - 0
main.blg

@@ -0,0 +1,8 @@
+This is BibTeX, Version 0.99dThe top-level auxiliary file: main.aux
+The style file: IEEEtran.bst
+Database file #1: bibliography.bib
+-- IEEEtran.bst version 1.12 (2007/01/11) by Michael Shell.
+-- http://www.michaelshell.org/tex/ieeetran/bibtex/
+-- See the "IEEEtran_bst_HOWTO.pdf" manual for usage information.
+
+Done.

+ 472 - 0
main.log

@@ -0,0 +1,472 @@
+This is pdfTeX, Version 3.14159265-2.6-1.40.18 (MiKTeX 2.9.6600 64-bit) (preloaded format=pdflatex 2018.3.15)  16 MAR 2018 20:15
+entering extended mode
+**N:/Documents/Unief/18.PostDoc/Papers/18.10.MoDELS.SCTutorial/main.tex
+(N:/Documents/Unief/18.PostDoc/Papers/18.10.MoDELS.SCTutorial/main.tex
+LaTeX2e <2017-04-15>
+Babel <3.17> and hyphenation patterns for 75 language(s) loaded.
+(IEEEtran.cls
+Document Class: IEEEtran 2015/08/26 V1.8b by Michael Shell
+-- See the "IEEEtran_HOWTO" manual for usage information.
+-- http://www.michaelshell.org/tex/ieeetran/
+\@IEEEtrantmpdimenA=\dimen102
+\@IEEEtrantmpdimenB=\dimen103
+\@IEEEtrantmpdimenC=\dimen104
+\@IEEEtrantmpcountA=\count79
+\@IEEEtrantmpcountB=\count80
+\@IEEEtrantmpcountC=\count81
+\@IEEEtrantmptoksA=\toks14
+LaTeX Font Info:    Try loading font information for OT1+ptm on input line 503.
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\psnfss\ot1ptm.fd"
+File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
+)
+-- Using 8.5in x 11in (letter) paper.
+-- Using PDF output.
+\@IEEEnormalsizeunitybaselineskip=\dimen105
+-- This is a 10 point document.
+\CLASSINFOnormalsizebaselineskip=\dimen106
+\CLASSINFOnormalsizeunitybaselineskip=\dimen107
+\IEEEnormaljot=\dimen108
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <5> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <5> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <7> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <7> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <8> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <8> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <9> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <9> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <10> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <10> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <11> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <11> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <12> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <12> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <17> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <17> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <20> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <20> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <24> not available
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 1090.
+LaTeX Font Info:    Font shape `OT1/ptm/bx/it' in size <24> not available
+(Font)              Font shape `OT1/ptm/b/it' tried instead on input line 1090.
+
+\IEEEquantizedlength=\dimen109
+\IEEEquantizedlengthdiff=\dimen110
+\IEEEquantizedtextheightdiff=\dimen111
+\IEEEilabelindentA=\dimen112
+\IEEEilabelindentB=\dimen113
+\IEEEilabelindent=\dimen114
+\IEEEelabelindent=\dimen115
+\IEEEdlabelindent=\dimen116
+\IEEElabelindent=\dimen117
+\IEEEiednormlabelsep=\dimen118
+\IEEEiedmathlabelsep=\dimen119
+\IEEEiedtopsep=\skip41
+\c@section=\count82
+\c@subsection=\count83
+\c@subsubsection=\count84
+\c@paragraph=\count85
+\c@IEEEsubequation=\count86
+\abovecaptionskip=\skip42
+\belowcaptionskip=\skip43
+\c@figure=\count87
+\c@table=\count88
+\@IEEEeqnnumcols=\count89
+\@IEEEeqncolcnt=\count90
+\@IEEEsubeqnnumrollback=\count91
+\@IEEEquantizeheightA=\dimen120
+\@IEEEquantizeheightB=\dimen121
+\@IEEEquantizeheightC=\dimen122
+\@IEEEquantizeprevdepth=\dimen123
+\@IEEEquantizemultiple=\count92
+\@IEEEquantizeboxA=\box26
+\@IEEEtmpitemindent=\dimen124
+\IEEEPARstartletwidth=\dimen125
+\c@IEEEbiography=\count93
+\@IEEEtranrubishbin=\box27
+) ("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\url\url.sty"
+\Urlmuskip=\muskip10
+Package: url 2013/09/16  ver 3.4  Verb mode for urls, etc.
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\hyperref\hyperref.
+sty"
+Package: hyperref 2018/02/06 v6.86b Hypertext links for LaTeX
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\generic\oberdiek\hobsub-
+hyperref.sty"
+Package: hobsub-hyperref 2016/05/16 v1.14 Bundle oberdiek, subset hyperref (HO)
+
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\generic\oberdiek\hobsub-
+generic.sty"
+Package: hobsub-generic 2016/05/16 v1.14 Bundle oberdiek, subset generic (HO)
+Package: hobsub 2016/05/16 v1.14 Construct package bundles (HO)
+Package: infwarerr 2016/05/16 v1.4 Providing info/warning/error messages (HO)
+Package: ltxcmds 2016/05/16 v1.23 LaTeX kernel commands for general use (HO)
+Package: ifluatex 2016/05/16 v1.4 Provides the ifluatex switch (HO)
+Package ifluatex Info: LuaTeX not detected.
+Package: ifvtex 2016/05/16 v1.6 Detect VTeX and its facilities (HO)
+Package ifvtex Info: VTeX not detected.
+Package: intcalc 2016/05/16 v1.2 Expandable calculations with integers (HO)
+Package: ifpdf 2017/03/15 v3.2 Provides the ifpdf switch
+Package: etexcmds 2016/05/16 v1.6 Avoid name clashes with e-TeX commands (HO)
+Package etexcmds Info: Could not find \expanded.
+(etexcmds)             That can mean that you are not using pdfTeX 1.50 or
+(etexcmds)             that some package has redefined \expanded.
+(etexcmds)             In the latter case, load this package earlier.
+Package: kvsetkeys 2016/05/16 v1.17 Key value parser (HO)
+Package: kvdefinekeys 2016/05/16 v1.4 Define keys (HO)
+Package: pdftexcmds 2018/01/21 v0.26 Utility functions of pdfTeX for LuaTeX (HO
+)
+Package pdftexcmds Info: LuaTeX not detected.
+Package pdftexcmds Info: \pdf@primitive is available.
+Package pdftexcmds Info: \pdf@ifprimitive is available.
+Package pdftexcmds Info: \pdfdraftmode found.
+Package: pdfescape 2016/05/16 v1.14 Implements pdfTeX's escape features (HO)
+Package: bigintcalc 2016/05/16 v1.4 Expandable calculations on big integers (HO
+)
+Package: bitset 2016/05/16 v1.2 Handle bit-vector datatype (HO)
+Package: uniquecounter 2016/05/16 v1.3 Provide unlimited unique counter (HO)
+)
+Package hobsub Info: Skipping package `hobsub' (already loaded).
+Package: letltxmacro 2016/05/16 v1.5 Let assignment for LaTeX macros (HO)
+Package: hopatch 2016/05/16 v1.3 Wrapper for package hooks (HO)
+Package: xcolor-patch 2016/05/16 xcolor patch
+Package: atveryend 2016/05/16 v1.9 Hooks at the very end of document (HO)
+Package atveryend Info: \enddocument detected (standard20110627).
+Package: atbegshi 2016/06/09 v1.18 At begin shipout hook (HO)
+Package: refcount 2016/05/16 v3.5 Data extraction from label references (HO)
+Package: hycolor 2016/05/16 v1.8 Color options for hyperref/bookmark (HO)
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\graphics\keyval.st
+y"
+Package: keyval 2014/10/28 v1.15 key=value parser (DPC)
+\KV@toks@=\toks15
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\generic\ifxetex\ifxetex.
+sty"
+Package: ifxetex 2010/09/12 v0.6 Provides ifxetex conditional
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\oberdiek\auxhook.s
+ty"
+Package: auxhook 2016/05/16 v1.4 Hooks for auxiliary files (HO)
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\oberdiek\kvoptions
+.sty"
+Package: kvoptions 2016/05/16 v3.12 Key value format for package options (HO)
+)
+\@linkdim=\dimen126
+\Hy@linkcounter=\count94
+\Hy@pagecounter=\count95
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\hyperref\pd1enc.de
+f"
+File: pd1enc.def 2018/02/06 v6.86b Hyperref: PDFDocEncoding definition (HO)
+)
+\Hy@SavedSpaceFactor=\count96
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\00miktex\hyperref.
+cfg"
+File: hyperref.cfg 2002/06/06 v1.2 hyperref configuration of TeXLive
+)
+Package hyperref Info: Hyper figures OFF on input line 4509.
+Package hyperref Info: Link nesting OFF on input line 4514.
+Package hyperref Info: Hyper index ON on input line 4517.
+Package hyperref Info: Plain pages OFF on input line 4524.
+Package hyperref Info: Backreferencing OFF on input line 4529.
+Package hyperref Info: Implicit mode ON; LaTeX internals redefined.
+Package hyperref Info: Bookmarks ON on input line 4762.
+\c@Hy@tempcnt=\count97
+LaTeX Info: Redefining \url on input line 5115.
+\XeTeXLinkMargin=\dimen127
+\Fld@menulength=\count98
+\Field@Width=\dimen128
+\Fld@charsize=\dimen129
+Package hyperref Info: Hyper figures OFF on input line 6369.
+Package hyperref Info: Link nesting OFF on input line 6374.
+Package hyperref Info: Hyper index ON on input line 6377.
+Package hyperref Info: backreferencing OFF on input line 6384.
+Package hyperref Info: Link coloring OFF on input line 6389.
+Package hyperref Info: Link coloring with OCG OFF on input line 6394.
+Package hyperref Info: PDF/A mode OFF on input line 6399.
+LaTeX Info: Redefining \ref on input line 6439.
+LaTeX Info: Redefining \pageref on input line 6443.
+\Hy@abspage=\count99
+\c@Item=\count100
+\c@Hfootnote=\count101
+)
+Package hyperref Info: Driver (autodetected): hpdftex.
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\hyperref\hpdftex.d
+ef"
+File: hpdftex.def 2018/02/06 v6.86b Hyperref driver for pdfTeX
+\Fld@listcount=\count102
+\c@bookmark@seq@number=\count103
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\oberdiek\rerunfile
+check.sty"
+Package: rerunfilecheck 2016/05/16 v1.8 Rerun checks for auxiliary files (HO)
+Package uniquecounter Info: New unique counter `rerunfilecheck' on input line 2
+82.
+)
+\Hy@SectionHShift=\skip44
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsfonts\amssymb.s
+ty"
+Package: amssymb 2013/01/14 v3.01 AMS font symbols
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsfonts\amsfonts.
+sty"
+Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
+\@emptytoks=\toks16
+\symAMSa=\mathgroup4
+\symAMSb=\mathgroup5
+LaTeX Font Info:    Overwriting math alphabet `\mathfrak' in version `bold'
+(Font)                  U/euf/m/n --> U/euf/b/n on input line 106.
+))
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsmath\amsmath.st
+y"
+Package: amsmath 2017/09/02 v2.17a AMS math features
+\@mathmargin=\skip45
+
+For additional information on amsmath, use the `?' option.
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsmath\amstext.st
+y"
+Package: amstext 2000/06/29 v2.01 AMS text
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsmath\amsgen.sty
+"
+File: amsgen.sty 1999/11/30 v2.0 generic functions
+\@emptytoks=\toks17
+\ex@=\dimen130
+))
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsmath\amsbsy.sty
+"
+Package: amsbsy 1999/11/29 v1.2d Bold Symbols
+\pmbraise@=\dimen131
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsmath\amsopn.sty
+"
+Package: amsopn 2016/03/08 v2.02 operator names
+)
+\inf@bad=\count104
+LaTeX Info: Redefining \frac on input line 213.
+\uproot@=\count105
+\leftroot@=\count106
+LaTeX Info: Redefining \overline on input line 375.
+\classnum@=\count107
+\DOTSCASE@=\count108
+LaTeX Info: Redefining \ldots on input line 472.
+LaTeX Info: Redefining \dots on input line 475.
+LaTeX Info: Redefining \cdots on input line 596.
+\Mathstrutbox@=\box28
+\strutbox@=\box29
+\big@size=\dimen132
+LaTeX Font Info:    Redeclaring font encoding OML on input line 712.
+LaTeX Font Info:    Redeclaring font encoding OMS on input line 713.
+\macc@depth=\count109
+\c@MaxMatrixCols=\count110
+\dotsspace@=\muskip11
+\c@parentequation=\count111
+\dspbrk@lvl=\count112
+\tag@help=\toks18
+\row@=\count113
+\column@=\count114
+\maxfields@=\count115
+\andhelp@=\toks19
+\eqnshift@=\dimen133
+\alignsep@=\dimen134
+\tagshift@=\dimen135
+\tagwidth@=\dimen136
+\totwidth@=\dimen137
+\lineht@=\dimen138
+\@envbody=\toks20
+\multlinegap=\skip46
+\multlinetaggap=\skip47
+\mathdisplay@stack=\toks21
+LaTeX Info: Redefining \[ on input line 2817.
+LaTeX Info: Redefining \] on input line 2818.
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\tools\xspace.sty"
+Package: xspace 2014/10/28 v1.13 Space after command names (DPC,MH)
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\graphics\graphicx.
+sty"
+Package: graphicx 2017/06/01 v1.1a Enhanced LaTeX Graphics (DPC,SPQR)
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\graphics\graphics.
+sty"
+Package: graphics 2017/06/25 v1.2c Standard LaTeX Graphics (DPC,SPQR)
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\graphics\trig.sty"
+Package: trig 2016/01/03 v1.10 sin cos tan (DPC)
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\graphics-cfg\graph
+ics.cfg"
+File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
+)
+Package graphics Info: Driver file: pdftex.def on input line 99.
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\graphics-def\pdfte
+x.def"
+File: pdftex.def 2018/01/08 v1.0l Graphics/color driver for pdftex
+))
+\Gin@req@height=\dimen139
+\Gin@req@width=\dimen140
+) (main.aux)
+\openout1 = `main.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 8.
+LaTeX Font Info:    ... okay on input line 8.
+
+-- Lines per column: 56 (exact).
+\AtBeginShipoutBox=\box30
+Package hyperref Info: Link coloring OFF on input line 8.
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\hyperref\nameref.s
+ty"
+Package: nameref 2016/05/21 v2.44 Cross-referencing by name of section
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\generic\oberdiek\gettitl
+estring.sty"
+Package: gettitlestring 2016/05/16 v1.5 Cleanup title references (HO)
+)
+\c@section@level=\count116
+)
+LaTeX Info: Redefining \ref on input line 8.
+LaTeX Info: Redefining \pageref on input line 8.
+LaTeX Info: Redefining \nameref on input line 8.
+ (main.out) (main.out)
+\@outlinefile=\write3
+\openout3 = `main.out'.
+
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\context\base\supp-pdf.mk
+ii"
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count117
+\scratchdimen=\dimen141
+\scratchbox=\box31
+\nofMPsegments=\count118
+\nofMParguments=\count119
+\everyMPshowfont=\toks22
+\MPscratchCnt=\count120
+\MPscratchDim=\dimen142
+\MPnumerator=\count121
+\makeMPintoPDFobject=\count122
+\everyMPtoPDFconversion=\toks23
+)
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\oberdiek\epstopdf-
+base.sty"
+Package: epstopdf-base 2016/05/15 v2.6 Base part for package epstopdf
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\oberdiek\grfext.st
+y"
+Package: grfext 2016/05/16 v1.2 Manage graphics extensions (HO)
+)
+Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4
+38.
+Package grfext Info: Graphics extension search list:
+(grfext)             [.pdf,.png,.jpg,.mps,.jpeg,.jbig2,.jb2,.PDF,.PNG,.JPG,.JPE
+G,.JBIG2,.JB2,.eps]
+(grfext)             \AppendGraphicsExtensions on input line 456.
+)
+LaTeX Font Info:    Try loading font information for U+msa on input line 19.
+
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsfonts\umsa.fd"
+File: umsa.fd 2013/01/14 v3.01 AMS symbols A
+)
+LaTeX Font Info:    Try loading font information for U+msb on input line 19.
+("C:\Users\Simon\AppData\Local\Programs\MiKTeX 2.9\tex\latex\amsfonts\umsb.fd"
+File: umsb.fd 2013/01/14 v3.01 AMS symbols B
+)
+Underfull \hbox (badness 10000) in paragraph at lines 15--21
+
+ []
+
+(abstract.tex) (tutorial_description.tex [1{C:/Users/Simon/AppData/Local/MiKTeX
+/2.9/pdftex/config/pdftex.map}
+
+
+]) (main.bbl)
+
+** Conference Paper **
+Before submitting the final camera ready copy, remember to:
+
+ 1. Manually equalize the lengths of two columns on the last page
+ of your paper;
+
+ 2. Ensure that any PostScript and/or PDF output post-processing
+ uses only Type 1 fonts and that every step in the generation
+ process uses the appropriate paper size.
+
+Package atveryend Info: Empty hook `BeforeClearDocument' on input line 62.
+[2]
+Package atveryend Info: Empty hook `AfterLastShipout' on input line 62.
+ (main.aux)
+Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 62.
+Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 62.
+Package rerunfilecheck Info: File `main.out' has not changed.
+(rerunfilecheck)             Checksum: 67A912E424B98C3B68909037B2041A13;48.
+Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 62.
+ ) 
+Here is how much of TeX's memory you used:
+ 6781 strings out of 493303
+ 104240 string characters out of 3129784
+ 192693 words of memory out of 3000000
+ 10243 multiletter control sequences out of 15000+200000
+ 40509 words of font info for 85 fonts, out of 3000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 28i,8n,26p,502b,405s stack positions out of 5000i,500n,10000p,200000b,50000s
+{C:/Users/Simon/AppData/Local/Programs/MiKTeX 2.9/fonts/enc/dvips/base/8r.enc
+}<C:/Users/Simon/AppData/Local/Programs/MiKTeX 2.9/fonts/type1/public/amsfonts/
+cm/cmsy7.pfb><C:/Users/Simon/AppData/Local/Programs/MiKTeX 2.9/fonts/type1/urw/
+times/utmb8a.pfb><C:/Users/Simon/AppData/Local/Programs/MiKTeX 2.9/fonts/type1/
+urw/times/utmr8a.pfb><C:/Users/Simon/AppData/Local/Programs/MiKTeX 2.9/fonts/ty
+pe1/urw/times/utmri8a.pfb>
+Output written on main.pdf (2 pages, 63611 bytes).
+PDF statistics:
+ 78 PDF objects out of 1000 (max. 8388607)
+ 25 named destinations out of 1000 (max. 500000)
+ 9 words of extra memory for PDF output out of 10000 (max. 10000000)
+

+ 1 - 0
main.out

@@ -0,0 +1 @@
+\BOOKMARK [1][-]{section*.11}{References}{}% 1

BIN
main.pdf


BIN
main.synctex.gz


+ 62 - 0
main.tex

@@ -0,0 +1,62 @@
+\documentclass[conference]{IEEEtran}
+\usepackage{url}
+\usepackage{hyperref}
+\usepackage{amssymb,amsfonts,amsmath}
+\usepackage{xspace}
+\usepackage{graphicx}
+
+\begin{document}
+\title{Statecharts Modelling and Simulation}
+\author{\IEEEauthorblockN{Simon Van Mierlo} \and \IEEEauthorblockN{Hans Vangheluwe}}
+
+\maketitle
+
+\section*{Presenters}
+\textbf{\uppercase{Simon Van Mierlo}} is a post-doctoral researcher at the University of Antwerp (Belgium).
+He is a member of the Modelling, Simulation and Design (MSDL) research lab.
+For his PhD thesis, he developed debugging techniques for modelling and simulation formalisms by explicitly modelling their executor's control flow using Statecharts.
+He is the main developer and maintainer of SCCD, a hybrid formalism that combined Statecharts with class diagrams.
+His e-mail address is \url{Simon.VanMierlo@uantwerpen.be}.
+\\
+
+\textbf{\uppercase{Hans Vangheluwe}} is a Professor at the University of Antwerp (Belgium), an Adjunct Professor at McGill University (Canada) and an Adjunct Professor at the National University of Defense Technology (NUDT) in Changsha, China.
+He heads the Modelling, Simulation and Design (MSDL) research lab.
+In a variety of projects, often with industrial partners, he develops and applies the model-based theory and techniques of Multi-Paradigm Modelling (MPM).
+His current interests are in domain-specific modelling and simulation, including the development of graphical user interfaces for multiple platforms.
+To model such reactive systems, he advocates the use of Statecharts to describe their behaviour.
+His e-mail address is \url{Hans.Vangheluwe@uantwerpen.be}.
+
+\section*{Abstract}
+\input{abstract.tex}
+
+\section*{Keywords}
+Statecharts, reactive systems, testing, Yakindu
+
+\section*{Length}
+The proposed length of the tutorial is three hours.
+
+\section*{Level of the Tutorial}
+Introductory. No knowledge of Statecharts or the tool (Yakindu) is necessary.
+
+\section*{Target Audience}
+Modellers with an interest in specifying the behaviour of reactive systems using Statecharts.
+
+\section*{Novelty}
+This tutorial has previously been given (in 2017) at the Spring Simulation Multi-Conference (SpringSim)\footnote{\url{http://scs.org/springsim}}.
+Due to the success of this tutorial, a second edition of the tutorial is scheduled for the 2018 edition of this conference.
+Since this conference is mainly targeted at an audience with a simulation background, the tutorial focuses on the introduction of modelling for specifying reactive systems, and covers the basics of Statecharts.
+For the audience at the MoDELS conference, we will discuss Statecharts more extensively and in-depth, focusing on the applicability to more complex systems than the running example.
+
+\section*{Description of the Tutorial and Intended Outline}
+\input{tutorial_description.tex}
+
+\section*{Required Infrastructure}
+A data projector is required.
+
+\section*{Sample Slides}
+A number sample slides of the previous versions of the tutorial are attached.
+
+\bibliographystyle{IEEEtran}
+\bibliography{bibliography}
+
+\end{document}

+ 2 - 0
make_total.sh

@@ -0,0 +1,2 @@
+#!/bin/bash
+gs -dBATCH -dNOPAUSE -q -sDEVICE=pdfwrite -sOutputFile=submission.pdf main.pdf sample_slides/slides.pdf

BIN
submission.pdf


+ 33 - 0
tutorial_description.tex

@@ -0,0 +1,33 @@
+%!TEX root = main.tex
+\begin{itemize}
+  \item Discovery of the complexity in engineerd 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, since 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).
+      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 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.
+  \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}