Language Design for Reactive Systems: On Modal Models, Time, and Object Orientation in Lingua Franca and SCCharts

Language Design for Reactive Systems On Modal Models, Time, and Object Orientation in Lingua Franca and SCCharts M. Sc. Alexander Schulz-Rosengarten geb. in Kiel Dissertation zur Erlangung des akademischen Grades Doktor der Ingenieurwissenschaften (Dr.-Ing.) der Technischen Fakultät der Christian-Albrechts-Universität zu Kiel eingereicht im Jahr 2023 Kiel Computer Science Series (KCSS) 2024/1 dated 2024-01-24 ISSN 2193-6781 (print version) ISSN 2194-6639 (electronic version) Electronic version, updates, errata available via https://www.informatik.uni-kiel.de/kcss Published by the Department of Computer Science, Kiel University Real-Time and Embedded Systems Group Please cite as: Ź Alexander Schulz-Rosengarten. Language Design for Reactive Systems — On Modal Models, Time, and Object Orientation in Lingua Franca and SCCharts Number 2024/1 in Kiel Computer Science Series. Department of Computer Science, 2024. Dissertation, Faculty of Engineering, Kiel University. @book{SchulzRosengarten24, author = {Alexander Schulz-Rosengarten}, title = {Language Design for Reactive Systems --- On Modal Models, Time, and Object Orientation in Lingua Franca and SCCharts}, publisher = {Department of Computer Science}, year = {2024}, number = {2024/1}, doi = {10.21941/kcss/2024/1}, series = {Kiel Computer Science Series}, note = {Dissertation, Faculty of Engineering, Kiel University.} } © 2024 by Alexander Schulz-Rosengarten ii About this Series The Kiel Computer Science Series (KCSS) covers dissertations, habilitation theses, lecture notes, textbooks, surveys, collections, handbooks, etc. written at the Department of Computer Science at Kiel University. It was initiated in 2011 to support authors in the dissemination of their work in electronic and printed form, without restricting their rights to their work. The series provides a unified appearance and aims at high-quality typography. The KCSS is an open access series; all series titles are electronically available free of charge at the department’s website. In addition, authors are encouraged to make printed copies available at a reasonable price, typically with a print-on-demand service. Please visit http://www.informatik.uni-kiel.de/kcss for more information, for instructions how to publish in the KCSS, and for access to all existing publications. iii 1. Gutachter: Prof. Dr. Reinhard von Hanxleden Christian-Albrechts-Universität zu Kiel Kiel, Deutschland 2. Gutachter: Prof. Dr. Edward A. Lee University of California, Berkeley Berkeley, USA 3. Gutachter: Prof. Dr. Michael Mendler Otto-Friedrich-Universität Bamberg Bamberg, Deutschland Datum der mündlichen Prüfung: 24.11.2023 iv Zusammenfassung Reaktive Systeme spielen eine wichtige Rolle im Bereich der eingebetteten Systeme. Sie interagieren kontinuierlich mit ihrer Umgebung, verarbeiten nebenläufige Vorgänge und sollten im Allgemeinen deterministisches Verhalten aufweisen, um auch sicherheitskritische Anwendungen zu ermöglichen. In solch einem Kontext ist das Sprachdesign ein wichtiger Aspekt, denn sorgfältig gestaltete Sprachkonstrukte können dabei helfen komplexe Herausforderungen dieser Domäne anzugehen. Dies zeigen beispielsweise die verschieden Nebenläufigkeitsmodelle, die es erlauben den klassischen Fallstricken bei der Nutzung von Threads zu entgehen. Heutzutage gibt es viele verschiedene Sprachen in diesem Kontext. Häufig zeichnen sie sich dadurch aus, dass sie einzigartige Charakteristika aufweisen, die sie für spezifische Anwendungsfälle besonders geeignet machen. Diese Arbeit beschäftigt sich mit zwei solcher Sprachen, der Aktor-orientierten polyglotten Koordinationssprache Lingua Franca und dem synchronen Statecharts-Dialekt SCCharts. Während die beiden Sprachen verschiedene Ansätze verfolgen, um eine reaktive Modellierung zu ermöglichen, weisen doch beide Gemeinsamkeiten in ihrer Semantik auf und ergänzen sich in ihren Designprinzipien. Diese Arbeit betrachtet Schlüsselaspekte des Sprachdesigns für reaktive Systeme im Kontext dieser beiden Sprachen. Für drei relevante Konzepte werden dabei schlanke und minimalinvasive Spracherweiterungen entworfen und evaluiert. Besonderes Augenmerk liegt darauf diese neuen Konzepte an die fundamentalen Prinzipien der zugrundeliegenden Sprachen anzupassen. Konkret wird Lingua Franca um die Möglichkeit erweitert modusabhängiges Verhalten zu modellieren, während SCCharts eine Timed Automata Notation mit dynamischen Ticks zur effizienten Ausführung erhält und um Konstrukte zur objektorientierten Modellierung erweitert wird. v Abstract Reactive systems play a crucial role in the embedded domain. They continuously interact with their environment, handle concurrent operations, and are commonly expected to provide deterministic behavior to enable application in safety-critical systems. In this context, language design is a key aspect, since carefully tailored language constructs can aid in addressing the challenges faced in this domain, as illustrated by the various concurrency models that prevent the known pitfalls of regular threads. Today, many languages exist in this domain and often provide unique characteristics that make them specifically fit for certain use cases. This thesis evolves around two distinctive languages: the actor-oriented polyglot coordination language Lingua Franca and the synchronous statechart dialect SCCharts. While they take different approaches in providing reactive modeling capabilities, they share clear similarities in their semantics and complement each other in design principles. This thesis analyzes and compares key design aspects in the context of these two languages. For three particularly relevant concepts, it provides and evaluates lean and seamless language extensions that are carefully aligned with the fundamental principles of the underlying language. Specifically, Lingua Franca is extended toward coordinating modal behavior, while SCCharts receives a timed automaton notation with an efficient execution model using dynamic ticks and an extension toward the object-oriented modeling paradigm. vii Contents 1 Introduction 1 1.1 The Furuta Pendulum Example . . . . . . . . . . . . . . . . . . 3 1.1.1 LinguaFranca........................ 4 1.1.2 SCCharts........................... 5 1.2 Design Opportunities and Considerations . . . . . . . . . . . . 8 1.3 Contributions and Publications . . . . . . . . . . . . . . . . . . 9 1.3.1 Related Publications and Advised Theses . . . . . . . . 12 1.4 Outline................................ 13 2 Design Principles of Lingua Franca and SCCharts 15 2.1 Synchronous Languages . . . . . . . . . . . . . . . . . . . . . . 17 2.1.1 Different Language Variants . . . . . . . . . . . . . . . 18 2.2 LinguaFranca............................ 19 2.2.1 Runtime Environment . . . . . . . . . . . . . . . . . . . 24 2.2.2 Target Language Integration . . . . . . . . . . . . . . . 25 2.3 SCCharts............................... 25 2.3.1 Dataflow SCCharts . . . . . . . . . . . . . . . . . . . . . 32 2.3.2 Runtime Environment . . . . . . . . . . . . . . . . . . . 34 2.3.3 Target Language Integration . . . . . . . . . . . . . . . 36 2.4 The Furuta Pendulum Example in Detail . . . . . . . . . . . . 38 2.4.1 MainProgram........................ 38 2.4.2 Pendulum Sound . . . . . . . . . . . . . . . . . . . . . . 40 2.4.3 Pendulum Controller . . . . . . . . . . . . . . . . . . . . 43 2.5 Modeling Pragmatics . . . . . . . . . . . . . . . . . . . . . . . . 46 ix 1. Introduction the arm. To achieve this, a controller usually has three phases; (1) it rotates the shaft to impart enough energy to the pendulum that it swings up, (2) it imposes a countermovement to catch the pendulum, and (3) it stabilizes the pendulum above the arm using minimal adjustments. Each of these steps requires a different control behavior, referred to as SwingUp,Catch, and Stabilize mode. To illustrate additional timing aspects, the scenario is extended by an LED light and a speaker. The LED displays the phase in which the controller operates. Off during swinging up, blinking with a 30 msec period while catching, and constantly on when stabilizing. The speaker indicates how close the pendulum is to its upright position. From the lowest to the highest position it should play an ascending chromatic scale, specifically C2 – B2 (approx. 65–123 Hz), by producing a square wave signal. 1.1.1 Lingua Franca Lingua Franca is an actor-oriented polyglot coordination language [LMB+21] based on the deterministic reactor model [LÍG+19]. Reactors are inherently reactive, timed, concurrent, event-based, and represent encapsulated objects. LF focuses on efficient implementations and features a wide-ranging applicability, from the embedded to the distributed domain. Figure 1.2 presents the LF program that controls the Furuta pendulum in an abstracted hardware environment. The program consists of reactors, represented by the rounded boxes with input and output ports. Reactors are concurrent and communicate via connections between their ports. In LF, computations are embedded in reactions, written in a target language, in this case C. In the graphical notation, reactions are represented by gray wedges, but the actual code is omitted to reflect only the coordination level. The PendulumSound reactor handles the angle-dependent sound. Its reaction is triggered by an input at the angle port or the occurrence of an action (white triangle). Actions enable the scheduling of future events internal to the reactor. This action in particular is an effect of the reaction itself and is used to schedule the next occurrence of a duty cycle switch. The reaction calculates the current note based on the angle value and schedules actions to control the frequency of the square signal. 4 1.1. The Furuta Pendulum Example FurutaPendulum Angles theta d_theta phi d_phi PendulumSound L angle sound PendulumController (0, 15 msec) 1 2 theta d_theta phi d_phi led control Speaker wave_signal LED on Motor control Figure 1.2. The pendulum control program in LF. The PendulumController uses a timer (clock figure), with an initial offset of 0 and a period of 15 msec, to trigger reaction 1. This reaction sets the led output in an alternating pattern if operating in Catch mode. Reaction 2 computes the control response for the motor based on the angles at the two hinges and their velocity. The number in the reaction labels indicates the ordering, which is used to ensure output determinism. Here, reaction 2 is able to override the value on the led output produced by the first reaction to enforce a constant LED state for modes other than Catch. The remaining reactors handle the interaction with the hardware. Their contents are hidden as it is of no further relevance to this example. Section 2.4 will present the given model in more detail, including the textual source code with the reaction bodies. 1.1.2 SCCharts SCCharts are a synchronous statecharts dialect with a Sequentially Constructive (SC) semantics [HDM+14]. They augment Harel’s classical statecharts [Har87] with various synchronous language constructs, while SC Model of Computation (MoC) combines sequential memory access with deterministic concurrency enabling a more intuitive imperative programming style than in classical synchronous languages, such as Esterel or Lustre. 5 1. Introduction FurutaPendulum float theta, d_theta, phi, d_phi, control bool msec = false, led = false, sound = true +Angles +Time PendulumSound const int SEC_TO_MSEC = 1000 int msecs = 0 float duration = 0 immediate during / duration = 1 / sound_frequency(theta) / 2 * SEC_TO_MSEC Alternate during msec / msecs++ msecs >= duration / sound = !sound; msecs = 0 - -Sound +Motor +LED +Speaker PendulumController float catch_phi = 0 SwingUp immediate during / control = swingup_control(theta , d_theta) Catch during / control = catch_control(theta , d_theta , phi , d_phi) Toggle 15 msec / led = !led -LED Stabilize during / control = stabilize_control(theta , d_theta , phi , d_phi , catch_phi) exit_swingup(theta) / led = true exit_catch(d_phi) / catch_phi = phi; led = true exit_stabilize(theta) / led = false - -Controller Figure 1.3. The pendulum control program in SCCharts. SCCharts support multiple code generation strategies tailored to different use cases and target languages combined in a powerful and transparent model-based compiler [Smy21]. Figure 1.3 illustrates the SCChart that models the same behavior for the pendulum as in LF. The SCChart has seven concurrent regions (white inner boxes). These regions communicate via shared variables, declared at the top of the root state. The additional msec variable indicates the passage of one millisecond. It is not present in LF because it can rely on a builtin time model. In this example, msec is computed in the Time region by 6 1.1. The Furuta Pendulum Example communicating with the hardware. 1 This and the other regions for hardware access are again hidden (collapsed). The PendulumSound state uses the milliseconds to control the frequency of the square signal. This state is the initial state of the enclosing region, indicated by the thicker border. It has a constant, two local variables, a during action, and an inner region. During actions executed the given effect as long as their state is active. If marked immediate, they already execute at the tick their state is entered; otherwise, they would only start at the subsequent tick. In this case, the external function sound_frequency is invoked to compute the frequency based on the current angle of the arm. The basic computations for the sound and motor control are factored out into external C functions to reduce the model size and reuse the same logic in SCCharts and LF. The frequency is converted into a half cycle duration in milliseconds and stored in duration. The inner region has a single state Alternate that increments the msecs counter every time a millisecond passed by using a during action. The self transition is activated if the msecs counter reaches the duration threshold and then toggles the sound signal and resets the counter. The transition weakly preempts the state, hence, the counting happens before the trigger test. Since the during action is not immediate, the millisecond cannot be counted twice. In the PendulumController state, three inner states represent the different control modes. Each state uses different external functions to compute the control response and whether to exit this state. The LED is set as an effect of the transitions, and in the Catch state an additional region handles the toggling every 15 milliseconds. The 15 msec notation is a count delay; syntactic sugar for a similar counting infrastructure as in PendulumSound, but only for constant values. The red dot at the transition to SwingUp indicates adeferred entry into this state, suppressing the immediate execution of the during action. Hence, the control logic in each state will only activate in the tick after entering its state.2 1 For an SCChart in general, it would be more common to have the hardware communication and time as dedicated inputs and outputs, see Section 2.3.2. However, the presented design focuses on highlighting the equivalence to the LF program. 2 Again, there are alternative designs, but this one was chosen for equivalence with LF , especially in regard to modes presented in Chapter 3. This does not impair the modeling quality of the solution. 7 1. Introduction 1.2 Design Opportunities and Considerations Without further details on the implementation or semantics of LF and SCCharts, a comparison between the two pendulum models already reveals valuable insights on the different design principles and enables identifying opportunities for the improvement of both languages and for such language design in general. Most apparent are the two notations that are used; the dataflow approach in LF, and SCCharts with its statecharts notation, as well as the different degrees of detail in the graphical notation. As discussed before, there is no clear preference for one or the other, and the granularity of the view is mostly a question of tool configuration. Yet, from a modeling perspective, LF cannot directly express the modal behavior of the pendulum controller, or the fact that the timer is only relevant to the Catch mode. Both aspects are explicit in the SCChart. Another important aspect is the handling of time. In LF, time is a firstclass citizen. This enables the use of a timer in the Controller reactor and the scheduling of actions in Sound with dynamic delays. On the other hand, the SCChart requires time as an explicit input; in this case single discrete milliseconds read from the hardware. This is a classical approach in synchronous languages that follows a multiform notion of time [Ber99]. In the face of the dynamic and real-valued nature of the angle-dependent delay and a per-tick time input, the counting of milliseconds is only a compromise between precision and workload. The counting requires a periodic execution of the SCChart at least every millisecond. In contrast to that, LF features a more resource-friendly sparse execution that facilitates a nanosecond precision (if supported by the hardware). There are also notable differences in the way both languages express concurrency, provide internal communication channels, and integrate their target languages to provide basic instructions. These and other design aspects are discussed in more detail in Chapter 2. However, a more subtle aspect that is in the focus of this thesis is the fact that LF supports an Object-Oriented (OO) design. To a certain degree, this comes naturally to an actor-based language [Cap03; LLN09], but there is also great potential for a statecharts language in adopting OO concepts to improve its capabilities 8 1.3. Contributions and Publications in abstraction, genericity, reusability, and modularity. This is particularly relevant in the face of increasingly complex software systems, also in the safety-critical and embedded domain [Dvo09]. A straightforward solution to all these issues could be an attempt to create a new language that is a union of both. However, this is not the goal of this thesis. Both language have their fundamental design principles and semantics that makes them valuable and successful in their area. Instead, the goal is to address and investigate the discussed issues by creating simple and minimally invasive extensions that stay true to the core principles of the language. This especially includes a seamless integration into the textual and graphical syntax, a lean implementation, and conservative and robust semantics. The previous comparison might give the impression that both languages are played against each other. However, the opposite is the case since they act as mutual motivation and inspiration due to the collaboration of both projects. Chronologically, some concepts were initially developed in parallel (cf. Section 1.3). Recent developments on efficient sparse execution [EH20; SIL+17] or time and object-like structures in imperative synchronous languages [SIL+17; GG18], also show the high relevance of the discussed topics to this domain. Yet, the consideration of modern MDE, deterministic concurrency, embedded targets, and high-level coordination, in combination with synchronous statecharts, or respectively reactor-oriented programming, represents a relevant contribution to the language design of reactive systems. 1.3 Contributions and Publications This thesis is the first work analyzing the design of LF and SCCharts in direct comparison (Chapter 2). The main contributions, however, concern the improvement of both languages and are divided into three topics. Modal models in LF, Time in SCCharts, and Object Orientation (OO) for SCCharts. In each contribution the respective language is used as an environment to carefully design an integration of this aspect that extends the modeling capabilities for reactive systems. 9 1. Introduction Modal Models Chapter 3 investigates the design of a modal coordination layer in a reactororiented environment. This chapter draws from and extends publications on modal reactors [SHL+23b; SHL+23c; SHL+23a]. Specifically, Chapter 3 presents • a minimally invasive language extension of LF to express modal structures that embraces the reactor-oriented nature and black-box approach towards reaction code; • an adaptation of a lean set of hierarchical composition capabilities and common transition types, reset and history, implementing modal behavior with reactors; and • a semantics for modal behavior that introduces mode-local time and leverages the superdense time model to achieve deterministic behavior. The adaption of the LF tooling to the modeling pragmatics of the KIELER project (see Section 2.5) is also part of my work, including the synthesis of LF diagrams. Yet, this is only covered implicitly and is not part of a dedicated publication or chapter in this thesis. Time Chapter 4 evolves around research questions on real-time modeling in a synchronous context with a focus on a flexible notation of time, efficient executions strategies, and practical arrangements for timer imperfections when dealing with physical time. The presented topics draw from and expand on publications titled “Time in SCCharts” [SHM+18; SHM+20]. The chapter covers • a lean timed automaton notation for SCCharts that models time with real-valued clocks and can be expressed in a synchronous setting and only minimal requirements on the execution environment or the languages itself; • a new language feature for periodically timed regions that enables modeling multiclocked systems; 10 1.3. Contributions and Publications • a detailed investigation of the suitability of different execution strategies in a timed setting; and • a sparse execution environment that implements dynamic ticks in a synchronous real-time setting and requires only a minimal runtime infrastructure. Object Orientation Chapter 5 investigates the integration of the OO programming and design methodology into a pragmatics-aware synchronous statecharts modeling language. My work on OO is published with the title “Toward Objectoriented Modeling in SCCharts” [SSM19; SSM21]. This chapter draws from these results and extends them, consisting of • a conservative extension of SCCharts that permits OO modeling under the principles of synchronous languages, providing modeling class-based data structures, capabilities for programming using methods, inheritance to improve reusability, and a proposal for type parameterization and subtyping to further facilitate abstraction; • an integration of the new OO design features into the modeling and compilation tooling of KIELER; and • mechanisms to ensure the determinism of host language objects under the shared memory concurrency of synchronous languages while retaining their encapsulation under a contract-based black-box scheduling approach. All three concepts have been implemented and tested and are publicly available in the respective open-source projects of LF3and SCCharts4. 3https://github.com/lf-lang/lingua-franca 4https://github.com/kieler/semantics 11 1. Introduction 1.3.1 Related Publications and Advised Theses There are various co-authored publications and student theses advised by me that relate to the topics discussed in this thesis and inspire and support some contributions. Ź On the topic of modal models and hybrid modeling, there is work under the lead of Nis Wechselberg on “Augmenting State Models with Data Flow” [WSS+18]; a Master’s thesis [Gri19] and subsequent publication [GSS+20; GSS+22] by Lena Grimm on the adaption of Lustre/SCADE dataflow into SCCharts (using the dataflow extension developed by Steven Smyth [Smy21]); and a Master’s thesis [Luc20] and publication [LSH+21] by Daniel Lucas on “Extracting Mode Diagrams from Blech Code”. Ź For time in SCCharts, Andreas Boysen developed in his Master’s thesis “An FPGA-based Demonstrator for Dynamic Ticks” that was also published [BSH20b; BSH20a; BSH20c], see also Section 4.5.2. The collaboration with the LF team also led to my participation in a publication on time in LF [LMS+20; LBM+23]. Ź In relation to OO stands the Bachelor’s thesis of Gavin Lüdemann on “Modular Code Generation for SCCharts” [Lüd21] and a supportive role in the introduction of scheduling directives [SSH19; SSH18b] (see Section 5.4.2 and Section 4.2.2) under the lead of Steven Smyth (covered in [Smy21]). Ź On MDE and modeling pragmatics, there are the Master’s theses by Philip Eumann on “Model-Based Debugging” [Eum20], by Andreas Stange titled “Model Checking for SCCharts” [Sta19], and by Sören Domrös on moving MDE tooling into web technologies [Dom18]. Likewise, a supportive role in “Guidance in Model-based Compilations” [SSH18a] led by Steven Smyth (covered in [Smy21]) relates to this topic. Finally, I participated in the creation of “Pragmatics Twelve Years Later: A Report on Lingua Franca” [HLF+22]. 12 1.4. Outline 1.4 Outline After this introduction follows Chapter 2 providing a direct comparison of LF and SCCharts, including a brief introduction of their notations and conceptional foundations. At the heart of this thesis are two parts. Part I focuses on LF and the integration of modal models in Chapter 3, and Part II bundles the two contributions based on SCCharts. Chapter 4 presents the contribution on time and dynamic ticks, and Chapter 5 covers OO. Each of the three main chapters briefly covers related work in the given context and presents and evaluates its contribution. Finally, Chapter 6 concludes these topics and gives an outlook on future work. 13 2. Design Principles of Lingua Franca and SCCharts of reactor-oriented programming is inspired by many well-established principles, such as OO [Str87], actor-oriented design [Hew77], or event-driven programming [DZK+02]. This short overview can only provide a limited introduction into LF. A more comprehensive description is available in the respective publications [LÍG+19; Loh20; LMB+21] and the official documentation3. Composition LF programs consist of reactors. The entry point is a single main reactor. Each reactor can instantiate other reactors and create connections between input and output ports to establish communication channels. In addition to ports and reactor instances, reactors can contain reactions, state variables, timers, and actions, as Figure 1.2 already illustrated. Object Orientation Reactors can be considered instantiable classes in an OO sense. They also offer inheritance to facilitate reusable designs. A reactor can extend another one, where all declaration of reactions, ports, timer, etc. in the super class are placed syntactically before locally defined ones. The natural ordering of LF reactions then automatically results in an overriding behavior. This form of inheritance is a bit more restrictive than in classical mainstream OO languages. Like objects, reactors encapsulate state and behavior in the form of state variables and reactions in combination with timers and actions. All contents of a reactor, except ports, have a local scope; they are only visible inside the reactor or its subclasses. While objects classically interact via method calls, reactors receive events from ports, timers, and actions and handle them in reactions. Unlike methods, reactions are not invoked directly, but are executed once if triggered by the presence of an event. There is no recursion or multiple invocation per tick. In addition to reactions, LF also has classical methods. However, these cannot react to input events but instead are invoked from within reactions. Causality Each reaction has a signature in the following form: reaction(<trigger*>)<source*> -> <effect*> {= <body> =} 3https://www.lf-lang.org/docs/ 20 2.2. Lingua Franca It defines optional lists of triggers (ports, actions, or timers that can trigger it), sources (ports that the reaction can read from when triggered), and effects (ports it may set or actions it may schedule). Scoping rules for the reaction body, enforced by the compiler, ensure that the data dependencies expressed in this signature are conservative. Hence, reaction signatures represent a causality interface for reactions [ZL08]. Reaction signatures and connections between ports or instantiated reactor can be turned into a dependency graph. If acyclic, it yields a partial order for all reactions that expresses all scheduling constraints that will result in a deterministic execution for each tick. This corresponds to the write-before-read protocol in synchronous languages. A causality problem is present if the graph is cyclic, e. g., a reaction’s trigger or source depends on its own immediate effect. Figure 2.6b will illustrate an example of a model with a causality error. The fact that the dependencies graph is valid independent of the actual code in the body enables to treat reactions as black-boxes. This property is the key factor in the polyglot nature of LF. State variables are implicitly accessible in all reactions, and multiple reactions may set the same output port. Therefore, reactions within the same reactor always have a fixed scheduling order assigned to them, which is derived from their textual position in the code. The dependency graph also reflects these constraints to ensure determinism. In this regard, LF features sequentiality similar to the SC MoC. Synchronicity The runtime mechanism of LF is event-driven, as only events trigger reactions. The event processing in reactors is synchronous and similar to synchronous languages. Events are tagged with their time of occurrence on a logical timeline. Execution progresses in ticks where all events of the current time are processed at once and time does not progress during execution. Consequently, outputs carry the same logical time tag as their inputs and may instantly trigger downstream reactions. The previously mentioned causality analysis ensures that no reaction executes before all the data sources that it depends on are known. While ticks can act as a barrier synchronization for concurrent reactors, primarily in a non-distributed 21 2. Design Principles of Lingua Franca and SCCharts context, LF also facilitates scheduling regimes that enable reactions to span multiple ticks, as in logical execution time [KS12; HHK03]. Events can be checked for their presence at the current time and carry a value. In this respect they correspond to valued signals in synchronous languages. Time While ports are terminals for the flow of events between reactors, actions and timers enable the creation of timed events inside reactors. Timers produce events with a predefined period and offset, whereas actions provide an interface to manually schedule future events as an effect of reactions. Considering the previously discussed causality, a reaction that dependents on itself via an action, as in PendulumSound in Figure 1.2, could be considered a problematic cycle. Yet, this is not the case due to a mandatory delay upon scheduling. While the delay clearly must not be negative, it may be zero. Tags in LF are pairs (t , m) , where t is a time value and m a microstep index. Mircosteps separate subsequent ticks at the same logical time t . This implements the concept of superdense time [MP93]. Connections pass events instantaneously (within the same tick/microstep), but they can also be configured to impose a delay. Again, this can be zero, introducing a microstep delay when passing events between reactors. Another important aspect of time in LF is the relation to physical time (wall clock time). This is also reflected in the difference between physical and logical actions. Logical actions create events from within the execution of reaction, hence, in sync with logical time, while physical actions can be scheduled from an asynchronous context, e.g., a spawned thread or interrupt service routine. Events from physical actions receive a tag based on current physical time. The execution engine ensures that logical time will not run ahead of physical time, such that there is no risk of out-of-order events. In practice, logical time will lag behind physical time, because it will not progress during execution. LF provides deadlines to detect and handle timing violations [LMS+20; LBM+23]. Concurrency Reactions are atomic execution units that are subject to a dependency graph. This transparently enables the parallelization of logically simultaneous reactions that are independent of each other, without risking 22 2.2. Lingua Franca data races or deadlocks. LF’s runtime implementation features different options for singleor multithreaded execution.4 Furthermore, LF programs can also be federated. If the main reactor is marked federated, this turns its inner reactors instances into federates that can be distributed onto different machines. Connections will be automatically set up as network channels. The semantics of reactors, especially the notion of logical time, will ensure determinism even in this distributed setting. Yet, the nature of this environment results in multiple timelines and a tradeoff between consistency and availability [LBL+23; LBL+21; LMS+20; LBM+23]. LF offers the choice between a centralized coordination that handles global synchronization of logical time or a decentralized control that relies on the local physical clocks and techniques from Programming Temporally Integrated Distributed Embedded Systems (PTIDES) [ZLL07]. The second mechanism requires explicit bounds on network latencies and clock synchronization errors, which may be violated in a practical deployment. However, LF can detect these situations and enables reactions to such faults, similar to deadlines. The decentralized distributed aspect shows that LF is not a classical synchronous language, in the sense that it is not driven by a single global clock, but rather corresponds to multiclocked variants, such as Signal [GG10] or multiclocked Esterel [BS01]. It also relates to the idea of a Globally Asynchronous Locally Synchronous System (GALS) [Cha84]. Mutations While static instantiation is the normal and most common way of composing reactors, the concept of reactors also supports dynamic runtime creation and destruction using mutations [LÍG+19]. This includes changing connections between reactors or reactions. By requiring the same static signatures for mutations, it is possible to decide at compile time on the soundness of runtime modifications to the reactor topology. In LF, mutations are currently only implemented for the Typescript target as an experimental feature. 4 Currently, only the C, C++, and Rust targets provide support for multithreaded execution. 23 2. Design Principles of Lingua Franca and SCCharts Environment Sensors Lingua Franca Runtime Reactor Network Read Control Future EventsCurrent Events Physical Actions Tick Actuators Event Loop Figure 2.2. LF -specific reactive program components and their interaction with each other and the environment. 2.2.1 Runtime Environment LF programs compile into standalone executables. In case of a federated program, multiple executables are generated that can be automatically deployed onto the different machines. An LF program consist of programspecific code, generated from the reactor network and its reactions, plus a generic runtime engine handling the event loop, scheduling of reactions, and progression of time. This event-driven approach and the fact that main reactors (as well as federated ones) cannot have input or outputs ports, defines the way LF programs interact with their environment. Figure 2.2 presents a concretized version of the reactive system schematics in Figure 2.1. It shows the LF-specific components and their interaction with each other and the environment. The arrangement represents the LF perspective on a reactive system. Hence, the Sensors and Actuators are positioned mostly in the environment, as they represent hardware components and are only accessed via their respective application programming interface (API). The Sensors provide input data asynchronously by scheduling events via physical actions or read directly from within reactions. The latter can be used to implement a polling mechanism by triggering a reading reaction by a periodic timer. The LF Runtime manages events and time. Dashed lines in the schematic represent triggering/execution of components, while solid lines indicate passing data. The LF Runtime runs an internal Event 24 2.3. SCCharts Loop that advances time until processable events are present. If present, it will start the execution—a Tick of the Reactor Network—passing the events with that tag. The execution of the reactions will control the Actuators and produce new internal events that need to be processed in the future. 2.2.2 Target Language Integration LF aims for a polyglot language design by embedding code of any target language directly into its coordination language. Key enabler for this approach is the black-box treatment of reactions. Target code blocks ({= ...=}), such as reaction bodies, are neither parsed nor otherwise analyzed. Only the reaction signatures are used as conservative dependency interfaces, while it remains unknown to the LF compiler if certain data source are actually accessed or effects are produced. The code generated for reactions contains a verbatim copy of the reaction body. Additionally, the LF compiler generates an individualized preface that makes only the triggers, sources, and effects of the reaction and state variables of the reactor available to its body. Section 2.4 will illustrate some functions that LF makes available to the embedded code. This API is target language specific. Furthermore, the LF compiler must support code generation for the desired target languages and requires a compatible implementation of the LF runtime engine. With these prerequisites the LF compiler can synthesize the main reactor into code and create an executable using a target language compiler. LF currently supports C, C++, Python, Typescript, and Rust as targets. LF’s coordination layer establishes separation between reactors, which in turn facilitates a polyglot design where different reactors are written in different target languages. While the LF compiler does not yet support such programs, at least federated LF models will soon provide the option to have polyglot federates. 2.3 SCCharts SCCharts are a synchronous language that follows that statecharts notation developed by Harel [Har87]. They are inspired by SyncCharts [And03] 25 2. Design Principles of Lingua Franca and SCCharts ABO input output bool A, B output bool O1, O2 WaitAB WaitA DoneA A / B = true; O1 = true -HandleA WaitB DoneB B / O1 = true -HandleB GotABInit / O1 = false; O2 = true / O1 = false; O2 = false - Figure 2.3. The ABO SCChart [HDM+14], consisting only of Core SCCharts elements. and draw concepts from various other synchronous languages, providing a powerful and versatile set of modeling elements. SCCharts are built around the SC MoC but also follow a more classical synchronous approach compared to LF. This short overview can only provide a limited introduction into SCCharts. A more comprehensive description is available in the respective publications [HDM+14; Mot17; Smy21; HDM+13] and the official documentation5. Core SCCharts Similar to Esterel, SCCharts are defined by a kernel language, called Core SCCharts, that facilitates the definition of semantics and code generation. This minimal syntactic core is relatively close to the basic building blocks of statecharts. All other modeling elements in SCCharts, called extended features, are reducible to this core language. Figure 2.3 shows the ABO SCChart that only consists of Core SCCharts elements. Its main purpose is to demonstrate core characteristics of the SCCharts semantics, e.g., shared variables with multiple different values during a tick. The program will produce O1 and O2 depending on the inputs Aand B. Both Aand Bwill set O1 to true but with different timing. 5https://github.com/kieler/semantics/wiki 26 2.3. SCCharts Additionally, Awill imply a true value on Bonce, overriding the value set by the environment. After both Aand Bare correctly consumed by HandleA and HandleB,O1 is reset to false and O2 is set to true. A complete presentation of the behavior of the model can be found in its original publication [HDM+14]. This model illustrates that Core SCCharts consist of states, variables, regions, and transitions that can carry an optional trigger and effects, separated by a slash. The top level state of an SCChart is called root state, in this example named ABO. It declares the input output interface of the program. Here, the interface consists of A,B,O1, and O2.Aand Bare both inputs and outputs, which means they are consumed from the environment but can be altered and provided as product of the program. Composition Regions are used to compose SCCharts hierarchically and additionally express concurrency if there are multiple regions in the same state. If a state with one or more inner regions, called superstate, is entered, all regions immediately start executing. Each region must have an initial state, drawn with thicker border (e.g., Init), and can have one or more final states, drawn with a double border (e.g., GotAB). When a region reaches a final state, it terminates. 6 Only when all inner regions have terminated, it can be left via a termination transition (indicated by a green triangle), as in the case of WaitAB. Reactivity & Synchronicity While LF follows an event-driven dataflow approach with connected reactors and reactions as event handlers, SCCharts with its statecharts notation expresses behavior in a control-flow manner. Yet, both languages react in synchrony and in discrete ticks, following the synchronous idea. Where LF processes events by running reactions, SCCharts transitions from one state to another. With concurrent regions there can be multiple active states. Each active state checks its available outgoing transitions (ordered by priority) whether its trigger expression holds, takes the first match, executes its effect sequence, and passes activity on to the target state. This continues until no further transition is enabled, which marks the end of the tick. Hence, ticks act as a barrier synchronization 6 Transitions leaving final states and final states with inner behavior are considered an extended feature and are not part of Core SCCharts. 27 2. Design Principles of Lingua Franca and SCCharts for concurrent regions. In contrast to reactions, SCCharts can reenter the same state and thus run the same behavior multiple times, w.r.t. limitations by the SC MoC and code generation approach. Time SCCharts do not have a built-in notation for expressing time or tagged events as LF has. It follows the idea that time is “just” another input to the system that comes in synchrony with other input values. This results in a multiform notion of time as in Esterel, where for example one signal indicates the passage of a second, while another represent a minute [Ber99]. The pendulum example in Section 1.1.2 illustrates this approach. However, as already mentioned, this approach has limitations. Chapter 4 will present a more advanced way of handling time, which is closer to LF and synchronous languages such as Céu. Yet, transitions have an important timing property concerning the discrete synchronous ticks. They can be either delayed or immediate. Delayed transitions require that at least one tick has passed after their source state was entered before they can be taken, while immediate ones are always available. Hence, a delayed transition contains a pause in the imperative sense of synchronous languages. In the graphical syntax, delayed transitions are solid lines, while immediate ones are dashed. For ABO this means that the SCChart cannot reach the state GotAB during the first reaction (assuming the appropriate inputs) because region HandleB has a delayed transition and always consumes at least one tick before state WaitB can be left. Sequential Constructiveness The semantics of SCCharts adhere to the Sequentially Constructive (SC)MoC [HDM+14] that establishes causality and determinism. A key factor is sequentiality, especially compared to classical synchronous languages, such as Esterel. In these languages, signals are the first-class citizens and their rather strict write-before-read protocol is enforced globally. This rules out sequential check-and-override patterns common to imperative programming, e.g., if (x < 42) x++, even in the absence of concurrency because it conflicts with the assumption of a globally consistent state. Destructive updates can be encoded in thread-local variables in Esterel, but cannot be shared concurrently. Even the ABO example in Figure 2.3 would be rejected in Esterel because it may write different 28 2.3. SCCharts values to O1 in the same tick. The SC MoC relaxes this limitation and unifies signals, channels, and local variables into a single notion, the SC-variable. SC-variables can have different values during a tick and are guided by a dependency graph that considers natural sequentiality in the code and only applies a synchronization protocol to concurrent contexts. This is similar to LF where connections between reactors are subject to a write-before-read protocol, but reactions in a reactor are ordered sequentially. The latter is imposed by the fact that the state variables are shared between the reactions of a reactor, and they may perform destructive updates on these variables, as well as on output ports. In SCCharts the communication solely relies on SC-variables, and they are shared between all concurrent regions of their declaring state and into deeper levels of hierarchy. In a concurrent context, SC-variables are synchronized under the InitializeUpdate-Read Protocol (IURP). The IURP allows variables to be initialized by an absolute write first and then permits multiple relative updates that are required to be commuting 7 (i.e., in case of multiple writers, a combination function must deterministically unify the value) before the value can be read. In ABO, the transition to WaitAB occurs before any behavior inside that state and, hence, is ordered sequentially. The IURP only applies to variables shared in the scope of the two regions inside WaitAB. This ensures that writing to Bin HandleA will happen before reading it in HandleB. The two concurrent initializations of O1 are sound since they are commuting and any ordering will yield the same result. The IURP applies per SC-variable, instant, and concurrent context. Hence, the end of tick or leaving a superstate resets the IURP for this variable. Another important difference to LF is that SCCharts feature their own expression language for triggers and effects. They are analyzed in a whitebox approach to extract variables accesses and in turn infer dependencies. In contrast to that, LF uses the reaction signatures and connections for explicit dependencies. For integrating host code, SCCharts rely on a similar principle as LF, see Section 2.3.3, and with more modular SCCharts or 7 In [HDM+14] this is called “confluent”, but “commuting” seems more precise in this context. The execution of all writers is “confluent” because they are pairwise “commuting.” 29 2. Design Principles of Lingua Franca and SCCharts 1#include "PendulumSound.h" 2#include "HardwareMockup.h" 3int main(int argc, const char*argv[]) { 4TickData model; 5reset(&model); 6while (1) { 7model.angle = read_from("theta"); 8model.msec = msec_passed(); 9tick(&model); 10 write_to("speaker", model.sound); 11 } 12 } (a) Main function invoking the tick function and handling inputs and outputs. 1typedef struct { 2double angle; 3char msec; 4char sound; 5... 6} TickData; 7 8void reset(TickData*d); 9void tick(TickData*d); (b) PendulumSound.h generated by the SCCharts compiler. Listing 2.1. Abstract implementation of a tick function loop for the PendulumSound SCChart in C. input is likewise determined by a utility function. Then, the tick function is called, and finally the output is written to the hardware. This setup illustrates that the tick function approach is more lightweight in terms of code generation but requires an additional environment implementation, compared to a standalone approach in LF. Yet, the SCCharts is also able to generate such a tick function wrapper and then compile and deploy an executable, if the context is known, e.g., for simulation or based on templates [Smy21]. It would also be possible to embed a tick function in LF and use it as an environment. In such a setup the LF runtime engine would act as the Trigger Unit. Section 3.4.4 will discuss such a design. 2.3.3 Target Language Integration SCCharts feature a design primarily independent of any target language, by providing a small generic expression language for specifying conditions and computations directly in SCCharts. If relying on this core language, a model can be specified without a pre-defined target. Furthermore, all SCCharts structures and the expression language itself can easily be translated into different target languages [HDM+14]. For example in the netlist compilation 36 2.3. SCCharts approach, the final sequentialized code only relies on conditional statements and assignments, which is available in nearly every programming language and easy to synthesize. SCCharts currently support C, Java, and VHDL. The inputs and outputs produce a simple communication interface to the environment, which could also be used for coordinating external behavior. Additionally, SCCharts support direct interaction with their host language, e.g., the sound_frequency function in Figure 1.3. Section 2.4 will present the involved extern declarations. The term “host language” is synonymous to target language but was coined by the fact that the tick function design implies a host system embedding the synchronous program. 9 External host functions in SCCharts are inspired by Esterel’s host language integration [PEB07; Ber99]. They are treated as black-boxes, same as reaction code in LF. In order to correctly include them in the causality analysis and to provide deterministic handling, an interface for potential data accesses is required. SCCharts infer this from the use of passed arguments. Call-by-value parameters are considered read accesses and call-by-reference non-confluent writers. In most cases and under the assumption that the function does not have side effects, this is sufficient to establish a causal relation to the surrounding synchronous program. Section 5.4 further discusses this aspect and introduces a concept for deterministically interacting with objects and their methods. An extern declaration introduces an external function, provided by a verbatim string, to the SCCharts expression language under an alias. This enables a degree of multilanguage support. For example the line extern @C "rand",@Java "Math.random" random declares a random function that works in C and Java using annotations to synthesize the correct host code depending on the compilation target. Additional annotations in the SCCharts source file would handle the correct host-specific import of the required libraries. Like LF and Esterel, SCCharts can use the host’s type system to define variables. For example host "uint64_t" mask 9 Even if synonymous, in this thesis the term “target language” or “target code” will be used primarily in the context of LF ’s polyglot reaction approach, while “host language” or “host code” will describe the way synchronous languages and SCCharts handle the interfacing with external languages. 37 2. Design Principles of Lingua Franca and SCCharts will create a 64 bit unsigned integer variable by using the type from the C library stdint. SCCharts also has a verbatim code expressions. Any string in the form ` ... ` will be directly passed on to the generated code, similar to {= ...=} in LF. This host language integration enables SCCharts to function as a deterministic coordination layer around an existing software systems without requiring communication via an input output interface. However, a polyglot programming concept that effectively mixes multiple host languages in the same SCChart, similar to the vision in LF, is not supported nor planned. 2.4 The Furuta Pendulum Example in Detail Section 1.1.2 presented the basic setup and objectives in the augmented Furuta pendulum scenario, as well as a first look at the two models in LF and SCCharts. In this section the implementation and the practical application of design elements in LF and SCCharts are in focus. This involves the modular composition starting with the main program and the two primary components PendulumSound and PendulumController. Again, the inner workings of modules for platform-specific hardware communication are excluded. Furthermore, the code factors out some of the control logic into an external file, used in both the SCCharts and LF model. The motor control behavior for the pendulum arm replicates a solution by Eker et al. [LEJ+02]. All source files are available online.10 2.4.1 Main Program The FurutaPendulum diagrams in Figure 1.2 and Figure 1.3 show the fully instantiated main reactor, respectively the expanded root state, of the main program. In the actual source, the program composes the two separate components for sound and motor control with the hardware handlers and sets up communication channels. 10https://github.com/a-sr/furuta-pendulum 38 2.4. The Furuta Pendulum Example in Detail 1target C { 2cmake-include: ["behavior.cmake"] 3} 4preamble {= 5#include "behavior.h" 6=} 7import PendulumController from "PendulumController.lf"; 8import PendulumSound from "PendulumSound.lf"; 9import Angles, Motor, LED, Speaker from "PendulumHardware.lf"; 10 11 main reactor { 12 controller = new PendulumController(); 13 sound = new PendulumSound(); 14 angles = new Angles(); 15 led = new LED(); 16 speaker = new Speaker(); 17 motor = new Motor(); 18 19 angles.theta -> controller.theta; 20 angles.d_theta -> controller.d_theta; 21 angles.phi -> controller.phi; 22 angles.d_phi -> controller.d_phi; 23 controller.control -> motor.control; 24 controller.led -> led.on; 25 angles.theta -> sound.angle; 26 sound.sound -> speaker.wave_signal; 27 } Listing 2.2. Source code of the FurutaPendulum main program in LF. Lingua Franca Listing 2.2 shows the textual source of the main reactor. The first line specifies the target language that the reactors will use, in this case C. It also includes a file that will help the build system find the source files that provide the low-level behavior implementation. The subsequent preamble includes the corresponding header. The next lines import the relevant reactors from accompanied files. The main reactor then instantiates these reactors and sets up connections between their input and output ports. SCChart Listing 2.3 shows the textual source of the main SCChart. Similar to the LF program, the first lines make the external files known to the build system, include the header file in the generated code, and import the SCCharts modules. The following implementation of the SCChart starts with the declaration of shared variables for the communication between the modules. Afterwards, seven regions are defined. Each region has a single initial state that references one of the modules. The parameters in these module macros represent the binding of the local variables to the inputs and outputs of the respective module. Hence, they correspond (in their use) to the connections between the LF reactors. 39 2. Design Principles of Lingua Franca and SCCharts 1#resource "behavior.h","behavior.c" 2#hostcode-c"#include \"behavior.h\"" 3import "PendulumController.sctx" 4import "PendulumSound.sctx" 5import "PendulumHardware.sctx" 6 7scchart FurutaPendulum { 8float theta, d_theta, phi, d_phi, control 9bool msec, led, sound 10 11 region Sound { 12 initial state PendulumSound is PendulumSound(theta, msec, sound) 13 } 14 region Controller { 15 initial state PendulumController is PendulumController(theta, d_theta, phi, d_phi, msec, control, led) 16 } 17 region Time { 18 initial state Time is Time(msec) 19 } 20 region Angles { 21 initial state Angles is Angles(theta, d_theta, phi, d_phi) 22 } 23 region Speaker { 24 initial state Speaker is Speaker(sound) 25 } 26 region LED { 27 initial state LED is LED(led) 28 } 29 region Motor { 30 initial state Motor is Motor(control) 31 } 32 } Listing 2.3. Source code of the FurutaPendulum main program in SCCharts. 2.4.2 Pendulum Sound The PendulumSound module produces a square wave signal for the speaker. Both implementations use the external sound_frequency function to compute the correct frequency for the note to play based on an angle value. Lingua Franca The reactor in Listing 2.4 first declares its input port for the angle and output port for the speaker signal. It has three state variables: wave_state,cycle_duration, and last_switch. The first indicates whether the signal is currently in its duty cycle or not. The next represents the current length of a half cycle. The last one is the time of the last signal edge. Additionally, the reactor has a logical action that carries a time value as payload. The behavior is defined in a single reaction that is triggered by input events on the angle port or the alternate action (both triggers can also be present simultaneously). The effects list the output port and the action. 40 2.4. The Furuta Pendulum Example in Detail 1target C; 2reactor PendulumSound { 3input angle: double; 4output sound: bool; 5state wave_state: bool = false; 6state cycle_duration: time = 0; 7state last_switch: time = 0; 8logical action alternate: time; 9reaction(angle, alternate) -> sound, alternate {= 10 if (alternate->is_present && alternate->value == self->cycle_duration) { 11 self->wave_state = !self->wave_state; 12 lf_set(sound, self->wave_state); 13 lf_schedule_copy(alternate, self->cycle_duration, &self->cycle_duration, 1); 14 self->last_switch = lf_time_logical(); 15 } 16 if (angle->is_present) { 17 interval_t new_duration = SEC((1 / sound_frequency(angle->value)) / 2); 18 if (new_duration != self->cycle_duration) { 19 interval_t remaining_time = MAX(new_duration -(lf_time_logical() -self->last_switch), 0); 20 lf_schedule_copy(alternate, remaining_time, &new_duration, 1); 21 self->cycle_duration = new_duration; 22 } 23 } 24 =} 25 } Listing 2.4. Source code of the PendulumSound component in LF. The basic idea is to determine the targeted frequency based on the angle input and then schedule the action at the time of the next planned signal edge. The reaction code is separated into two if statements. In the fist one (lines 10 to 15), the periodic square signal is produced by emitting alternating outputs based on the occurrence of the action. In the second (lines 16 to 23), the cycle duration is adjusted based on the angle-induced frequency. To illustrate how these parts work together, we start with a first angle event at tag ( 0,0 ) . The reaction will be triggered and the first if block is skipped because only angle is present. In the second block, the new duration for a cycle is computed using the sound_frequency function. The SEC function handles the conversion into LF’s time representation. If the new duration differs from the current one, the timing behavior must be adjusted, which is always the case at program start. The remaining time to the next signal switch is computed in line 19. It takes into account the last switch and 41 2. Design Principles of Lingua Franca and SCCharts 1scchart PendulumSound { 2input float angle 3input bool msec 4output bool sound = true 5 6const int SEC_TO_MSEC = 1000 7extern "sound_frequency" sound_frequency 8int msecs = 0 9float duration = 0 10 immediate during do duration = 11 ((1 / sound_frequency(angle)) / 2) *SEC_TO_MSEC 12 13 region { 14 initial state Alternate { 15 during if msec do msecs++ 16 } 17 if msecs >= duration do sound = !sound; msecs = 0 18 go to Alternate 19 } 20 } Listing 2.5. Source code of the PendulumSound component in SCCharts. prevents negative values by a maximum function. This time is then used as a delay for scheduling the action. Finally, it saves the new cycle duration. At time 0, the logic will always determine an immediate signal switch and hence schedule the action with a delay of 0. However, actions impose a microstep delay in this case. Hence, the reaction will not be executed again at tag ( 0,0 ) but at ( 0,1 ) . In this turn, only the first part will be active, since angle is absent. This block first toggles the state, sets the output to this new value, schedules the action again with the current cycle duration to ensure a periodic signal, and saves the current logical time in last_switch. In the further execution, the duration will change as the angle changes, which will result in additional actions scheduled for a time before or after the action that was scheduled based on the old frequency in line 13. This is where the payload becomes relevant. It associates each action with the duration it represents. The if statement in line 10 checks this value and ignores actions that do not represent the currently targeted sound frequency. This design is a consequence of the current limitation in LF that prohibits removing or adjusting scheduled events. 11 The fact that this implementation introduces a microstep delay for producing a cycle switch “immediately” is mainly for demonstration purposes, as the output could also be set directly before line 20 and then only the next switch would be scheduled. 11 A limitation that LF may lift in the future by returning a handle upon schedule that enables the user to unschedule an action. 42 2.4. The Furuta Pendulum Example in Detail SCChart Listing 2.5 shows the code of the PendulumSound SCChart, initially illustrated in the Sound region of Figure 1.3. Comparing the code with the diagram, one can notice that there is very little difference in the amount of information. This is a clear contrast to LF, which hides the entire implementation in reactions and only illustrates the coordination layer in the diagram. While this is subject to the configuration of details in the diagram, it presents different views on the model that are provided by default. While LF focuses on the coordination aspect, SCCharts’ focus is more on behavior modeling, which includes details on concrete conditions and effects of individual transitions. Section 2.5 will discuss the concept of views in more detail. The SCChart code in Listing 2.5 first declares its module-specific inputs, angle and msec, and the sound output variable. In line 6 it declares a constant for converting seconds into millisecond as it cannot resort to a built-in time model, as in LF. Afterwards, the external hostcode function sound_frequency is defined and two local variables are declared. Since SCCharts are not explicitly event-driven as LF, the during action updates the cycle duration in each tick based on the angle. The Alternate state in the region advances the msecs counter every time a milliseconds passes. The self transition toggles the sound signal output and resets the counter. Hence, the signal edge in the square wave signal is modeled as a dynamic threshold between the targeted half cycle length and the passed time, see line 17. However, in order to work with the msec input, the SCChart needs to be executed each millisecond, i.e., every time any operand changes. A sparse execution, more similar to LF, requires a more sophisticated infrastructure, as proposed in Chapter 4. 2.4.3 Pendulum Controller The PendulumController module controls the motor to balance the pendulum and sets the LED state to indicate its mode of operation. Again, both implementations use external functions for the control logic in each mode and to check for mode switches. 43 2. Design Principles of Lingua Franca and SCCharts 1target C; 2reactor PendulumController { 3input theta: double; 4input d_theta: double; 5input phi: double; 6input d_phi: double; 7output control: double; 8output led: bool; 9 10 preamble {= typedef enum {SwingUp, Catch, Stabilize} ControlModes; =} 11 state control_mode: ControlModes = {=SwingUp=}; 12 state led_state: bool = false; 13 state catch_phi: double = 0.0; 14 timer toggle_led(0, 15 msec); 15 16 reaction(toggle_led) -> led {= 17 if (self->control_mode == Catch) { 18 self->led_state = !self->led_state; 19 lf_set(led, self->led_state); 20 } 21 =} 22 reaction(theta, d_theta, phi, d_phi) -> control, led {= 23 switch (self->control_mode) { 24 case SwingUp: 25 lf_set(control, swingup_control(theta->value, d_theta->value)); 26 if (exit_swingup(theta->value)) { 27 self->control_mode = Catch; 28 self->led_state = true; 29 lf_set(led, self->led_state); 30 } 31 break; 32 case Catch: 33 lf_set(control, catch_control( theta->value, d_theta->value, phi->value, d_phi->value)); 34 if (exit_catch(d_phi->value)) { 35 self->catch_phi = phi->value; 36 self->control_mode = Stabilize; 37 self->led_state = true; 38 lf_set(led, self->led_state); 39 } 40 break; 41 case Stabilize: 42 lf_set(control, stabilize_control( theta->value, d_theta->value, phi->value, d_phi->value, self->catch_phi)); 43 if (exit_stabilize(theta->value)) { 44 self->control_mode = SwingUp; 45 self->led_state = false; 46 lf_set(led, self->led_state); 47 } 48 break; 49 } 50 =} 51 } Listing 2.6. Source code of the PendulumController component in LF. Lingua Franca The reactor code in Listing 2.6 12 is similarly structured as the SoundController. The PendulumController first declares its input and output ports and then local state variables. The type for the control_mode is defined as an enum in C by using a preamable that will be added to the generated code for this reactor. The control_mode is initialized to the SwingUp mode and the led_state starts in its Off state. The value catch_phi must be passed 12 This code is based on an implementation by Edward A. Lee that adapts the original Ptolemy II model by Eker et al. [LEJ+02] to C and LF . My variant extends this solution by additionally controlling the LED. 44 2.4. The Furuta Pendulum Example in Detail between the Catch and Stabilize phase. Additionally, the reactor defines a timer with an initial offset of 0 and a period of 15 msecs. The first reaction is triggered by this timer. It toggles the led_state and sets the output with this value but only when operating in Catch mode. The second reaction processes all angle related inputs. The implementation assumes that all four events will always be present simultaneously and omits individual checks for presence. The different modes of operation are implemented in a switch statement. In each case, the control output is set with the result of the respective control logic function, which receives the relevant angle data. Afterwards, an if statement checks whether this mode should be left. If that is the case, the new mode is set, the led_state is updated accordingly, and the led output is set. Setting the LED in the second reaction, ordered after the one for toggling, is important to override the effect of the previous reaction if they happen to be triggered simultaneously. However, while the design with two reactions is quite reasonable, it results in a timing subtlety. Even if the first reaction toggles the LED only in the Catch mode, the timer is not aligned with actual mode change. Hence, the start of the Catch mode may not be the start of the periodic blinking. This issue will be discussed in more detail in Chapter 3. SCChart As it was the case for the PendulumSound, the source code in Listing 2.7 only reveals minor additional details on the behavior of the PendulumController compared to Figure 1.3. Again, this SCChart declares the inputs and outputs relevant to this module and defines the external functions. Compared to the LF implementation, the state machine notation enables SCCharts to express the modes more naturally and explicitly. This supersedes the need for the corresponding state variables and the synchronization of the alternating LED to the Catch mode. The SCChart models the same behavior as its LF counterpart, which includes the way modes are changed. Specifically, at any time, the control output is defined by the current mode, and if it decided to exit this mode and switch to the next, the next one will only determine the value in the subsequent instant. This is modeled by the fact that the during actions for the control output are not immediate and the transitions only perform 45 Chapter 3 Modal Models The direct comparison of the pendulum implementation in LF with its SCCharts counterpart (in Section 1.2 and Section 2.4) reveals two major opportunities for improvement in LF; 1. extending modeling capabilities to express modal behavior 1 , such as SwingUp,Catch, and Stabilize; and 2. binding of timed elements, such as the timer in PendulumController, to specific modes of operation. Modeling (1.) Complex software systems often feature distinct modes of operation that provide a particular behavior for a specific context. The Furuta pendulum example represents this characteristic well, even if it is relatively small. Yet, the implementation of modes in a state machine using a switch pattern is relatively extensive, as Listing 2.6 illustrates. More importantly, such handwritten code contradicts the fundamental idea of model-driven engineering and, moreover, is easily prone to errors, complex to extend, and hinders formal verification. Furthermore, the entire modal structure is “hidden” in a single reaction, see Figure 1.3. From a modeling perspective, the explicit use of separate states for the modes in the SCChart variant provides in comparison an additional value by enabling meaningful diagrams. While there are techniques 1 The term mode describes the concept of combining program behavior into modes of operation. While the most natural notation for modes is a state machine, modes can subsume multiple states of a system into a single mode [MR98]. Hence, modes and states can be used synonymously, if states do not refer to a single memory state but a more abstract modal state of the program, as it is usually the case in statecharts and SCCharts. 53 3. Modal Models false true SwingUp Catch Stabilize LED Logical Time (msec) 1040 1055 1070 1085 1100 1115 1130 non-aligned aligned Figure 3.1. An excerpt of the led output by the PendulumController reactor in a simulation. It illustrates a timing behavior of a non-aligned and an aligned timer in relation to the catch mode. to extract such mode diagrams from handwritten code, as Section 3.1.2 will present, this contradicts the black-box approach that governs LF’s reactions. Hence, there is merit to expressing modal structures directly on the coordination layer of LF. It breaks down the behavior into smaller units that promote code readability and can be supported by more meaningful diagrams. Furthermore, it enables robust code generation for controlling these modal units and exposes mutually executive behavior that can be used to enhance modeling capabilities or facilitate verification. Timing (2.) Figure 3.1 shows an excerpt of the LED output by the PendulumController reactor in a simulation. The simulation emulates the pendulum behavior with a sample period of 5 msec. The presented interval reflects the time in which the controller switches from mode SwingUp to Catch and later to Stabilize, as indicated at the top of the plot. The solid non-aligned line represents the output of the PendulumController reactor presented in Listing 2.6. According to its implementation, the LED is set directly by the second reaction when the mode changes, at time 1055 and 1115 msec. During Catch mode the signal is toggled by the first reaction when the timer expires. Since the timer runs all the time, it happens to trigger the reaction at 1065 msec in this simulation. This reduces the on cycle to only 10 msec. The dashed aligned line is the output of the corresponding SCChart that models the alternating LED outputs inside the Catch and thus aligns their activity. 54 Of course, this behavior has no critical consequences in this particular scenario. Even if the start of the cycle would be aligned, the last cycle could be cut off depending on the start of the Stabilize mode. 2 Alternatively, a logical action could be used to create a periodic triggering that starts with the Catch mode, similar to the one in the PendulumSound reactor. Yet, a timer is more simple and robust than manually scheduled actions, but it cannot be controlled correctly if modes are only expressed on the target code level and not in the model. This example shows that timing is an important issue when working with modes and that modal models are able to express time-related associations more naturally if their semantics are carefully designed. Goals The main goal is to bring the advantages of modal models to LF and the reactor-oriented programming paradigm, and indirectly also closer to mainstream programming languages, which can be embedded into LF. From FSMs to statecharts up to SCCharts, there are many concepts and languages that are already able to express modal models. While the idea of modes is not new, a seamless integration into LF that is guided by its fundamental principles is. The goal is to create modal models that offer the following characteristics. Lean design Modes should constitute a minimal coordination layer that provides the most essential functionality but still offers maximal versatility and user adjustability. Polyglotism The modal notation should act as flexible multilanguage wrapper that focuses on the user’s language and requires only minor adaptation effort. Time sensitivity The model should offer a reliable and precise way to specify time sensitive modal behavior, even in parallel and distributed environments. Concurrency The design should enable the composition of multiple separate modal units acting independently. 2It is only a coincidence that the Catch phase in this simulation is exactly 60 msec long. 55 3. Modal Models Determinism A model must yield unambiguous and reproducible output behavior for the same sequence of input events. The concept of modal reactors presented in this chapter embodies these very principles and embraces the crucial black-box approach of reactions. Outline This chapter starts with a brief presentation of related work, covering different languages and approaches to express modal behavior. Next, Section 3.2 illustrates the basic principles of modal reactors by presenting a variant of the PendulumController reactor that uses modes. Subsequently, Section 3.3 describes the detailed concept and implementation of modal reactors in LF. Finally, Section 3.4 discusses the proposed design and briefly illustrates potential alternatives. 3.1 Related Work The idea of expressing modal behavior is not new and there are many languages and concepts that enable the use of mode automata or state machines in this regard. While the design of modal reactors builds on existing concepts, there is no previous work that truly matches the unique principles of LF, especially in terms of polyglot design. Statecharts A natural notation for modal behavior can be found in the many variants of FSMs. Beyond that, there are statecharts that offer more feature-rich language constructs. With their hierarchical composition, they facilitate the encapsulation of individual behavior and fine-grained states into broader modes of operation. Synchronous dialects, such as SyncCharts, adapt statecharts into a semantic domain that is relatively close to LF. However, in contrast to plain statecharts or FSMs, modes for LF require a more hybrid approach, to accommodate for the dataflow nature of reactors. SCCharts SCCharts surpass most other statecharts languages in terms of features variety and versatility. This also includes modal modeling capabilities. Yet, the focus of the modal model concept in this thesis is on LF, 56 3.1. Related Work since it provides a unique opportunity to design modes in an actor-oriented, polyglot, coordination context. While SCCharts also provide a dataflow notation (Section 2.3.1), their own form of multilanguage support (Section 2.3.3), and can be used to deterministically orchestrate processes, these aspects are more pronounced in LF. 3.1.1 Mode Extensions Since LF is a reactor-oriented language, work that extends dataflow notations with state machines is particularly relevant. Yet, a commonality in all existing work is that they feature an additional extensive notation for states, transitions, triggers, and effects, representing an obstacle for a lean and polyglot integration in the context of LF. SCADE The work that is perhaps the closest in spirit to modal reactors is the extension of Lustre and SCADE with state machines. Maraninchi and Rémond propose a concept of mode-automata [MR98] that combines statecharts-like automata with a minimal Lustre language. Colaço et al. pick up this approach and adapt a more lean variant into Lustre and SCADE [CPP05; CHP06]. At its core, SCADE is a synchronous dataflow modeling language, where concurrent nodes communicate via clocked streams, see also Section 2.1.1. With the extension for modes, nodes received a state machine notation that features reset and history transitions, as well as preemption. Most importantly, states encapsulate equations, which enables a hybrid design that mixes modes and dataflow. The implementation uses a clock-directed approach based on a sourceto-source transformation. It extends the original clocks of Lustre/SCADE into a richer type system that encodes and controls modes. In order to simplify analysis, states and their equations are in mutual exclusion. Therefore, preemption is restricted, such that a state can only be entered weakly (non-deferred) if the previous is strongly preempted upon leaving or vice versa. 57 3. Modal Models The SCADE approach represents a very similar design to the one later found in modal reactors. However, it is based on the classical synchronous principles, which LF exceeds in terms of distributed execution and notion of time. In this regard, LF embodies a more event-driven concept than a clock-driven one. Ptolemy The Ptolemy II tool provides an environment for heterogeneous modeling [EJL+03]. It is based on an actor-oriented design that supports nesting and interconnecting components. A unique characteristic is that each level of the hierarchy can have a separate MoC directing its semantics. Ptolemy II provides various MoCs, such as continuous time (CT) or synchronous dataflow (SDF), as well as a state machine layer that enables modal models [LT10; Pto14]. A key to combining arbitrary MoCs in a modal model is a notion of mode-local time to preserve a sound compositional semantics. As mentioned in Section 2.4, some parts of the low-level implementation of the Furuta pendulum are based on a previous implementation in Ptolemy [LEJ+02]. Figure 3.2 presents an excerpt of this model. It illustrates the different layers of the model governed by different MoCs. A modal model inside the controller manages the different computations of the control output (uin this variant).3 In many ways, LF continues the research of the Ptolemy project. Yet, the focus shifted from an experimentation platform for different MoCs to a more application-oriented polyglot coordinating language. Simulink MathWorks’ Simulink tool is an environment for modeling and simulating control logic with block diagrams. With Stateflow [HR04] it provides a statecharts-like notation able to express modes by nesting blocks in different states. In contrast to the discretized time in LF and synchronous languages, Simulink primarily uses a continuous-time concept with semantics that depend on the configuration of the simulation [CCM+03]. 3 Most of the pendulum controllers in this thesis factor out the control logic into external functions, see Section 2.4. The example of dataflow SCCharts in Figure 2.4 illustrates a variant that includes the modeling of these computations and, hence, corresponds more to the approach in the Ptolemy model. 58 3.1. Related Work Figure 3.2. A Furuta pendulum implementation in Ptolemy by Liu et al. [LEJ+02]. (©2002 International Federation of Automatic Control. Reproduced with the permission of IFAC from J. Liu, J. Eker, J. W. Janneck, E. A. Lee, “Realistic Simulations of Embedded Control Systems”. IFAC Proceedings Volumes, 35/1, pp. 391-396) LabVIEW National Instruments’ LabVIEW is a graphical dataflow language for implementing control systems [Kod20]. It enables modeling modal behavior by using a pattern with a switch structure in a while loop. A dedicated state diagram view supports the user in this design. While LabVIEW does provide a notion of modes, the pattern-based state notation and strong reliance on a graphical syntax only loosely relates to the modal extension pursued in this thesis. 59 3. Modal Models ROOM The Real-time Object-Oriented Modeling (ROOM) language by Selic et al. [SGW94] uses an actor notation for the high-level specification of distributed real-time systems. The behavior of these actors is modelled in a statecharts dialect, called ROOMcharts [Sel93]. In terms of characteristic statecharts features, Selic et al. exclude concurrent composition with the arguments that this aspect is better expressed on the actor level. Hierarchical nesting is kept but is restricted only to the ROOMcharts elements. Hence, while ROOM actors can be composed hierarchically, ROOMcharts are specified independently and do not enclose inner actors into modal units. Instead, it represents an additional specification for message processing. Furthermore, communication in ROOM is governed by synchronous (blocking) and asynchronous (non-blocking) message delivery rather than a global model of timestamped events as in reactors. Akka The Java-based actor programming framework Akka [RWB16] provides means to implement concurrent actors that interchange and process event messages. LF uses Akka as a guideline for its performance benchmarks [Loh20; MLB+23]. Akka also supports implementing stateful behavior in actors by extending an FSM actor class [RWB16]. It enables defining states, their event processing, transitions, and internal timers. However, Akka does not ensure deterministic behavior. Furthermore, the FSM notation does not support hierarchy, resulting in limited hybrid modeling capabilities. 3.1.2 Mode Extraction Instead of extending a language towards modes, there is also work that extracts the implicit states from the code into a modal view. However, this approach confines the modal modeling capabilities to the target language and does not account for a modal coordination layer. C/C++ Said et al. [SQK18] propose a technique that explores the state space of a program by mining for state variables and simplifies these into a state machine. The approach of Somé and Lethbridge [SL02] detects special patterns, such as switch statements (as in Listing 2.6), and visualizes 60 3.1. Related Work them. The same technique is used by Andersen to convert C/C++ code into SCCharts [And19]. Blech Synchronous languages facilitate detecting states, as they explicitly contain pauses. The translation from imperative Esterel code to SyncCharts [PTH06] illustrates such a procedure but with strong focus of semantic equivalence. The more recent work for the similarly structured Blech language [GG18] applies an approach that emphasizes abstraction and reveals a mode-oriented view on the underlying behavior of the program [LSH+21]. SCCharts An inverse procedure of mode extraction is illustrated by SCCharts’ induced dataflow [WSS+18]. It extracts the implicit dataflow relations between concurrent regions, as illustrated in Figure 2.6a. 3.1.3 Modal Augmentation As an alternative to a separate coordination language with modes, there are various proposals that aim at directly augmenting mainstream programming languages with a notion of states or modes. Statecharts in C/C++ Wagner et al. describe a design process for flat FSMs directly in C [WSW+06]. An advanced approach by Samek describes the implementation of UML statecharts in C/C++ [Sam08]. While this includes concurrency, there are no provisions for a deterministic behavior. FairThreads FairThreads [Bou06] are an extension of C that enables cooperative threading. They are implemented based on macros and use native threads. FairThreads also include macros to model automata for auxiliary tasks, as their restricted structure facilitates a more efficient execution w.r.t. threads. SyncCharts in C There are also some synchronous extensions to C, with SyncCharts in C [Han09] as probably the most relevant for modes. Again, this concepts relies on C macros to provide a light-weight low-level language extension. It enables expressing states and provides deterministic concurrency based on a priority-based dispatching of threads. 61 3. Modal Models and all reactions associated with their target modes. As a consequence, any cyclic modes structure would impose a causality loop and would have to be rejected. Alternatively, transitions could wait until all contents of a mode finish executing but then immediately switch to the next mode and execute that one, still at the same tag. However, this would raise the question of how to handle the reactivation of the same mode multiple times at the same tag. Moreover, this would permit an arbitrary number of mode changes during the same execution instant. In the end, some notion of a sequential separation between mode activations would be necessary. Furthermore, the reactor MoC is simply not intended to execute reaction multiple times at the same tag. The evident solution is to implement delayed transitions that introduce at least a microstep delay. Hence, in modal reactors, reactions can set a new mode, but this has no immediate effect. Only when the reactor has finished executing all its contents, the transition will take effect and the new mode becomes active in the next microstep. Hence, no two modes in the same reactor can be active at the same tag. Neither can a transition interfere with ongoing reactions. The same principle for mutual exclusion of modes can be found in SCADE [CPP05; CHP06]. Yet, this approach requires resolving potentially “conflicting” transition effects from different reactions. To resolves such situations, the same mechanism applies as in setting ports. The fixed ordering of reactions determines the effective target mode that will be used. In terms of deterministic outcome and overriding behavior, setting new modes can be considered analogous to assigning output ports. However, in terms of timing, transition effects correspond to scheduling actions with a zero delay, which also enforces a microstep delay to prevent causality cycles. To be precise, if at a tag (t , m) , a new mode was set by a reaction in a modal reactor, the execution of that tick will finish unchanged. Only at the end of that instant, the target mode will be determined by the last reaction that set a mode, the current mode will be deactivated, and the new one will be activated for future execution. This means no reaction of the newly active mode will execute at tag (t , m) . Instead, the earliest possible reaction in the new mode occurs one microstep later, at (t , m+ 1 ) . If the newly active mode has for example a timer that will elapse with an offset of zero, it will trigger at (t,m+1). In case the mode itself does not require an immediate 68 3.3. Modal Reactors execution in the next microstep, the next executed tag depends on future events (t+e ,0 ) , with e as the time offset to the next event, just as in the normal behavior of LF. Thus, modes in the same reactor are always mutually exclusive w.r.t. superdense time. Reset Transitions A mode can be reset upon entry, returning it to its initial state. Specifically, this has the following effects: •all contained modal reactors are reset to their initial mode (recursively); •all contained timers are reset and start again awaiting their initial offset; • all events (actions, timers, delayed connections) that were previously scheduled from within this mode are discarded; • all contained state variables that are marked for automatic reset are reset to their initial value; and •all contained reactions with the new reset trigger are executed. Note that “contained” refers to all contents defined locally in the mode and in local reactor instances (recursively) that are not otherwise enclosed in modes of lower levels. These effects ensure that whenever a mode is entered with a reset transition, the subsequent timing of behavior is as if the mode was never executed before. Furthermore, state variables are not reset automatically by default. Instead, they need to be marked for reset explicitly because it is idiomatic for reactors to store manually managed resources, such as allocated memory, in state variables. Hence, an automatic reset could easily lead to memory leaks or runtime exceptions. Section 3.3.3 will provide a more detailed example of manual resource management. To provide manual control over resetting state variables, a new built-in reset trigger for reactions is provided that enables reacting to a reset entry of a mode. The reset modifier on state variables is a convenience feature that automatically resets state variables to their initial value, e.g., used for led_state in line 22 of Listing 3.1. History Transitions In contrast to a reset transition, a history transition will “simply” skip resetting a mode’s contents. This enables the mode to continue its behavior from the point it was last left, or its initial configuration 69 3. Modal Models if it was not active yet. In regard to the temporal behavior, the time is frozen during mode inactivity. This requires adjusting all events that originate from timers, scheduled actions, and delayed connections. During mode inactivity these events are suspended and will not be present at the intended tag. Upon continuing the mode, their remaining delay is adjusted such that it reflects the remaining delay recorded at the instant the mode was previously left. This results in a notion of local time that elapses only when the mode is active. Diagrams As Section 3.2 illustrates, the extension to modal reactors also includes a graphical notation to provide an intuitive perception of the modal structures. 3.3.2 Local Time The notion of mode-local time suspends all timing behavior within inactive modes. This is an established and well-formed principle also found in modal models in Ptolemy II [LT10; Pto14] and synchronous languages such as Esterel or SCCharts. The considerations by Lee et al. that favor local time over alternative approaches also apply to LF. The suspension of time gives a clear and consistent meaning to the inactivity of modes and provides comprehensible state of the mode’s contents upon entry. This especially favors modularity, as reactors that may be instantiated in modes do not have to anticipate the fact that their time (driven by timers or scheduled actions) will advance while their reactions are suppressed. Furthermore, modes allow defining reactor elements outside of modes, which gives the developer control over which elements should be subject to local time. The timer in the ToggleLED reactor in Figure 3.4 is one example for this. Example Figure 3.5 shows an LF model that illustrates the different characteristics of local time affecting timers and actions in the presence of the two transition types. It consists of two modes One (the initial one) and Two, both in the Modal reactor. The next input toggles between these modes. The input port is controlled by a reaction on the top level that is triggered by the timer T. After one second, the mode switch is triggered periodically. Both modes’ contents are structured identically. Each has a timer T1/T2 that triggers a 70 3.3. Modal Reactors TimingExample Modal One (100 msec, 750 msec) T1 1 2 3 L min delay: 500 msec out next Two (100 msec, 750 msec) T2 4 5 6 L min delay: 500 msec out next nextnext next out (1 sec, 1 sec) T Figure 3.5. The TimingExample model for illustrating the different effects of reset and history transitions on timers and actions in modes. (Publ. in [SHL+23c]) reaction after an initial offset of 100 msec and then periodically after 750 msec. This reaction then schedules a logical action with a delay of 500 msec (the actual target code does not add an additional delay upon the minimum specified in the model). This action triggers the second reaction that writes the output out. The last reaction is triggered by the input next and invokes the transition to the other state. The main difference between the modes is that One is entered via a history transition, continuing its behavior, while Two is reset. Execution Trace Figure 3.6 illustrates the execution trace of the first 4 seconds of this program. Above the timeline are the model elements that are executed at certain points in time, together with arrows indicating triggering relations and dashed lines for distribution through time. On top of that is the currently active mode. 71 3. Modal Models 0 1000100 600 850 T1 out One 1100 2000 1600 1850 Two 1 out 2 T1 action suspends 1 T 3 LLL T2 4 5 T2 4 T 6 LLL action resumes logical time (msec) mode 2000 26002350 3000 One Two out action is discarded timer restarts with initial offset timer resumes remaining period time 2 L T1 1 L T 6 T 3 3100 4000 3600 3850 T2 4 5 T2 4 T 6 LLL action suspends out Figure 3.6. The execution trace with reaction illustration for the TimingExample model in Figure 3.5. (Publ. in [SHL+23c]) 72 3.3. Modal Reactors At 100 msec the initial offset of timer T1 elapses, which leads to the scheduling of the logical action in this mode. The action triggers the reaction 500 msec later at 600 msec and thus causes an output. At 850 msec the first 750 msec period of T1 elapses and again invokes its chain of effects. However, this time at 1000 msec the timer Tcauses a mode switch and mode One is rendered inactive. For the scheduled action, this means that its event (scheduled for 1350 msec) are suspended and will no longer trigger. The same holds for timer T1. The reset transition has no real effect on Two as the mode was never active before. Hence, mode Two starts with the initial offset of T2 triggering at 1100 msec. The following sequence of events is identical to the one that mode One produced. At 2000 msec the Modal reactor switches back to mode One with a history transition. The event of the action in Two is discarded because this mode is only entered via a reset and no suspension of events is necessary. In general, it could be conservatively suspended and then discarded when the mode is entered via reset instead of history, but this is not necessary in this case. The event of the logical action in mode One resumes. Since it was scheduled at 850 msec with a 500 msec delay and a 1000 msec inactivity of this mode, it is reintroduced for occurring at 2350 msec. Hence, the delay is kept relative to the time passing local to the mode. The same holds for the timer T1, whose second period would have elapsed at 1600 msec without mode inactivity, now it triggers at 2600 msec. After 3 seconds the next mode switch happens, which again suspends the event of the action in One. However, mode Two is reset upon entry, which effectively puts the mode in a state as if it has never run before. No events resume and timers restart with their initial offset. Hence, T2 triggers at 3100 msec and the sequence of events local to mode Two unravel in the same way as the first time. Time Progression Figure 3.7 illustrates the relation between global time in the environment and the localized time for each timer in Figure 3.5. Since the top-level reactor TimingExample is not enclosed by any mode, its time always corresponds to the global time. Mode One is the initial mode and hence progresses in sync with TimingExample for the first second. During 73 3. Modal Models 0 500 850 1000 1500 2000 2500 3000 3500 4000 One OneTwo Two 0 500 1000 1500 2000 2500 3000 3500 4000 Localized Time (msec) Global Time (msec) Mode Timing Example (T) One (T1) Two (T2) 100 1600 Leave One Leave Two Continue One Leave One Start Two Reset Two Figure 3.7. The progression of time in each mode and their respective timer of the TimingExample model in Figure 3.5. (Publ. in [SHL+23c]) inactivity of mode One the timer is suspended and does not advance in time. At 2000 msec it continues relative to this time. T2 only starts advancing when the mode becomes active at 1000 msec. The reentry via reset at 3000 msec causes the local time to be reset to zero. This example illustrates that from the perspective of timers and actions, time does not advance during mode inactivity. This also applies to indirectly nested reactors, if instantiated inside a mode. In the same way, delayed connections are affected by local time, if their source lies within a mode. This corresponds to the fact that delayed connections can be considered syntactic sugar for connections delayed by a logical action. 74 3.3. Modal Reactors Connection 1 2 3 msg Figure 3.8. The Connection reactor. 1target C; 2reactor Connection { 3input msg: char*; 4state socket: int; 5 6reaction(startup) {= 7self->socket = socket(AF_INET, SOCK_STREAM, 0); 8struct sockaddr_in server = {/*Connection configuation*/}; 9connect(self->socket, (struct sockaddr*)&server, sizeof(server)); 10 =} 11 reaction(msg) {= 12 send(self->socket, msg->value, strlen(msg->value), 0); 13 =} 14 reaction(shutdown) {= 15 close(self->socket); 16 =} 17 } Listing 3.3. Source code of the Connection reactor illustrating manual management of a socket connection. 3.3.3 Startup and Shutdown Section 3.3.1 already mentions that state variables cannot be reset by default because they might store manually managed resources. Hence, the reset trigger was introduced. This new trigger comes in addition to the two built-in triggers, startup and shutdown, that are defined by the reactor MoC [LÍG+19]. Reactions with a startup trigger will be executed at the very first tag at which their reactor exists. Symmetrically, shutdown reactions will execute during the very last tag before the reactor ceases to exist. In most programs this corresponds to the start and end of the program. Only if mutations are used, the association with a reactor’s lifetime becomes relevant. These two triggers are commonly used for initializing and finalizing manually managed resources, such as allocating memory, sensor or actuator connections, or threads for handling asynchronous interactions. Figure 3.8 illustrates a reactor that manages a socket connection. The circle indicates a startup trigger, while the diamond represents shutdown. Listing 3.3 presents the corresponding source code. The startup reaction (lines 6 to 10) creates 75 3. Modal Models a socket, stores it in a state variable, and connects it to some address. The second reaction sends a message received on the input port via the socket (line 12) and the shutdown reaction closes the socket connection (line 15). The code omits the actual address configuration for the socket, checks on return codes, and the relevant includes, to keep the example simple. While the behavior is relatively clear with respect to the reactor, the question is: How does this reactor behave when instantiated in a mode? More specifically: When are the startup and shutdown reactions triggered? This question corresponds to defining the lifetime of mode-local elements. Considerations on the Lifetime of Modes One solution could be binding the lifetime to the modes’ activity and triggering startup and shutdown upon entering and leaving a mode. This would also render the reset trigger redundant. However, in case of a history transition, the mode has to continue its behavior, requiring the previous configuration and state. And in the general case with both reset and history transitions to a mode, this can only be decided upon re-entry. Moreover, there is the challenging question of finding the right time for executing shutdown reactions upon leaving because the decision for leaving a mode is only final at the end of execution, see Section 3.3.1. Consequently, shutdown reactions cannot simply be invoked when leaving a mode. The next best alternative is to associate mode-local elements with the reactor’s lifetime. However, based on the current definition, modal reactors suppress any behavior in inactive modes, which would include reactions triggered by startup and shutdown. Hence, only initial modes would execute their startup reactions (depending on the nesting of modes), while other startup reactions would be skipped. The same applies to shutdown reactions in inactive modes at the time of a shutdown. A possible solution is to exclude startup and shutdown reactions from this suppression mechanism. However, these are reactions with arbitrary effects that now would circumvent the mutual exclusion of modes at start and end of a reactor’s lifetime. Proposed Behavior While several other options and variations were considered to solve this issue, there was no fully satisfying solution. The proposed concept is a compromise that 76 3.3. Modal Reactors •tries to minimize behavioral oddities in practical applications, • enables embedding reactor instances with startup and shutdown reactions into modes without further adjustment, and •provides intuitive and deterministic behavior. Startup reactions are executed at first activation of a mode. When the reactor is shut down, it triggers all shutdown reactions at the same time, but only those which modes were at least once active, i.e., had a potential startup reaction. Hence, the lifetime of reactor elements in modes, especially reactor instances, starts with the first activation of the mode and ends with the shutdown of the reactor. This design is a result of application-oriented considerations. Startup reactions are more common, also for tasks other than resource management, and are more likely to have effects than shutdown reactions. Therefore, preventing their execution from bypassing mutual exclusion, as in shutdown, hopefully reduces the noticeable effects of this design. The possible improvement of this behavior is considered future work but may require a more invasive redesign of resource management that in parts replaces startup and shutdown reactions, see Section 6.2.1. 3.3.4 Implementation The goal of creating a lean mode extension is not only reflected in the language design itself but also in its runtime implementation. At the time of writing this thesis, modes are implemented for C and Python, but extending support for modal reactors to other targets is already planned for future development. Nonetheless, modes have been successfully tested for these targets with single-threaded and multi-threaded execution, and inside reactors of a federation. This section provides a generic and reasonably target language-independent view on the adjustments required to support modes, achieving the behavior described in Section 3.3.1. Extending the LF Compilation and Runtime As initially presented in Section 2.2.1, generated LF programs consist of two parts, the programspecific code and the generic runtime engine. The adjustments necessary 77 3. Modal Models FurutaPendulumLive ws : WebSocket control led speaker theta d_theta phi d_phi pause disturb Paused Running sim : PendulumSimulation control disturb theta d_theta phi d_phi c : PendulumController theta d_theta phi d_phi control led s : PendulumSound angle sound 2 ws.disturb ws.theta ws.d_theta ws.phi ws.d_phi ws.control ws.led ws.speaker ws.pause pause pause Figure 3.9. The control components of the Furuta pendulum in a simulation setup connected to a user interface that supports pausing. illustrates a program that enables observing a simulation of the pendulum while running. Without going into much detail about the implementation, it communicates via a WebSocket 5 connection with a web-based user interface that displays the state of the pendulum as 3D model (Figure 1.1 is a snapshot of this visualization). The user can interact with the live system by imposing an external disturbance to the pendulum or pausing and continuing the simulation. In this example, modes are used to implement the effect of pausing by simply switching between a Paused and Running mode. The Running mode contains all the reactor instances relevant for the simulation and continues their behavior with a history transition upon entry. While this model relies on modes and their notion of local time to solve the rather simple task of pausing, achieving the same behavior with nonmodal LF is quite cumbersome in comparison. It would require adjusting all reactors inside the Running mode that have timing elements. They all would require a new input for pausing, a state variable that remembers the pause status, and all reactions need to stop producing outputs when paused. Since their local time would continue to run, timers and actions would still elapse and trigger reactions. For actions in PendulumSound, this would require some bookkeeping to discard invalidated events and reschedule actions 5https://datatracker.ietf.org/doc/html/rfc6455 84 3.4. Evaluation ModalFeeders One 1 next out Two Producer out 2 out next Three Producer out 3 out next next out (a) Multiple feeders (reaction and two reactors) to the same output port (out) but separated by modes. Modal One 1 in1 out1 Two 2 in2 out2 in2 in1 out1 out2 (b) A cyclic dependency resolved by the use of modes. Figure 3.10. Two examples for LF models that can be accepted as deterministic/ causal due to the use of modes. accordingly upon unpausing. Timers, as in PendulumController, could most certainly no longer be used as they do not offer control over their temporal behavior at runtime and would need to replaced by actions. All in all, this example illustrates the efficient temporal modeling capabilities that come with modes and their notion of local time. Static Analysis The basic principle of modes is to separate reactor elements into mutually exclusive modes. The pendulum example in its nonmodal form illustrates that the same behavior can be achieved without modes on the coordination level. However, the explicit presence of modes enables more advanced structural analyses of LF programs. This lifts certain modeling restrictions imposed under the standard LF MoC and allows accepting more programs. Figure 3.10 illustrates two such examples. 85 3. Modal Models In the absence of modes, an output port can never be fed by multiple connections to reactors or a mix of reactions and reactors, as this is a potential source of non-determinism. Only reactions have an intrinsic ordering, while reactors are inherently concurrent. However, in a model that locates these writers in separate modes, the compiler has access to this additional information. It can accept such structures, provided that all writers are mutually exclusive. Figure 3.10a illustrates such a situation. Both the first reaction and the two instances of the Producer write to the out port. The modal structure statically ensures that these writes will not happen currently at runtime. The design of modes and timing of transitions guarantee this property in all cases, except for shutdown reactions, see Section 3.3.3. Hence, these are exempted from this adjustment to the static analysis and are handled as before by the LF compiler. Furthermore, the same principle applies to causality problems imposed by feedback loops. In this case, the use of modes enables an advanced dependency analysis that takes mutual exclusion into account when detecting cycles. Figure 3.10b illustrates a model that would be rejected in the absence of modes. If both reactions could be active at the same time, it would constitute a causal cycle: in1 – out1 – in2 – out2 – in1. Hence, the structural information provided by modes enable inferring additional static information about the program that can be used to reduce the conservative over-approximation by the compiler and accept more programs. Yet, a full formal analysis of modal behavior remains future work, see Section 6.2.2. 3.4.2 Feature Comparison with Statecharts Guided by the goal of creating a lean modal extension, modal reactors only provide a minimal set of built-in features. In comparison, statecharts languages offer a much broader range of language constructs and transition behavior. SCCharts are a prime example of such a design, as they combine many features of common synchronous languages. While the fundamental concepts of states and transitions are the same, many advanced aspects 86 3.4. Evaluation were considered during the design of modes. Hence, some features are implicitly present in modes, while others are deliberately excluded in favor of simplicity. Nonetheless, LF can also utilize the target code in reactions to implement advanced behavior. Hybrid Modeling A hybrid modeling approach that combines a dataflow notation and statecharts is common in many modeling languages. SCCharts, SCADE, and Ptolemy II all provide such design capabilities, see Section 3.1.1; and likewise does LF. However, an interesting subtlety in the design of LF is its incorporation of pragmatics-aware modeling, discussed in Section 2.5. Other languages follow a rather strict syntactic separation between the dataflow and statecharts domain. Ptolemy II is a prominent example of this layered design. In LF, this separation is more distinct in the diagrams than the textual source. The concept of views facilitates a language design that seamlessly integrates modal structures into the textual syntax of reactors, while preserving a graphical notation that explicitly expresses the state machine nature of modes. Preemption In synchronous languages, transitions typically apply a form of preemption [Ber93] when a state is left. In case of SCCharts, there are strong and weak aborts, see Section 2.3. While the strong variant preempts all inner behavior of the left state, the weak variant grants a “last wish” before leaving. Technically, transitions in modal reactors always perform a weak preemption, since they allow all inner behavior to execute in the current tick and deactivate the mode afterwards. The main reason for this design is that transitions are triggered by reactions that are inner behavior of the mode. As discussed in Section 3.3.1 on the timing of transitions, mode changes that immediately preempt other behavior are complicated in this context and impose additional dependencies with a negative impact on the parallelization potential. Such problems are also present in other synchronous languages. In SyncCharts, for example, it constitutes a causality error if a state emits a signal that would strongly preempt that state. SCCharts do not have this issue, as they consider strong abort checks ordered sequentially before the execution of inner behavior. 87 3. Modal Models StrongAbortExample input signal stop output int result Compute Computation result -Stopped stop - (a) SCChart ShallowStrongAbortExample Compute Computation result 1 2 stop result Stopped stop stop result (b) LF reactor Figure 3.11. An example for a strong abort in SCCharts and a similar but shallow implementation in LF. 1target C; 2import Computation from "Computation.lf"; 3reactor ShallowStrongAbortExample { 4input stop: bool; 5output result: int; 6 7initial mode Compute { 8reset state abort: bool = false; 9c = new Computation(); 10 11 reaction(stop) -> Stopped {= 12 lf_set_mode(Stopped); 13 self->abort = true; 14 =} 15 reaction(c.result) -> result {= 16 if (!self->abort) { 17 lf_set(result, c.result->value); 18 } 19 =} 20 } 21 mode Stopped {} 22 } Listing 3.4. Source code of the ShallowStrongAbortExample reactor. While the proposed modal reactors model does not include preemption, there were considerations for including this feature, for example in the form of special “initial” reactions that would be executed before any other reactor elements to determine and suppress preempted content. However, such a design was deemed expendable in the face of a lean language design and the fact that LF already offers many ways to influence the transition triggering in reaction bodies by using target language capabilities. Figure 3.11 illustrates a small example modeling a strong abort in SCCharts and a variation in LF that emulates a form of shallow preemption. Listing 3.4 presents the source code of the reactor. The first reaction sets the abort variable (line 13) to prevent an effect on the result output in the 88 3.4. Evaluation second reaction (line 16). Admittedly, this exemplifies only a preemption of the behavior of the second reaction but not a true hierarchical preemption of the internal behavior in the Computation reactor. It rather suppresses the observable effect of the behavior in Computation and, hence, could be considered a shallow abort. Nonetheless, it illustrates the general procedure. To explicitly abort the internals of Computation, the reactor would require an additional input to pass on the abort variable downstream as an event and react accordingly inside the Computation reactor. However, the LF community has not yet requested a more convenient built-in strong preemption feature and, as of yet, there are no use cases that justify an introduction. Termination SCCharts and SyncCharts also feature the non-preemptive termination transition type, see Section 2.3, that is enabled when all inner regions reached a final state. It corresponds to joining one or more spawned threads. However, termination is a control-flow concept that does not make much sense in a dataflow language that does not model concurrency as explicit threads or that does not provide built-in constructs that indicate termination. Modal reactors could give an opportunity to introduce such a feature, but the proposed concept simply embraces the dataflow in LF and keeps the extension lean. Priorities With the use of reactions as transition triggers comes another difference in comparison to SCCharts and other statecharts dialects. They usually use priorities to assign an order to available transitions, with the first enabled transition preempting lower ones. While the preemption aspect was already discussed, modes in LF have exactly the inverse behavior, where the last invocation of lf_set_mode in reaction order determines the actual transition. An implementation for setting modes in reactions that favors the first writer could be easily achieved, but the proposed design favors the analogy to setting output ports. Immediate and Delayed A timing aspect, predominately present in synchronous languages, is the distinctions between immediate and delayed transitions, see Section 2.3. Section 3.3.1 already explained arguments on why immediate transitions are not supported in this proposal for modal reactors. 89 3. Modal Models Deferred Some languages, such as SCCharts or SCADE, also provide deferred transitions. They suppress the immediate behavior of an entered state. This concept assumes that transitions are instantly processed and, hence, represent a way to enter a state delayed by one tick. Considering the microstep delay for transitions in modal reactors, as discussed in Section 3.3.1, one might argue that these transitions are always deferred. This is also illustrated by the fact that the SCCharts variant of the PendulumController uses a deferred transition to produce a behavior equivalent to the LF model, see Section 1.1.2. Reset and History While reset and history transitions in modal reactors are equivalent to statecharts, SCCharts feature a further distinction of history transitions into a deep and a shallow variant, see Section 2.3. While the shallow history only affects the direct elements of the target state and resets nested statechart, the deep variant continues the behavior recursively. In pursuit of a lean design, modal reactors only implement a deep variant. 3.4.3 Modes as Mutations In the current concept for modal reactors, modes are established as a core language feature and implemented directly in the LF runtime. However, early on in the design process, there was the idea to define and implement modes via mutations [LÍG+19]. Mutations offer an interface to restructure a reactor at runtime. Using this concept as a foundation for modes would mean that modes would be translated into mutations for each modal reactor. The mutations would make sure that at runtime a modal reactor only contains the elements of the currently active mode. Upon transition, the mutations would destroy all these elements and create those defined the target mode. However, this approach assumes that the lifetime of modes is bound to its activity. Such a design would conflict with the support of history transitions, as already discussed in Section 3.3.3. Mutations would need to store and re-apply the state of modes that are entered with history. Furthermore, the interface for mutations is intended for end-users and does not provide the capabilities to manipulate events sufficiently to implement 90 3.4. Evaluation mode-local time as in Algorithm 3.1. In the absence of history behavior, an implementation with mutations would be feasible, but history transitions were considered more important. Another consideration that argues against mutations is their intended use case. Mutations are designed to give the user the opportunity to dynamically adjust the elements of a reactor. For example, instantiating a number of reactors for a parallelized processing of data, such as a map-reduce pattern with a variable input size. In contrast to that, modes are a more static feature that select which parts of the program are active at a certain point in time. 3.4.4 Embedded SCCharts Section 3.1 discusses various related approaches that represent alternatives to a modal reactor implementation in LF. Let us investigate such an alternative design by conceptually embedding SCCharts as a target language in a non-modal LF. This approach would utilize the polyglot nature of LF to include a notation that can naturally express modal models and facilitates the extraction of mode diagrams. Concept Figure 3.12 illustrates an example for the proposed design and presents the compilation infrastructure necessary to support SCCharts embedded in LF. The file ao.lf in the top right corner represents the source LF program. The reactor uses SCCharts as a target language, but also C to indicate the code synthesis target for the SCCharts. The program models a very simple behavior that waits for the presence of the input Aand passes its value on to the output O. The following Done state does not permit a repetition of this process. In order to create executable code, the LF compilation requires an additional intermediate step. In this step, the SCCharts code is extracted from the reaction and put into a separate artifact, ao.reaction.sctx on the right. While the code in the reaction body implicitly assumes the presence of the declared interface, as it usual in LF, the SCChart is now completed with the necessary declarations, to yield a valid model. The events are encoded as signals to represent the event’s presence and payload. 91 3. Modal Models ao.lf target SCCharts, C; reactor AO { input A:int; output O:int; reaction(A) -> O {= scchart { inital state Wait if A do O(val(A)) go to Done state Done } =} } ao.reaction.sctx scchart AO { input signal int A output signal int O initial state Wait if A do O(val(A)) go to Done state Done } LF Intermediate Compilation LF Compilation C Compilation AO Executable ao.intermediate.lf target C; reactor AO { input A:int; output O:int; state scchart:{=TickData=}; reaction(startup) {= reset(&self->scchart); =} reaction(A) -> O {= self->scchart.A = A->is_present; if (A->is_present) self->scchart.A_val = A->value; tick(&self->scchart); if (self->scchart.O) lf_set(O, self->scchart.O_val); =} } LF Runtime ao.tick.c ao.tick.h typedef struct { char A; int A_val; ... } TickData; void reset(TickData* d); void tick(TickData* d); ao.intermediate.c ... int main(int argc, char* argv[]) { return lf_reactor_c_main(argc, argv); } ... SCCharts Compilation AO ao input signal int A output signal int O Wait Done A / O(val(A)) - SCCharts Synthesis LF Synthesis Figure 3.12. Conceptual structure of an LF compilation with an embedded SCChart. 92 3.4. Evaluation The second output of the intermediate compilation is an adjusted LF source, ao.intermediate.lf on the left. The SCChart in the reaction body is replaced by C code that handles the invocation of the tick functions, as described in Section 2.3.2. Additionally, the program now has a state variable (scchart) to store the internal state of the SCChart and a startup reaction to initialize this data structure.6 In the subsequent compilation, the intermediate LF code can be ordinarily processed by the LF compiler, while the SCChart is compiled into its tick infrastructure by the SCCharts compiler. Finally, the C compilation combines all artifacts into an executable. In addition to the compilation, the LF diagram synthesis can likewise embed the SCChart. By invoking the SCCharts synthesis to create a diagram from the completed SCCharts model, the LF diagram could display the state machine inside the reaction figure, as illustrated in the top right corner. Evaluation Regarding the goals for a modal model in LF, such a design retains the determinism due to the use of SCCharts and is still compliant to the polyglot black-box approach, as the semantics of LF do not rely on a white-box analysis of the SCCharts code. Yet, there are several disadvantages to such a concept, as already mentioned in the context of similar related work, see Section 3.1. Most importantly, this design only provides modal reactions, since the SCCharts code does not support embedding reactors, neither practically nor under the black-box abstraction of reactions. Hence, it does not actually constitute a modal notion for the LF coordination layer but only for individual reactions. Furthermore, this alternative concept reintroduces the problem of nonaligned time. The modal behavior is again confined to a reaction and does not provide for association of timers with modes. However, the concept of dynamic ticks, presented in Chapter 4, improves the timed modeling capabilities of SCCharts in a way that it could handle time locally. 6 This example uses default names for the tick function and other variables. In the presence of multiple reactions with SCCharts code, this concept requires a naming scheme that prevents conflicts. 93 4. Time Efficient Execution (2.) The SCCharts implementation of the Furuta pendulum counts milliseconds to control its timed behavior, as presented in Section 2.4. Consequently, over the course of a three seconds long execution, (at least) 3000 ticks need to be executed in order to yield the intended behavior w.r.t. to real-time. Moreover, such an execution is only feasible if the computation time for each tick is below 1 millisecond. Otherwise, the behavior would lag behind, as tick execution must not overlap. For the same reason, milliseconds were chosen as a compromise for time granularity in the SCCharts implementation. A higher precision increases the general execution load and may cause delays. Yet, a more coarse-grained resolution will impose delays when timed effects are rounded up to the next millisecond, as it is the case for the sound signal in the SoundController SCChart. Section 4.5.1 will investigate the tick load of different implementations. It reveals that the LF model requires only 1300 ticks in the same three-second simulation 1 , while producing a more precise timing for the sound signal. This is a result of the sparse event-driven execution that only triggers a tick if an input event occurs or an internal timing event fires, such as timers or actions. Hence, a comprehensive timed modeling concept should include a dynamic (sparse) tick execution to decrease the system load. In turn, this opens up space for (theoretically) scheduling ticks onto more precise points in time. Goals This chapter investigates how to incorporate physical time into synchronous languages, using SCCharts as an example. While such an endeavor is not new and there are many viable solutions in various other languages, see Section 4.1, the goal is to emphasize efficiency in terms of runtime and implementation, as well as modeling aspects in the context of synchronous statecharts. This particularly includes evaluating and incorporating the latest developments in sparse and event-driven execution models, as in LF or with dynamic ticks by von Hanxleden et al. [HBG17]. More specifically, the design is guided by the following principles. 1 This simulation of the pendulum works at a 5 msec pace, which makes tick loads below 3000 possible. 100 Determinism The semantics should fit seamlessly into the synchronous paradigm and provide deterministic behavior, e.g., outputs are fully determined by inputs. For SCCharts that means there should be no changes to the underlying SC MoC. Resilience A solution must cope with run-time variations and imperfections of physical timers. It should be possible to avoid accumulations of timer imperfections and to detect variations and lags. Scalability The number of (concurrent) timers should not be restricted or impose significant overhead per timer. Fine granularity The specification of time constrains should not be restricted by a specific granularity. For example, it should be possible to specify timeouts of 1 sec and 3.1415926 msec in the same model. Time composability Time-based constraints should remain their intuitive semantics if composed. E.g., waiting 1 sec twice should mean the same as waiting 2 sec’s once. Simultaneity and order Timers that started in the same tick and run the same duration should expire in same tick. Lean interface The inference between the model and its environment should be simple, lean, and independent of application specifics or the number of timers. Seamless compiler integration In the context of SCCharts, any solution should fit into the incremental compilation concept [MSH14; Smy21]. It should consist of a minimal core, with more advanced modeling aspects implemented as extended features, see Section 2.3. The concept of timed SCCharts presented in this chapter embodies these very principles and implements dynamic ticks to create a precise and efficient execution model with a light-weight interface and implementation. Outline This chapter starts with a brief overview of related work on time in modeling languages and synchronous languages in particular. Next, Section 4.2 will introduce the timed automaton notation in SCCharts and 101 4. Time other modeling capabilities of timed SCCharts. Section 4.3 discusses different execution regimes for a timed model, ultimately settling for dynamic ticks. Then, Section 4.4 illustrates how dynamic ticks are implemented in SCCharts and discusses strategies to deal with imperfections when exposed to physical time. Finally, Section 4.5 evaluates the performance of timed SCCharts and compares the design to event-driven approaches, such as LF. 4.1 Related Work Time plays an important role if a program has to work in relation to the real world, most prominently in the form of real-time systems. The same holds for distributed execution [LL21]. Many specification models and languages have been developed over the years that provide notions of time. Here, synchronous languages are again of particular interest to this thesis. 4.1.1 Modeling with Time Specifying a model with explicitly timed behavior requires a capable modeling formalism and a notion of time. Timed Automata A formalism for timed models that is particularly relevant in the context of state machines and SCCharts are timed automata by Alur and Dill [AD94]. Timed automata consist of state-transition graphs with additional real-valued clocks that enable expressing timing constraints for transitions. They extend the theory of ω -regular languages into timed words that pair the input word with an (infinite) sequence of real-valued time values indicating their occurrence. This results in a dense-time model. Clocks are similar to regular program variables but bound to the continuous flow of time. Having multiple clocks with the option to independently reset their values in addition to their natural progression provides a powerful and flexible modeling concept for the specification of temporal constraints. Timed automata in different forms and variations have been extensively studied for verification purposes [AD94; ACH+95; OSY94; HNS+94]. In the context of this thesis, they will be used with a focus on code synthesis and 102 4.1. Related Work the synchronous MoC. This includes the investigation of practical execution strategies, see Section 4.3. Altisen and Tripakis [AT05] investigate the effects of execution semantics and platforms on the timed automaton behavior. They propose an implementation methodology that wraps a timed automaton into a global execution model, to decouple the real-time access and interpret the original model based on simulated time. This approach makes it possible to keep a fixed behavior for timed automata that is independent of influence of the execution environment on timers, which facilitates platform-independent verification. This thesis will not focus on the topic of verification, but the interface of timed SCCharts to their environment also facilitates a form of wrapped simulated time. However, as Section 4.4 will discuss, it also supports the opposite approach by providing access to the raw real time. Exposing the model to platform-specific imperfections may yield a different behavior but also enables the model to detect them and adjust its control behavior accordingly. Multirate Timed Automata Timed automata have been extended in various ways, one example are multirate timed automata (or multirate timed systems) [ACH+95]. There, each clock progresses at its own speed, possibly varying between a lower and an upper bound. This further extends the capabilities of clocks to model timed behavior, e. g., in the context of Cyber Physical System (CPS) [LS17]. Olivero et al. illustrate that multirate timed automata can be mapped to single-rate timed automata [OSY94]. The implementation of timed automata in SCCharts will feature singlerate clocks, but their design as an extended feature also facilitates a more advanced behavior in the future. Discrete Timed Automata Pinisetty et al. [PRS+17] introduce discrete timed automata to formalize runtime enforcement of CPS, also using SCCharts in the process. Instead of real-valued clocks they use discrete clocks, counting specific timed events, in this case periodic ticks. While timed SCCharts may also use integer-typed clock implementations to circumvent issues of floating-point arithmetic, discussed later in 103 4. Time Section 4.2.2, they rely on a dense-time model. Furthermore, dynamic ticks are specifically designed to overcome a fixed discrete time progression, as in a periodic execution, see Section 4.3. Uppaal The Uppaal tool provides an environment for modelling and verifying real-time systems using timed automata [LPY97]. These systems are specified as a network of non-deterministic sequential processes featuring concurrency, advanced data types, and communication channels with synchronization and prioritization capabilities. Uppaal supports model checking and simulation by using symbolic interpretation and statistical model checking techniques [BBB+10]. For timed automata in SCCharts the focus lies more on the aspects of practical real-time modeling in a synchronous context, rather than verification. Nevertheless, with model checking capabilities in SCCharts [Sta19], there is also potential future work in this direction. CCSL The Clock Constraint Specification Language (CCSL) [AM09] is a notation for expressing clock domains and relations, independent of a specific programming language. Clocks in the sense of CCSL correspond more to the concept of polychronous systems [GTL03], rather than clocks in timed automata. Yet, CCSL not only provides patterns of classical synchronous clock constraints for multiclocking [GG10] or asynchronous clock relations [Lam78], but also real-time representations of physical time. For example, CCSL is used in a simulation and debugging tool for LF programs [DCB+21]. For timed SCCharts, CCSL opens up a future avenue into multiclocked and polychronous systems design, see Section 6.3.2. Ptolemy The heterogeneous modeling environment of Ptolemy II provides different domains to express timed behavior, such as discrete events or continuous time [EJL+03; Pto14]. It also includes a multirate timed automata implementation, illustrated later in Figure 4.1. Internally, time is a global property of the simulation and provided as a single unit to all components. A floating-point number specifics its resolution, but to ease and harden time arithmetic, time itself is handled in the form of integer multiples of that resolution [CLB+19]. 104 4.1. Related Work In timed SCCharts, time also conceptually originates from a real-valued domain, but the implementation is adjustable on an application-specific basis, see Section 4.2.2. ROOM The real-time modeling capabilities of the actor-oriented ROOM language [SGW94] include time-controlled behavior. In contrast to a modelbased specification, such as timed automata, ROOM supports the periodic creation of events [SFR97], similar to timers in LF. Additionally, the ROOM virtual machine provides access to a low-level timeout service. Timing constraints in ROOM mainly concern classical real-time scheduling and response times analyses, as they specify bounds on arrival times of timetriggered events and deadlines on event-processing sequences [SFR97]. While timed SCCharts can be used for hard real-time tasks, see Section 4.5.2, this proposal does not investigate the combination with real-time scheduling strategies or analyses. Statecharts Harel’s proposal for statecharts also includes expressing timed reactions [Har87]. Using an implicit notion of timers, a transition can specify a timeout based of the occurrence of an event or the entry of the state. Timers refer to a global notion of discrete time steps that is controlled by the way the model is simulated [HN96]. The effects of different simulation strategies on timeouts are similar to the consideration of logical and physical time in Section 4.4. However, timeouts in statecharts are an abstracted notion of discretized time and do not provide access to real time, limiting the model in reacting to its actual environment. Furthermore, timed SCCharts account for both discrete and real-valued models of time. 4.1.2 Synchronous Languages Classically, synchronous languages rely on a more abstract notion of time. Yet, there are several synchronous languages that handle time in a more robust and precise fashion compared to the multiform notion. Esterel In its classical form, Esterel relies on the multiform notion of time [Ber99]. Bourke and Sowmya investigate the implications and draw105 4. Time backs of this design, such as imprecisions when measuring time intervals via fixed-paced time inputs and inconsistencies between multiple time inputs in different granularity [BS09]. They propose an extension by realtime delays. These timed delays act as a form of abstract macros that are subsequently implemented using sampling or event-based strategies, similar to the considerations in Section 4.3. However, there is a gap between the expressed timing constraints and the actually provided behavior by the (platform-specific) implementation. This was one motivation for the development of dynamic ticks by von Hanxleden et al. [HBG17]. The proposed concept for timed SCCharts tries to overcome this gap by using dynamic ticks and the option to handle raw physical time inputs in the model. Zélus Zélus [BP13] mixes both discrete time and continuous time behavior specification in a single synchronous language. It uses a discrete Lustre-like dataflow syntax with automata and combines it with ordinary differential equations for continuous behavior. At runtime, an external solver simulates the continuous time domain and detects zero-crossings, at which the discrete sections of the program can react. The type system and causality analysis ensure that the hybrid segments correctly align and no discontinuities occur during integration of the two domains. The proposal for time in SCCharts does not aim to express continuous behavior but to provide a timed extension that enables explicit modeling of time-related behavior based on a combination of real-valued and logical constraints. Argos The statecharts-like synchronous modeling language Argos [Mar92] is a predecessor of SyncCharts [And03] and thus in spirit also of SCCharts. An extension by Jourdan et al. introduces the specification of temporized states for verification purposes [JMO93]. States can carry timeouts, similar to statecharts, and must be left before it expires. Timeouts in Argos are abstract and can either be implemented by dedicated discrete events that are passed to the program but cannot occur simultaneously with other inputs, or by internal timed automata. However, Argos does not provide an accessible notion of time to handle differences in the implementation, as timed SCCharts strive for. 106 4.2. Timed Automata in SCCharts Céu The imperative synchronous language Céu [SIL+17] is strongly inspired by Esterel. However, there are some key differences, such as the notion of time, which is a first-class citizen in Céu. Timers can be used to express real-time delays and expose physical lag to the program to enable adjusting the behavior. Timing events dynamically trigger reactions and the Céu runtime tries to automatically compensate for physical lag. There are many similarities between the handling of time in Céu and timed SCCharts. However, a core difference is the fact that Céu uses an event-based runtime and thus is more closely related to LF. This includes a notion of logical time for events. In contrast, the concept of timed SCCharts embraces the classical tick function-oriented approach and is not bound to an event queue or event-based processing. The Sparse Synchronous Model Inspired by the concept of PTIDES [ZLL07; ELM+12], Edwards and Hui developed the Sparse Synchronous Model (SSM) [EH20; HE22]. It combines an event-driven, and hence sparse, execution regime with the principles of synchronous languages. Consequently, it is closely related to Céu and also LF. While externallyand time-triggered reactions are driven by events, the internal program behavior is synchronous and based on activation of routines, similar to reaction in reactors but permitting recursion. In terms of timing specification, the SSM provides a statement that postpones writes to variables based on a real-time delay, while another one can wait for the occurrence a write access. With dynamic ticks, timed SCCharts also achieve a more sparse execution regime but also provide a more flexible interface for real time behavior. 4.2 Timed Automata in SCCharts Timed automata are a well-established and extensively studied formalism for the behavior of real-time systems, see Section 4.1.1. The research question investigated in this section is: How can we seamlessly integrate timed automata into SCCharts, while maintaining the underlying MoC and modeling principles and capabilities? In particular, this includes practical considerations, such as a robust execution semantics, efficient and scalable 107 4. Time 4. HYBRID SYSTEMS Figure 4.7: A timed automaton that generates a pure output event every Ttime units. Figure 4.8: A timed automaton variant of the traffic light controller of Figure 3.10. Lee & Seshia, Introduction to Embedded Systems 87 Figure 4.1. Trafficlight controller modeled as timed automaton by Lee and Seshia [LS17] (CC BY-NC-ND 4.0). code generation, and handling varying granularity in the time representation, imposed by the application environment or hardware. Additionally, this section will investigate the utilization of timed automata into a higher level construct for multiclocked synchronous programs. The Traffic Light Controller Example The Furuta pendulum example illustrates the need for improved timed modeling capabilities in SCCharts. However, the parts of the model that can be expressed in timed automata are relatively small and are best matched with more advanced concepts, as Section 4.2.3 will illustrate. Hence, to introduce, discuss, and investigate the basic notion and semantics of timed automata in SCCharts, the traffic light controller is better suited example. It is a model used by Lee and Seshia [LS17] to discuss (multirate) timed automata in the context of CPS design. Figure 4.1 shows this traffic light controller. The represented traffic light has three lights, green, yellow, and red, to control the car traffic. An additional button for pedestrians causes the traffic 108 4.2. Timed Automata in SCCharts light to temporarily switch to a red light to stop the traffic and provide for a safe crossing of the street. The controller handles the timed behavior of a single traffic light. It has a real-valued clock x, a pedestrian input that indicates a pedestrian request for crossing, and three outputs sigR,sigG,sigY. The type pure denotes a signal without payload that is either present or absent at each reaction. For the pedestrian input this denotes the event of pressing the button. Likewise, the outputs use the signal to trigger color changes rather than controlling the state of the light directly. It is assumed that the red light is turned on initially and subsequently emissions of signals will switch from the current configuration to the requested one. In this notation, the clock is represented by a first-order differential equation on a real number. It can be explicitly set (e.g., x(t):= 0) or used as a transition constraint. Time progresses in states controlled by an explicit derivative, in this example one ( x ˙(t) = 1). Furthermore, the resolution of time is expressed in abstract units. For this example, we can assume that one time unit corresponds to one second. The automaton for the controller consists of four states red,green,yellow, and pending, with red as the initial one. Transitions between states carry optional guards and effects, using the same notation as in SCCharts. One could denote guards as triggers, analogously to SCCharts, but this would already imply a specific execution semantics, as discussed in Section 4.2.1. The system starts in the red state. When the clock xreaches or surpasses the threshold of 60, the transitions to green is enabled, which will emit the signal for switching to a green light and resetting the time to zero. In the green state the system waits for a pedestrian to push the button, but the following state depends on the passed timed. Case 1, if less than 60 sec passed since entering green, the automaton will transition to pending, but x is not reset. It remains there until the time has reached at least 60 sec, then the yellow light is turned on, the timer is reset, and the state is switched to yellow. Case 2, if the pedestrian signal is received after at least 60 sec have passed, the automaton transitions directly to yellow with the same output and reset. After at least 5 sec in state yellow, the automaton switches to red, signals a red light, and resets the time in x. 109 4. Time Counter Reset output int counter = 0 Wait Increment / counter++ -Increment Wait Reset counter >= 10 / counter = 0 -Reset Figure 4.6. A concurrent counter reset, illustrating the fundamental problem with clocks managed by a single concurrent during action [SSH19]. (©2019 IEEE) The issue is caused by the now concurrent during action and its relations to the resets and readers. Previously, the sequential relation of inner state behavior and outgoing weak abort transitions constituted their ordering, but now they are subject to the concurrent communication protocol. However, the IURP orders updates (here, the clock progression) after the initializations (reset) and both before reads, while the transitions enforce a sequential order from reading the clock to resetting it. This constitutes a causality issue. Figure 4.6 illustrates the underlying problem. It shows a counter (corresponding the clock) that is updated while concurrently read and then reset. Additional arrows indicate the data dependencies imposed by the IURP (blue for initialization Ñupdate and green for update Ñread). One way to work around this issue could be the encoding of the clock update as an absolute write while users have to express resets as updates (e.g., x -= x). However, the SC semantics are not conceptually bound to the IURP, as it is only one possible synchronization protocol implemented for SCCharts, and should not be limited by it. For this reason Smyth et al. created Scheduling Directives (SDs)[SSH19]. The issue with clock resets was one motivation to extend the SCCharts compiler to support customized scheduling protocols that override the default IURP. The SCChart in Figure 4.5 contains the SD xSD that introduces a scheduling regime for the clock x. The ClockUIUR regime is an extended variant of the standard three-staged IURP, but with an additional phase at the beginning for advancing the clock. The SCChart shows that only the during action is assigned to this stage (xSD 0), while the transitions indicate that some of 116 4.2. Timed Automata in SCCharts their triggers and effects are subject to phase one (reset) and three (read). The current visualization does not yet support a per statement display of scheduling assignments, as present in the source code. Classical updates (relative writes on xby the user) that would fall in stage two are not present. The declaration of xSD lists stages as conflicting and commuting, which has no further effect in this specific example and will be discussed in more detail in Section 5.4.2. The use of the custom SD xSD renders the SCChart in Figure 4.5 permissible for the SCCharts compiler, while providing the same behavior as the model in Figure 4.4 because the clock progression is scheduled before any other access. Similarly, the same issue arises with hierarchy, even in the absence of concurrency. At a first glance, one could think that adding during actions only to inner states but not the superstates, following the previous strategy, would be sufficient. However, regions may terminate, leaving no active state other than the superstate, and this state may not be left at that time (e.g., in the absence of a termination transition). This results in clocks not being updated. Yet, updating clocks only in the top-most superstate, again, creates a concurrent context between this during action and inner resets, and that requires an SD. Compositional Effects on Time Progression By default the SCCharts compiler tries to use the simple transformation, since it best corresponds to the classical flat timed automata schema. If concurrent or hierarchical use of a clock is detected, an error is raised suggesting the activation of the advanced transformation. This is a manual process because it changes the way clocks interact with other SCCharts features. The simple transformation assumes that there is only one active state using a specific clock. This state controls the progression of time in that clock, e.g., illustrated by the state-local rates in Figure 4.1. Hence, any effects on the active state of the timed automaton also affect the clock. For example, if the state is suspended, so is the progression of time; and preemption of the state likewise preempts the clock. In the transformation with support for concurrent access, the behavior is different. Here, the clock is bound to the superstate it is declared in. Hence, 117 4. Time if any contained region or inner state is suspended, it does not affect the progression of time. This is important, since states in other regions may not be suspended and rely on the clock’s progression. Only effects concerning the state or region declaring the clock will influence its behavior, since this is the location of the synthesized during action that handles the progression of time. Time Resolution The transformations illustrated in Figure 4.5 and Figure 4.4 both convert the clock declaration into a float 4 variable. While this is in line with the formal definition of timed automata and enables normalizing time to the common (SI) base unit seconds, it subjects the practical implementation in SCCharts to the known limitations and imprecision of floating point representation and arithmetic in computers, such as quantization errors [CLB+19]. For demonstration purposes or in models without a known hardware context, such as the traffic light controller example, such an approach is acceptable. However, as soon as the model is supposed to run on hardware and meet its specified timing behavior, a more robust integral-based resolution is usually desired. This for example to preserve the associative law for additions. Yet, this requires a more hardware-platformspecific implementation, which is difficult to provide generically. For example, if targeting a nanosecond resolution in C, the standard time library can provide this precision on Linux, but Windows only yields milliseconds or requires a different API. Embedded processors also vary in supported time access and resolution. Furthermore, effectively handling time in nanoseconds requires integer types with more than 32-bit, which is supported on common platforms but cannot be guaranteed when working with embedded processors. LF solves this issue by providing a reasonably platform-independent time API for each target language. In C, these are macros 5 , such as SEC in line 17 of Listing 2.4. Time specifications on the LF coordination level, for example 15 msec in line 14 of Listing 2.6, internally use the same macros. A preprocessor directive can switch these macros between micro and nanosecond precision. 4 In SCCharts float is an abstract floating point number and does not express a specific precision limitation. 5https://github.com/lf-lang/reactor-c/blob/4c97e960d9a40d60dfb3725678dbd38176023f45/include/ core/tag.h 118 4.2. Timed Automata in SCCharts While this approach is appropriate for LF, since it controls the compilation of the execution environment for LF programs, SCCharts follow a more abstract approach in accordance with the concept of generating tick functions, see Section 2.3.2. The deltaT interface likewise aligns with this concept and puts the extraction of time into the hand of the external environment. For timed automata in SCCharts, the float type acts as the default type. However, the transformation can be configured to synthesize any type. For example by annotating the SCChart with @IntegerClockType "int64_t", the code generator produces host code type for 64-bit integers in C, see Section 2.3.3. Yet, the timing guards may require manual adjustment to the targeted resolution. This can be done by appropriate constants, as in line 6 of Listing 2.5, or using methods introduced alongside OO in Section 5.3.1. The timed automaton implementation of the Furuta pendulum in SCCharts presented in the next section will illustrate this approach by using an SCCharts-based class to provide time conversion utilities. This way, one can achieve a reasonably platform-independent design that is easily adaptable to changes in hardware. Alternatively, an SCChart can be specified with implicit knowledge about the external resolution of time, as in Figure 4.23 in the context of the DS demonstrator. Furthermore, timed SCCharts provide the special type time for use in combination with clocks. During compilation, time declarations will automatically adjust their type to the one used in clocks and deltaT, i.e., they comply with the @IntegerClockType annotation. This enables the user to store time independent of the actual resolution and host type, and keeps hardware-specific modeling at a minimum. 4.2.3 The Furuta Pendulum in Timed SCCharts In the Furuta pendulum example, both the PendulumSound and PendulumController use timed behavior and can be re-modelled using timed SCCharts. The actual changes only involve replacing the milliseconds counters by clocks. 119 4. Time PendulumSound input ref TimeUtil tu input float angle output bool sound = true clock t time duration = 0 immediate during / duration = tu.sec(1 / sound_frequency(angle) / 2) Alternate t >= duration / sound = !sound; t -= duration - Figure 4.7. The PendulumSound component modelled as timed SCChart. Pendulum Sound Figure 4.7 illustrates the PendulumSound SCChart as a timed automaton. In contrast to the original implementation, see Section 2.4.2, this component no longer requires the msec input, the msecs counter, or the during action in state Alternate. Instead, it relies on the new clock tto track time automatically. Considering that the transformation for timed automata will reintroduce the same components to track time in clocks shows the nature of extended features. Compared to the traffic light example, this model does not use a fixed value as timed guard but another variable to model the angle-dependent shifting of the threshold for the sound signal. This extends the classical timed automaton model [AD94], which only permits constant thresholds. While fixed value constraints ease verification, this example shows that variable thresholds are also relevant in practice. The transformation of timed automata in SCCharts naturally supports this feature. Another difference to the previous implementation is the use of the time type for the duration variable. This ensures the time resolution and type matches the clock t. In the same spirit, the sec method is used in the during action to convert the half cycle length into the appropriate resolution. The method is provided by the tu object of type TimeUtil and is passed as an input to the SCChart. Section 5.3 will provide a detailed introduction of these OO features. In this example, TimeUtil represents an interface for time conversion, inspired by the LF macros. The concrete object that is passed as input will implement these methods for a specific time resolution, e.g., 120 4.2. Timed Automata in SCCharts PendulumController input ref TimeUtil tu input float theta, d_theta, phi, d_phi output float control = 0 output bool led = false float catch_phi SwingUp immediate during / control = swingup_control(theta, d_theta) Catch during / control = catch_control(theta, d_theta, phi, d_phi) period tu.msec(15) Toggle / led = !led -LED Stabilize during / control = stabilize_control(theta, d_theta, phi, d_phi, catch_phi) exit_swingup(theta) / led = true exit_catch(d_phi) / catch_phi = phi; led = true exit_stabilize(theta) / led = false - Figure 4.8. The PendulumController component modelled as timed SCChart. nanoseconds. In the future, the interface and common implementations may be provided as a standard library by the SCCharts tool. This approach illustrates how the model can be kept independent of the underlying time resolution and easily adapted to new platforms. Alternatively, one could use hard-coded factors in the model, such as SEC_TO_MSEC in Listing 2.3 or invoke host code functions to achieve a similar design. A last difference that should be noted in comparison to the traffic light example is the way the clock tis reset. Instead of setting the clock value to zero, only the duration threshold is subtracted. This design is a precaution for timing imperfections in the actual execution, if tis bound to physical time. Section 4.4.3 will discuss this “soft” reset in detail. Pendulum Controller In the PendulumController component, the only timing aspect is the periodic blinking of the LED during the Catch mode. While 121 4. Time this again can be solved with a timed automaton, the SCChart model in Figure 4.8 illustrates the use of another extended feature in timed SCCharts: periodic regions. The period directive confines a region (or state) to a periodic activation. In this example, the state machine in the LED region toggles the boolean value unconditionally in each step, but the period will ensure that these reactions are 15 msecs apart. The next section will illustrate that this feature has a straight-forward translation into timed automata and can be considered syntactic sugar. 4.2.4 Multiclock SCCharts Timed automata naturally support multiple clocks and so does its SCCharts implementation, as there is no restriction of the number of clock declarations. In synchronous languages, there is also the concept of multiclocking [GG10], for example in Signal or Multiclock Esterel by Berry and Sentovich [BS01]. However, in this context the term “clock” does not describe real-valued time measurement but a hardware clock that drives a hardware circuit or similarly designed software. In other words, this notion of clocks refers to the source of discrete synchronous ticks. In multiclocked systems, different parts of the program are activated by different clocks. These clocks refine a base clock and can be considered additional inputs to trigger specific parts of the program. Polychronous systems [GTL03], as in Signal, go beyond refining clocks and support loosely coupled clocks synchronized by clock relations and hierarchies. Multiperiodic SCCharts With the period directive, timed SCCharts provide means to express multiclocked SCCharts based on real-time. Periodic regions and states subject their inner behavior to a new clock that refines the base clock of the model. Instead of deriving their pace directly from the discrete ticks of the base clock, periods bind it to a real-time clock used in timed automata. This is especially relevant for modeling with dynamic ticks, as presented in Section 4.4, because dynamic ticks do not provide a periodic base clock to refine but instead derive the pace for ticks dynamically from inner timing requirements. 122 4.2. Timed Automata in SCCharts TwoLEDs output bool ledA = false, ledB = false period 2.5 / ledA = !ledA -A period 0.333 / ledB = !ledB -B (a) SCChart with multiple periodic regions TwoLEDs output bool ledA = false, ledB = false clock c = 0 bool tick = false tick / ledA = !ledA -A 1: c >= 2.5 / c = 0; tick = true 2: / tick = false -Period -A clock c = 0 bool tick = false tick / ledB = !ledB -B 1: c >= 0.333 / c = 0; tick = true 2: / tick = false -Period -B (b) Transformed SCChart Figure 4.9. Example of a multiclocked SCChart that has two LEDs blinking in different frequencies. Transformation Figure 4.9a illustrates a multiclocked SCChart using periodic regions. The example is inspired by the LED handling in the Catch mode in Figure 4.8. It simply toggles two LEDs,ledA and ledB on and off. Each in separate regions and with different periods, 2.5 sec for ledA and 0.333 sec for ledB. Figure 4.9b shows how this extended feature is transformed into a timed automaton during compilation. Both regions Aand Bare transformed individually but follow the same pattern. The inner states of the region are moved into a new super state that declares a new clock variable cand 123 4. Time a boolean flag tick. The tick variable acts as guard for all reactions in the original state machine. In this example, they are added to the self-transitions toggling the LEDs in each region. If any transition or action has its own guard, it would be conjuncted with tick. This prevents the inner SCChart from performing any action unless enabled by tick. This approach corresponds to the concept of suspension, present in synchronous languages, such as Esterel or SCCharts. In this case, tick is initialized to false, which means that no reaction takes place in the initial tick. However, there is also an immediate period directive that initializes tick to true and enables an initial reaction. Additionally, there is a new region Period with a single-state timed automaton for each of the periodic regions. In each tick the clock creaches its period’s threshold, the clock is reset and tick is set to true, enabling the reaction in the region that now holds the user-specified behavior. Otherwise, represented by the transition with the lower priority (2:), the variable is set to false. By introducing the clock directly at the level of the period directive, the guarded state or region is only activated if the given amount of time has passed since the entering/start of the state/region or its last activation. In the PendulumControl in Figure 4.8 this ensures that the blinking behavior is aligned with the activation of the Catch state (cf. Figure 3.1). Clock Relation Specification While the period directive is a simple way to achieve a form of multiclocking in SCCharts, it also sets a first cornerstone for future work toward polychrony and distributed execution [GG10]. There are some initial efforts to combine multiclocked SCCharts with the CCSL by André [And09] to establish a formal specification for the relation of clocks [SHM+20]. CCSL was also used for the specification and validation of timing requirements in Esterel [AM09] and the simulation and debugging of LF programs [DCB+21]. Section 6.3.2 will discuss this topic in more detail. 4.3 When to React? Timed automata use timing constraints on transitions and real-valued clocks to express timed behavior. It is clear that if a constraint is not met, the transition must not be taken. However, when the constraint is satisfied, 124 4.3. When to React? 0 I0O0 tl I1O1I2O2 1 2 (a) Logical time: time is discretized into logical ticks 0, 1, etc. Input Ii is synchronous with output Oi , the reaction time is abstracted to be 0. w0 = 0 I0O0 t[μsec] w1 = 100 w2 = 200 tick() I1O1 tick() I2O2 tick() c0c1c2 (b) Physical time: the computation of the i -th reaction, corresponding to logical tick i and the i -th call of the tick function, begins at wake-up time wi . Inputs are read at the beginning of the computation, outputs are written at the end of the computation. Figure 4.10. Different timing abstractions [HBG17]. (©2017 IEEE) the automaton can react. Section 4.2.1 presented the eager semantics that tightens this specification such that the automaton should react as soon as possible. While in a theoretical model, it is possible to react at any time and perfectly meet this semantics, in reality, an execution regime can only approximate the eager semantics. The same holds for the abstraction of time in synchronous languages. Under the synchrony hypothesis a reaction does not take time and the program runs in logical time steps, as illustrated in Figure 4.10a. However, in practice a tick takes time to compute ( ci ) which create a temporal separation between inputs and outputs, as in Figure 4.10b. Additionally, the tick computations must not overlap because the synchronous program must be able to atomically access its internal state and prepare it for the subsequent execution. Furthermore, the question of when an automaton should react is not restricted to this “timed” setting. Instead, it is relevant to synchronous programming in general. While LF comes with its own event-driven execution environment, classical synchronous languages, such as SCCharts, synthesize a tick function (Section 2.3.2), which puts the invocation of ticks into the hands of the tick environment. And, as already discussed in Section 4.2.1, this can have implications on the final behavior of the model. Hence, a more thorough investigation of different execution strategies is necessary to determine drawbacks and limitation. The goal is to identify a 125 4. Time Environment Sensors Tick Function (Automaton) Inputs Outputs sleepTdeltaT Event Trigger Time Trigger Trigger Unit Actuators Tick Time Manager Figure 4.13. A dynamic tick function and its environment. Components in red are new compared to Figure 2.5. (Publ. in [SHM+18; SHM+20] ©2018 IEEE) a relative notation with an input deltaT for passing the time elapsed since the last tick and a sleepT output to communicate the time until the next time-related reaction is expected. The new input and output simply extend the environment of the tick function. A Time Manager is responsible for providing time and triggering a tick when the requested sleep time expired. The triggering by events remains the same, as previously discussed. The conservative nature of this extension shows that this structure is still fully within the standard synchronous execution model. The execution of the system is divided into logical ticks, which read inputs and produces outputs. Conceptually, deltaT is an input like any other input, and sleepT is an output like any other output. It also upholds the general requirement of determinacy: given a trace of inputs (including deltaT), the output trace (including sleepT) is fully determined. Tick Loop Implementation While the basic design of the dynamic tick environment and its communication interface is clearly defined, its implementation depends on the platform and the specific use case. For example, it could use an interrupt routine for inputs or requires a special API for accessing time in a precise resolution. Listing 4.1 shows a fairly generic implementation for a dynamic tick loop. It picks up the example from Listing 2.1 and runs a version of the PendulumSound component with the dynamic ticks interface, which is the 132 4.4. Dynamic Ticks in SCCharts 1#include "PendulumSound.h" 2#include "HardwareMockup.h" 3int main(int argc, const char*argv[]) { 4TickData model; 5reset(&model); 6 7double last_tick = curr_time(); 8while (1) { 9double tick_start = curr_time(); 10 model.deltaT = tick_start -last_tick; 11 model.theta = read_from("theta"); 12 tick(&model); 13 write_to("speaker", model.sound); 14 15 last_tick = tick_start; 16 double sleep = MAX(model.sleepT - (curr_time() -tick_start), 0); 17 awaitInputOrTimeout(sleep); 18 } 19 } Listing 4.1. Tick loop example for dynamic ticks. model described in Section 4.2.3 but compiled with the sleep time inference that will be introduced in Section 4.4.2. Compared to the previous no-delay version in Listing 2.1a, it implements a Time Manager and waits for triggering ticks instead of immediately starting the next. Before the start of the tick loop, the last_tick variable is declared in line 7 and initialized with the current time. Each tick execution begins with storing the start time (line 9). Then, the deltaT input is computed based on the time between the current and last tick. Afterwards, the program provides the remaining inputs, invokes the tick function, and processes the outputs. At the end of this tick computation, the start time of the current tick becomes the last tick time (line 15) and the sleep time is computed (line 16). The sleep time is based on the sleepT output but subtracts the execution time of the tick function. This compensates the fact that deltaT is a stable input for the synchronous tick function and consequently sleepT represents a sleep time relative to this point in time. A maximum function prevents negative sleep times. Alternatively, this step could raise a runtime error because a negative sleep time indicates that the program requires an execution pace that cannot be satisfied due to its own execution time. The awaitInputOrTimeout function can be considered an abstraction of a platform-specific interrupt and waiting routine. Here it is a blocking call that returns as soon as any input can be read from the hardware or the provided sleep time expires. Only then the loop repeats itself to execute the next tick. 133 4. Time Logical or Physical Time? LF uses a notion of time that includes a logical and physical timeline (or even multiple ones [LMS+20]). Events are processed in timestamp order and always on time w.r.t. to logical time, even if physically impossible. Physical time represents the wall clock time during execution and is always in advance of logical time (or equal to), potentially triggering deadlines if processing timeframes are violated. For example, if two events occur after each other but with a delay smaller than the execution time of the processing tick, it is impossible to process the second event at its physical time of occurrence. Furthermore, it is a property of the event-based processing with logical time that the program is able to recognize the event during execution, store it, and catch up on its processing. Sant’Anna et al. provide a detailed discussion on the consequences of different sampling strategies in the context of Céu [SIL+17]. Timed SCCharts neither rely on such an event-based semantics nor introduce an explicit separation between logical and physical time. The concept of dynamic ticks only relies on the time provided by the environment via deltaT. Hence, it is very well possible to create a tick environment that executes the SCChart with logical time, see Section 4.5.3, by hiding the natural execution lag from the program. This would keep the program in a “perfect world.” As a consequence, deltaT will always be equal to the previously requested sleepT, if input events are not interrupting. This perfectly simulates the eager semantics. However, dynamic ticks also work without this additional requirement on the environment. Listing 4.1 represents a tick environment with physical time input. In this example, the curr_time() function is supposed to directly access the system’s clock, also illustrated by the fact that it is used to determine the execution time of the tick function in line 16. This approach can be very valuable for a modeler, as it implicitly communicates physical lag to the program and enables an adjustment of the behavior. For example, a model can measure its own execution time and modify its workload, enter a “degraded” mode if timing overruns occur, or even maintain a local logical timeline. Section 4.4.3 will discuss modeling options in timed SCCharts that deal with the exposure to a physical time input. 134 4.4. Dynamic Ticks in SCCharts TimedTrafficLight input signalpedestrian input float deltaT = 0.0 output signal sigR, sigG, sigY output float sleepT = 0.0 float x = 0 immediate during/ sleepT = 1000.0 red during / x += deltaT immediate duringx < 60.0 / sleepT min= 6.0 - x green during / x += deltaT pending during / x += deltaT immediate duringx < 60.0 / sleepT min= 6.0 - x yellow during / x += deltaT immediate duringx < 5.0 / sleepT min= 3.0 - x x >= 60 / sigG; x = 0 1: pedestrian && x < 60 2: pedestrian && x >= 60 / sigY; x = 0 x >= 60 / sigY; x = 0 x >= 5 / sigR; x = 0 - Figure 4.14. The traffic light controller SCChart after the non-concurrent clock transformation producing dynamic ticks. (Publ. in [SHM+18; SHM+20] ©2018 IEEE) 4.4.2 Sleep Time Inference from Timed Automata An SCChart is compatible to dynamic ticks as soon as it provides the specified interface. Of course these variables can be used to manually track time and compute sleep times, but the notation of timed automata in SCChart offers a more elegant way to automatically infer sleep times. As presented in Section 4.2.2, the transformation of timed automata in SCCharts already relies on a time input named deltaT and thus is in accordance to the dynamic tick interface. The same transformation can be configured to additionally produce an overall sleep time for the model. 135 4. Time Transformation Figure 4.14 shows the traffic light controller example in its transformed state (based on Figure 4.4) with full support for dynamic ticks. The SCChart now declares the additional output sleepT. Additionally, the root state contains an immediate during action that initializes the sleep time to 1000. This presumably large default value is simply denotes that there is no active timeout and could be just as well infinity. The transformation can be configured to use different default values. Afterwards, the value of sleepT is updated by the states requesting an earlier wake-up time. Each state that has transitions with a trigger involving a clock-based guard creates an immediate during action for each constraint (state green is special case discussed later). If the timing condition can be met in the future (e.g., x < 60.0 for the x >= 60 transition of state red), it registers the remaining time for the trigger point of the guard (consequently, 60.0 - x) in sleepT. The min= is an update assignment that sets sleepT to the minimum of its current value and the right-hand side expression. The result is a consensus of all active time-related guards on the closest relevant triggering time. The specifics of the sleep time calculation will be discussed later. With the provided sleep times and a dynamic tick environment, the model will now behave as illustrated in Figure 4.11f and comply with the eager semantics. The program reacts to the pedestrian input at time 40, but the state of the automaton does not change. However, as illustrated by deltaT and sleepT presented under the timeline, the dynamic ticks adapt to the input-triggered invocation and correctly compute a new sleep time of 20. After the output of sigG at time 60, no timing constraint is available. Hence, the model has to rely on inputs for triggering and defaults to 1000 in sleepT. The trace further shows that the reaction to the pedestrian event at 122.2 is likewise on time, and the output of sigR is exactly 5 sec after this event. How to Compute Sleep Times The main task in computing automatic sleep times is to detect if and which passage of time causes a transition to be enabled in the future. The transformation uses a static analysis of the timing bounds in the outgoing transitions of states for this task. In order to facilitate its implementation, it is subject to certain restrictions in the timing constraint specification. More specifically, it considers timing constraints if the form cěltb , where c is a clock and ltb some expression 136 4.4. Dynamic Ticks in SCCharts for a lower timing bound. As illustrated in Figure 4.14, the difference between ltb and the current clock value determines the requested sleep time for this constraint (e.g., sleepT min= 60.0 - x). To simplify the detection of lower timing bounds, the implementation does not handle negations of timing constraints. 6 Furthermore, constraints that specify an upper bound do not contribute to the sleep time since they, considered separately, do not require time to pass to be enabled and hence would result in a sleep time of zero. Another case in which the passage of time has no triggering effect, despite the presence of a timed guard, can be found in the green state of Figure 4.14. Here, both outgoing transitions primarily depend on the pedestrian input, and xonly distinguishes which of the two paths is taken. To detect such non-triggering timing constraints, assume that the i -th outgoing transition of some state has a guard Gi=Ci^Ti , where Ci is a condition that does not depend on time and Ti is a timing constraint. Assume that no guard is currently active, i.e., ⋁︁iGi=false , and that T1 specifies a lower timing bound ltb . If Di such that C1 implies Ci and ␣T1 implies Ti (i.e., whenever the ltb has not been reached yet, Ti holds), T1 is considered nontriggering. This will prevent a contribution to the sleep time computation. The implementation further simplifies this condition and assumes that C1 and Ci are the same boolean guard, and T1 and Ti are negations of each other. In the example, the guards on the outgoing transitions from green fulfill that criterion. Taking pedestrian && x ą = 60 for C1 and pedestrian && x ă 60 for C2 , the compiler classifies 60 to be a non-triggering ltb and does not compute a sleep time for it. Timing Bounds The concept of computing sleep times based on lower bounds is closely tied to the eager semantics. In a perfectly eager execution, it would be sufficient to write xě60 as x=60 . However, considering realvalued time and a realistic implementation with physical time and possible timer imperfections, the first option is more robust and thus preferable. The following section will take a closer look at handling such imperfections. Open timing intervals, specified via ą , are not supported by the proposed concept because they would imply a request for an infinitesimally 6 Note that this simplification does not limit expressiveness, as for example, !(x ă 10) can be written as xě10. 137 4. Time larger sleep time in a real-valued time domain, while in an integer-based time representation, it would be trivial to express the same timing bound in the ěnotation. 4.4.3 Dealing with Physical Time As already discussed, dynamic ticks can be operated in an environment with logical or physical time inputs. While logical time ensures a perfect eager semantics, physical time might be preferable in cases where the program should be able to detect timing imperfections and adjust the behavior of the system from within the model. In LF, watchdogs and deadlines provide such means to react to a deviation between logical and physical time. Yet, LF’s notion of physical time is slightly different from the physical time input discussed here in the context of SCCharts, since physical time continues to progress during execution of an LF program. In contrast to that, the deltaT input in SCCharts is held stable during execution, even if determined based on physical time. With timed SCCharts exposed to physical time, this raises the question: Can we react in time? If, for example, more time than the minimum of a specified lower bound passes, it is possible that other transitions also get enabled or disabled, which may change the expected behavior. Assume the example that a state is entered when at least 60 sec passed ( xě60 ) and is immediately (in the same tick) left when at most 80 sec have passed ( xă80 ), without any reset of the clock. With eager semantics, the state will be entered after a time of 60 and then left immediately. If the tick is delayed due to physical lag, for example to react after a time of 80 for the first time, then the state is entered but can never be left. One could argue such a system is designed badly and advocate the use of logical time to perfectly match the eager semantics. Alternatively, one could consider this design a deliberate expression of a deadline. Specifically, if the execution environment approximating the eager semantics in the real world fails to meet the 60 sec trigger point by an additional margin of 20 sec, the system must not advance to the next state. Section 4.5.3 will discuss a similar model. 138 4.4. Dynamic Ticks in SCCharts FastAndSlow clock x = 0 x >= 333 / x = 0 -Fast clock x = 0 x >= 1000 / x = 0 -Slow (a) SCChart motivating the use of soft bounds. FastAndSlowGreedy clock x = 0 x >= 333 / x = 0 -Fast clock x = 0 x >= 999 || x >= 1000 / x = 0 -Slow (b) SCChart using soft bounds in the trigger in region Slow. FastAndSlowGreedy input int deltaT = 0 output int sleepT = 0 int _region_Fast_x = 0 int _region_Slow_x = 0 immediate during / sleepT = 1000 during / _region_Fast_x += deltaT immediate during _region_Fast_x < 333 / sleepT min= 333 - _region_Fast_x _region_Fast_x >= 333 / _region_Fast_x = 0 -Fast during / _region_Slow_x += deltaT immediate during _region_Slow_x < 1000 / sleepT min= 1000 - _region_Slow_x _region_Slow_x >= 999 || _region_Slow_x >= 1000 / _region_Slow_x = 0 -Slow (c) Transformed SCChart with soft bounds Figure 4.15. Motivating example for using soft bounds in dynamic ticks. (Publ. in [SHM+20]) In addition to such modeling options, timed SCCharts provide strategies and language constructs to deal with physical delays in timing bounds and on clocks. This enables the user to create models that yield a more robust and desirable behavior in a realistic physical environment. 139 4. Time Hard vs. Soft Bounds—A Greedy Semantics An eager execution will always try to react to inputs on time. However, if two events (input or time) occur so close that their separating time falls below the execution time of the tick function, the second event can only be processed with inevitable physical delay. Since timed SCCharts are not strictly bound to an event-based processing in logical time as LF, they provide the concept of soft bounds to handle such situation differently. The soft approach loosens the regime of the eager semantics and leads to a greedy semantics. Figure 4.15a illustrates a minimal SCCharts example to motivate soft bounds. The SCChart has two regions Fast and Slow, each one uses a timed automaton to react. Every time its threshold is reached, it resets its clock. The SCChart uses an implicit time resolution in microseconds. Hence, Slow should react every millisecond and Fast three times faster. Starting at time zero, the third reaction of region Fast will be at 999 usec, leaving only one microsecond to invoke the reaction of Slow, which might be infeasible for the environment. With soft bounds such short sleep times can be avoided. The idea is to widen the timed reaction window of a transition, speculating to possibly “piggyback” on a somewhat earlier reaction invoked by another state. At the same time, the transition should still request its own sleep time to ensure that it is triggered. In timed SCCharts, the modeler may replace the hard bound x ě 1000 in region Slow by a soft bound x ě 999 || x ě 1000, as illustrated in Figure 4.15b. If enabled, the compiler detects this pattern and adjusts the computed sleep time, as presented in Figure 4.15c. The state now only requests a sleep time of 1000 usec, as for the original hard bound specified with x ě 1000. However, at run time the transition may already be taken at time 999 usec, thus subsuming the sleep time of 1000 usec. This favors earlier reactions over late reactions, prevents very small sleep times, and possibly reduces the total number of reactions by processing assuredly delayed reactions ahead of time. Hard vs. Soft Resets—Handling Physical Lag in Clocks With physical time fed to deltaT, timer imperfections affect the clocks in SCCharts. Ticks executed before the requested sleep duration are normal in the presence of external input events. These do not affect the timed behavior since the 140 4.4. Dynamic Ticks in SCCharts FastAndSlowGreedySoftReset clock x = 0 x >= 333 / x -= 333 -Fast clock x = 0 x >= 999 || x >= 1000 / x = x - 1000 < 0 ? 0 : x - 1000 -Slow Figure 4.16. Variant of FastAndSlowGreedy SCChart using soft reset in both regions. (Publ. in [SHM+20]) clocks will register this intermediate time, compute a new sleep time, and related time constraints do yet not trigger. However, when a tick is executed after the requested sleep time, the additional delay time will be present in all clocks. This fact should be considered when performing a reset on a clock. Ahard reset sets the value of the clock to an absolute value, as presented in Figure 4.15. Alternatively, one can use a soft reset that takes into account the potential lag on a clock. Figure 4.16 shows a variant of the previously introduced FastAndSlowGreedy SCChart that uses soft resets in both regions. Each resets its clock xto the amount of time that exceeds the expected wake-up ( x´333 and x´1000 ). Due to the soft bounds in region Slow, it is legal to take this transition with 999 usec, which would result in a negative clock value. Therefore, the maximum of 0 and x´1000 is used to assign x. A consequence of hard resets is that clocks start to drift as soon as the tick function is invoked slower than the expected wake-up time. For example, if region Fast in Figure 4.15b wakes up at 335 usec, it would reset the clock to 0 and request a sleep time of 333 usec, disregarding the 2 usec that additionally passed. Hence, the (earliest) next wake-up would be at 668 usec and this drift increases as the delays accumulate over time. This violates the set goal of temporal order and simultaneity. Soft resets compensate this accumulation of timer imperfections by leaving the lag on the clock and consequently include them in the sleep time computation. 141 6. Conclusions static analysis and compilation but also prevents passing around objects at runtime, which is quite common in general purpose OO languages. One direction for future work is to lift this restriction. Rust, discussed in Section 5.1.1, illustrates a model that uses reference lifetimes and ownership borrowing [Pea21] to address this issue statically. The same mechanism is used in Blech to restrict mutable references. With subtyping there is another dimension to this problem, since references can hold subtype objects that have different behavior, and might access data differently, affecting causality. Here SPs could be used to ensure a schedule independent of subtypes. A subtype object that is policy-coherenent to its supertype’s policy could be used as a replacement for its supertype without the need to adjust the policy-conformant scheduling. A detailed sketch of this approach can be found in the journal publication on OO in SCCharts [SSM21]. An alternative approach can be found in Céu, mentioned in Section 5.1.2, where concurrent intra-instant communication is prohibited and threads are scheduled in lexical order. While this can be considered a harsh restriction, the idea of adding constraints on concurrency can help in reducing the complexity of the problem of causality. For example, reactors have no shared state variables, only instantaneous events between reactors. The lean state-based compilation approach for SCCharts by Smyth [Smy21] uses a region-based scheduling granularity that limits interleaving and drops support for instantaneous back and forth communication, similar to LF. Behavioral Subtyping Section 5.3.3 presented different levels of subtype admissibility. While the proposed implementation with its white-box scheduling does not require extensive subtyping restrictions and explicitly refrains from creating built-in limitations for SCCharts that go beyond minimal type safety, it is certainly relevant to further investigate means to express advanced aspects of subtyping. As already mentioned, SPs can be used to retain a scheduling interface in the face of type inheritance. A more extensive approach comes in the form of behavioral subtyping. There is already research in the context of Harel’s OO statecharts [HK02; SSL19] that could be transferred to SCCharts. Lee and Xiong present a behavioral type system for component-based designs that uses extended interface 244 6.3. Future Work on SCCharts automata [LX04]. Furthermore, the existing model checking capabilities in SCCharts [Sta19] could be utilized to introduce preand post-conditions for methods and regions that must be fulfilled by subtype implementations. Formal Semantics While the focus of this thesis lies on language design and pragmatics-aware modeling with a proof of concept implementation, future research for OO in SCCharts may include formal models for the proposed concepts. This could involve a dedicated formalization of SCCharts themself because their current semantics is grounded via model transformations [Mot17] in the SC semantics of the SCG/SCL. Alternatively, the SC kernel language could be extended to capture aspects of OO. With the Sequentially Constructive Procedural Language (SCPL), Gretz et al. made a first step in this direction when they created an extension to formalize the semantics of Blech [GGM+20; GGM+22]. Furthermore, there is a detailed theory on type systems and subtyping [Pie02; Car88], as well as machine-checked proofs of type soundness in languages such as Java [KN06] and C++ [WNS+06], that could be adapted to express aspects of type inheritance in SCCharts. 6.3.5 Object-Oriented State-Based Code Generation Section 5.3 used a high-level transformation approach for the proposed OO features. In addition to that, the new OO features provide an opportunity to create dedicated OO code generation approaches that do not remove aspects of OO but transfer them into the host language, if supported. The state-based code generation approach for SCCharts [SMH18; Smy21] is particularly well suited for such a concept. It is designed to directly represent the stateful structure of SCCharts in code, e.g., by synthesizing regions and states into separate functions, and enumerations and switch statements to encode state machines. An OO state-based approach could modularize the code into separate classes and express instantiation and inheritance directly at this level. Listing 6.1 illustrates a mockup in Java using the CountingCounterApplication in Figure 5.4b and the CountingCounter in Figure 5.7a. Note that the code omits some aspects for brevity, such as the handling of region termination, which is irrelevant in this example, the transitions of the Wait and Reset states, and 245 6. Conclusions 1public class CountingCounterApplication { 2enum RegionApplicationStates { Wait, Reset } 3 4private CountingCounter counter; 5private RegionApplicationStates regionApplicationActiveState; 6 7public CountingCounterApplication() { 8reset(); 9} 10 11 public void reset() { 12 counter = new CountingCounter(); 13 regionApplicationActiveState = RegionApplicationStates.Wait; 14 } 15 public void tick() { 16 counter.regionCounting(); 17 regionApplication(); 18 } 19 20 private void regionApplication() { 21 switch (regionApplicationActiveState) { 22 case Wait: regionApplication_Wait(); break; 23 case Reset: regionApplication_Reset(); break; 24 } 25 } 26 private void regionApplication_Wait() { 27 // Check transition and set next state 28 } 29 private void regionApplication_Reset() { 30 // Check transition and set next state 31 } 32 } (a) CountingCounterApplication 1public class CountingCounter extends Counter { 2private boolean regionCountingDelayEnabled = false; 3 4public void reset() { 5value = 0; 6regionCountingDelayEnabled = false; 7} 8public void regionCounting() { 9regionCounting_Counting(); 10 } 11 private void regionCounting_Counting() { 12 if (regionCountingDelayEnabled) { 13 increment(); 14 } 15 regionCountingDelayEnabled = true; 16 } 17 } (b) CountingCounter 1public class Counter { 2protected int value = 0; 3 4public void increment() { 5value++; 6} 7public void decrement() { 8value--; 9} 10 public int getValue() { 11 return value; 12 } 13 } (c) Counter Listing 6.1. A mockup of the code structure generated by an OO state-based approach in Java for the CountingCounterApplication in Figure 5.4b and CountingCounter with inheritance. 246 6.3. Future Work on SCCharts optimizes the Counting region, which only has one state. In contrast to the object instantiation via macro expansion, discussed in Section 5.3.1, this approach keeps SCCharts-based classes as classes including their regions. This is the case for the CountingCounter in Listing 6.1b that, in this example, also utilizes Java’s inheritance mechanism to extend the Counter class in Listing 6.1c. The CountingCounter is then kept as an object reference in the CountingCounterApplication, see lines 4 and 12 of Listing 6.1a. The CountingCounterApplication as the main program provides a tick function interface that invokes the Counting regions of the counter in line 16 and the local Application region in line 17. This design follows the lean state-based approach that treats regions as atomic scheduling units. Additionally, it represents a refinement of the tick function modularity approach, proposed by Smyth [Smy21; Lüd21]. Assuming scheduling information about each region in an SCChart, e.g., in the form of an SP or a causality interface, the container SCChart could invoke regions individually and schedule its own regions in between. This would permit accepting more programs, since this approach is more fine-grained than the one invoking tick functions of submodules. Still, with regions as atomic scheduling units, the approach does not support interleaving of regions, which is required in the presence of instantaneous back and forth communication. While this is a justified design decision for the lean state-based approach, it means that the given CountingCounterApplication SCChart cannot be compiled with this code generator. The IURP prescribes that reset must be scheduled before the increment in region Counting, while getValue must be ordered after this update, which is impossible if region Application is not split up into separate scheduling units. The code in Listing 6.1 actually assumes a CountingCounter with a custom update-before-reset scheduling, discussed in the context of clocks in Section 4.2.2. This allows and prescribes the scheduling of the Counting region (line 16) before the Application region (line 17). To mitigate such a limitation, future development could involve techniques to automatically divide regions into subunits that enable interleaved scheduling, e.g., by Pouzet and Raymond [PR10]. This would also benefit methods in SCCharts, which are limited in the same way. Without inlining, they need to scheduled atomically, which rules out interleaving at a statement level. 247 6. Conclusions 6.4 Closing Remarks This thesis discussed various aspects of language design for reactive systems and illustrated the proposed solutions directly in SCCharts and LF. Now that the contributions of my work have been presented and discussed, I would like to close this thesis with some personal remarks and observations adjacent to these topics. Section 2.5 already sketched the idea of pragmatics-aware modeling and automatically generated views. However, it deserves another mentioning that this approach is a significant factor in working with SCCharts and LF. Especially the interactivity plays a crucial role, and although the many figures in this thesis are a result of these diagrams, a written document cannot adequately convey the live experience. Moreover, the fact that this approach represents the model in both a textual notation, for editing, and a graphical notation, for perception with an adjustable degree of abstraction, is (for now) a rare characteristic by itself. This thesis capitalizes on the availability of this approach and uses the unique opportunity to set different emphases in the notations for defining and visualizing certain language constructs in SCCharts and LF. Fortunately, my work can build upon years of development from previous Ph.D. students that laid the foundations and provided the frameworks for automatic layout, diagram synthesis, and interactive visualization. Likewise, open source solutions, such as Xtext, are a cornerstone of tools such as KIELER or the LF editor. The combination of these technologies not only enables crafting useful tools but also allows rapid prototyping, which has proven itself valuable to me many times. When meeting with members of the LF team for the first time, we were able to quickly create the first diagrams and try out different graphical styles. Another aspect that I would like to emphasize is the fact that both LF and SCCharts (and KIELER in general) are developed and maintained as feature-rich and lasting tools, instead of being just disposable prototypes demonstrating a single concept. They are consistently reevaluated in terms of their user experience and are actively integrated in teaching and industrial collaboration. From my perspective, this has the benefit of providing a sense of lasting purpose, which motivates creating high quality and usable solutions. At the same time, it requires a lot of effort to orga248 6.4. Closing Remarks nize and maintain such projects. When I joined the KIELER team in 2013 in the context of my Bachelor’s thesis, it was already several years in use and had a large codebase. It always took a team effort to maintain and advance this project. And while such an endeavor provides valuable experiences in software engineering and project management, the time spent on maintaining and sometimes restructuring the codebase itself rarely directly results in academic publications on that particular topic. In my experience, it requires a careful balance between innovative research and maintenance of the surrounded tooling. Additionally, it relies on the endorsement and support from the academic advisory side, which I am glad to have received plentifully. While LF is a younger project compared to KIELER, it likewise carries the same aspiration for creating a lasting usable tool, maybe also in the spirit of its predecessor Ptolemy. Finally, I hope the concepts presented in this thesis provide a valuable perspective on the topic of language design and maybe inspire new or further refined approaches in the future. Equally, I hope that, also in the long run, the extensions to the LF and the SCCharts language will support users in modeling reactive systems. 249 Acknowledgments I want to thank my advisor, Reinhard von Hanxleden, for giving me the opportunity to write my thesis at his group and under his experienced supervision. Working with him on the subjects of this thesis and various topics beyond was a great and invaluable experience to me. I am very grateful for his support, his patience, and the freedom and trust he has given me. He has been a steady source of motivation and opportunities. My thanks also go to Michael Mendler for the productive and inspiring collaboration on various topics and papers. His knowledge and experience, especially in the field of synchronous semantics, always provided a valuable perspective and a great source of advice. I thank Edward A. Lee for welcoming me so warmly into the LF team. Working with him and such an international and global team was an honor. His expertise and openness helped me in learning the subtleties of LF and in contributing to it myself, ultimately resulting in this thesis covering research questions regarding both SCCharts and LF. In the LF team, my thanks go to Marten Lohstroh in particular. After our initial meeting at the FDL in Southampton, which was the birthplace of the first LF diagrams, he cordially integrated me into the team, resulting in many productive and interesting meetings, as well as a joint effort for the LF product. Likewise, I want to thank my colleagues and predecessors in the KIELER team. Their software and research on layout, pragmatics, and SCCharts laid the foundation for much of my work in this thesis. It was a great pleasure to be part of such a dedicated team. Special thanks go to my colleague, Steven Smyth, for the countless hours we spent together discussing ideas in front of whiteboards, collaborating on research, and programming for the KIELER project. Working with him will always remain a core memory of my time at the group. I would also like to thank Steven and Marten for their very valuable proofreading of my thesis. 251 Acknowledgments Furthermore, I thank my colleagues, friends, and family who accompanied me on my academic journey and helped me in keeping my personal life at balance. Finally, I would like to express my deepest thanks to my parents, Gudrun and Hans-Werner Schulz-Rosengarten. I will be forever grateful for their unlimited patience and unwavering support that made my academic endeavor and ultimately this thesis possible. 252 Bibliography [ABP+97] Charles André, Frédéric Boulanger, Marie-Agnès Péraldi, JeanPaul Rigault, and Guy Vidal-Naquet. “Objects and synchronous programming”. In: RAIRO-APII-JESA-Journal Europeen des Systemes Automatises 31.3 (1997), pp. 417–432. [Abr96] Jean-Raymond Abrial. “Steam-boiler control specification problem”. In: Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. Berlin, Heidelberg: Springer, 1996, pp. 500–509. isbn: 978-3-540-49566-6. doi: 10. 1007/BFb0027252. [ACH+95] Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The algorithmic analysis of hybrid systems”. In: Theoretical Computer Science 138.1 (1995), pp. 3–34. doi:10.1016/0304-3975(94)00202-T. [AD21] Joaquín Aguado and Alejandra Duenas. “Synchronised shared memory and model checking: a proof of concept”. In: 24th Forum on specification and Design Languages, FDL’21. Antibes, France: IEEE, Sept. 2021, pp. 01–08. doi: 10 . 1109 / FDL53530 . 2021 . 9568373. [AD94] Rajeev Alur and David L. Dill. “A theory of timed automata”. In: Theoretical Computer Science 126.2 (1994), pp. 183–235. doi: 10.1016/0304-3975(94)90010-8. [Ada16] AdaCore. High-integrity object-oriented programming in Ada, v1.4. Oct. 2016. url: https: //www.adacore.com/uploads/techPapers/ HighIntegrityAda.pdf. [Agh86] Gul Agha. “An overview of actor languages”. In: Proceedings of the 1986 SIGPLAN Workshop on Object-Oriented Programming, 253 Bibliography guages. POPL’90. San Francisco, California, USA: ACM, 1989, pp. 125–135. isbn: 0897913434. doi:10.1145/96709.96721. [CHP06] Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. “Mixing signals and modes in synchronous data-flow systems”. In: Proc. 6th ACM & IEEE International conference on Embedded software, EMSOFT 2006. Seoul, Korea: ACM, 2006, pp. 73–82. doi:10.1145/1176887.1176899. [CLB+19] Fabio Cremona, Marten Lohstroh, David Broman, Edward A Lee, Michael Masin, and Stavros Tripakis. “Hybrid cosimulation: it’s about time”. In: Software & Systems Modeling 18.3 (2019), pp. 1655–1679. doi:10.1007/s10270-017-0633-6. [CÖ14] Michele Colledanchise and Petter Ögren. “How behavior trees modularize robustness and safety in hybrid systems”. In: 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, Chicago, IL, USA, September 14-18, 2014. IEEE, 2014, pp. 1482–1488. doi:10.1109/IROS.2014.6942752. [CÖ17] Michele Colledanchise and Petter Ögren. Behavior trees in robotics and AI: an introduction. CRC Press, 2017. isbn: 9781-138-59373-2. doi:10.1201/9780429489105. [Coo09] William R. Cook. “On understanding data abstraction, revisited”. In: Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications. OOPSLA ’09. Orlando, Florida, USA: ACM, 2009, pp. 557–572. doi:10.1145/1640089.1640133. [CPP05] Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. “A conservative extension of synchronous data-flow with state machines”. In: Proc. of the 5th ACM International Conference On Embedded Software, EMSOFT 2005. Jersey City, NJ, USA: ACM, 2005, pp. 173–182. doi:10.1145/1086228.1086261. [CPP17] Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. “SCADE 6: A formal language for embedded critical software development (invited paper)”. In: 11th International Symposium on 260 Bibliography Theoretical Aspects of Software Engineering TASE. Sophia Antipolis, France, Sept. 2017, pp. 1–11. doi:10.1109/TASE.2017.8285623. [Cra07] Iain D. Craig. Object-oriented programming languages: interpretation. London: Springer-Verlag London, 2007. isbn: 978-1-84628773-2. doi:10.1007/978-1-84628-774-9. [CW85] Luca Cardelli and Peter Wegner. “On understanding types, data abstraction, and polymorphism”. In: ACM Computing Surveys 17.4 (Dec. 1985), pp. 471–523. doi:10.1145/6041.6042. [DCB+21] Julien Deantoni, João Cambeiro, Soroush Bateni, Shaokai Lin, and Marten Lohstroh. “Debugging and verification tools for Lingua Franca in Gemoc studio”. In: Proc. Forum on Specification and Design Languages, FDL’21, Antibes, France, September 8-10, 2021. IEEE, Sept. 2021, pp. 1–8. doi:10.1109/FDL53530.2021.9568383. [DDR04] Martin De Wulf, Laurent Doyen, and Jean-François Raskin. “Almost ASAP semantics: from timed models to timed implementations”. In: Hybrid Systems: Computation and Control. Berlin, Heidelberg: Springer, 2004, pp. 296–310. doi: 10.1007/9783-540-24743-2_20. [DO-11] DO-332. Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A. Standard. Washington, D.C., USA: Radio Technical Commission for Aeronautics, Dec. 2011. [DO-12] DO-178C. Software Considerations in Airborne Systems and Equipment Certification. Standard. Washington, D.C., USA: Radio Technical Commission for Aeronautics, Jan. 2012. [Dom18] Sören Domrös. “Moving model-driven engineering from Eclipse to web technologies”. Master’s thesis. Kiel University, Department of Computer Science, Nov. 2018. url: https://rtsys. informatik.uni-kiel.de/~biblio/downloads/theses/sdo-mt.pdf. [Dvo09] Daniel Dvorak. “NASA Study on Flight Software Complexity”. In: AIAA Infotech@Aerospace Conference. 2009. 261 Bibliography [DZK+02] Frank Dabek, Nickolai Zeldovich, Frans Kaashoek, David Mazières, and Robert Morris. “Event-driven programming for robust software”. In: Proceedings of the 10th Workshop on ACM SIGOPS European Workshop. EW 10. Saint-Emilion, France: ACM, 2002, pp. 186–189. isbn: 9781450378062. doi: 10.1145/1133373. 1133410. [EB10] Moritz Eysholdt and Heiko Behrens. “Xtext: implement your language faster than the quick and dirty way”. In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion. OOPSLA ’10. Reno/Tahoe, Nevada, USA, 2010, pp. 307–309. isbn: 9781450302401. doi:10.1145/1869542.1869625. [EH20] Stephen A. Edwards and John Hui. “The sparse synchronous model”. In: Proc. Forum on Specification and Design Languages (FDL’20). Kiel, Germany, Sept. 2020. doi: 10. 1109 / FDL50818 . 2020. 9232938. [EJL+03] Johan Eker, Jörn W. Janneck, Edward A. Lee, Jie Liu, Xiaojun Liu, Jozsef Ludvig, Stephen Neuendorffer, Sonia Sachs, and Yuhong Xiong. “Taming heterogeneity—the Ptolemy approach”. In: Proceedings of the IEEE 91.1 (Jan. 2003), pp. 127–144. issn: 0018-9219. doi:10.1109/JPROC.2002.805829. [EL07] S. A. Edwards and E. A. Lee. “The case for the Precision Timed (PRET) machine”. In: Proceedings of the 44th Design Automation Conference. DAC ’07. San Diego, CA, USA: ACM, June 2007, pp. 264–265. doi:10.1145/1278480.1278545. [ELM+12] John Eidson, Edward A. Lee, Slobodan Matic, Sanjit Seshia, and Jia Zou. “Distributed real-time software for cyber-physical systems”. In: Proceedings of the IEEE 100.1 (Jan. 2012), pp. 45–59. doi:10.1109/JPROC.2011.2161237. [Ess96] Robert Esser. An Object Oriented Petri Net Approach to Embedded System Design. Dissertation. Eidgenössische Technische Hochschule [ETH] Zürich, 1996. 262 Bibliography [Eum20] Philip Eumann. “Model-based debugging”. Master’s thesis. Kiel University, Department of Computer Science, June 2020. url: https://rtsys.informatik.unikiel.de/~biblio/downloads/theses/ peu-mt.pdf. [FH10] Hauke Fuhrmann and Reinhard von Hanxleden. “Taming graphical modeling”. In: Proceedings of the ACM/IEEE 13th International Conference on Model Driven Engineering Languages and Systems (MoDELS ’10). Vol. 6394. Lecture Notes in Computer Science. Springer, Oct. 2010, pp. 196–210. doi: 10.1007/978-3-64216145-2. [FYK92] Katsuhisa Furuta, M. Yamakita, and S. Kobayashi. “Swing-up control of inverted pendulum using pseudo-state feedback”. In: Proceedings of the Institution of Mechanical Engineers, Part I: Journal of Systems and Control Engineering 206.4 (1992), pp. 263– 269. doi:10.1243/PIME_PROC_1992_206_341_02. [GG10] Abdoulaye Gamatié and Thierry Gautier. “The signal synchronous multiclock approach to the design of distributed embedded systems”. In: IEEE Trans. Parallel Distributed Syst. 21.5 (2010), pp. 641–657. doi:10.1109/TPDS.2009.125. [GG18] Friedrich Gretz and Franz-Josef Grosch. “Blech, imperative synchronous programming!” In: Proc. Forum on Specification Design Languages (FDL’18). Sept. 2018, pp. 5–16. doi: 10.1109/FDL. 2018.8524036. [GGB+91] Paul Le Guernic, Thierry Goutier, Michel Le Borgne, and Claude Le Maire. “Programming real time applications with SIGNAL”. In: Proceedings of the IEEE 79.9 (Sept. 1991), pp. 1321– 1336. doi:10.1109/5.97301. [GGM+20] Friedrich Gretz, Franz-Josef Grosch, Michael Mendler, and Stephan Scheele. “Synchronized shared memory and procedural abstraction: towards a formal semantics of Blech”. In: Proc. Forum on Specification and Design Languages (FDL’20). Kiel, Germany, Sept. 2020. doi:10.1109/FDL50818.2020.9232942. 263 Bibliography [GGM+22] Friedrich Gretz, Franz-Josef Grosch, Michael Mendler, and Stephan Scheele. “Synchronized shared memory and blackbox procedural abstraction: towards a formal semantics of Blech”. In: ACM Transactions on Embedded Computing Systems (Nov. 2022). Just Accepted. doi:10.1145/3571585. [GHJ+95] Erich Gamma, Richard Helm, Ralph Johnson, and John M. Vlissides. Design patterns: elements of reusable object-oriented software. Addison-Wesley, 1995. [GJS+15] James Gosling, Bill Joy, Guy Steele, Gilad Bracha, and Alex Buckley. The Java Language Specification. Java SE 8 Edition. Addison-Wesley Professional, 2015. [GM10] Maurizio Gabbrielli and Simone Martini. Programming languages: principles and paradigms. London: Springer-Verlag London, 2010. isbn: 978-1-84882-913-8. doi:10.1007/978-1-84882-914-5. [Gri19] Lena Grimm. “From Lustre to graphical dataflow programs”. Master’s thesis. Kiel University, Department of Computer Science, May 2019. url: https://rtsys.informatik.uni-kiel.de/~biblio/ downloads/theses/lgr-mt.pdf. [GSS+20] Lena Grimm, Steven Smyth, Alexander Schulz-Rosengarten, Reinhard von Hanxleden, and Marc Pouzet. “From Lustre to graphical models and SCCharts”. In: Proc. Forum on Specification and Design Languages (FDL ’20). Kiel, Germany, Sept. 2020. doi:10.1109/FDL50818.2020.9232944. [GSS+22] Lena Grimm, Steven Smyth, Alexander Schulz-Rosengarten, Reinhard von Hanxleden, and Marc Pouzet. “From Lustre to graphical models and SCCharts”. In: ACM Transactions on Embedded Computing Systems (July 2022). Just Accepted. doi: 10.1145/3544973. [GTL03] Paul Le Guernic, Jean-Pierre Talpin, and Jean-Christophe Le Lann. “POLYCHRONY for system design”. In: Journal of Circuits, Systems, and Computers 12.3 (2003), pp. 261–304. doi: 10.1142/S0218126603000763. 264 Bibliography [Gur99] Corin A. Gurr. “Effective diagrammatic communication: syntactic, semantic and pragmatic issues”. In: Journal of Visual Languages & Computing 10.4 (1999), pp. 317–342. doi: 10.1006/jvlc. 1999.0130. [Hal93] Nicolas Halbwachs. Synchronous programming of reactive systems. Kluwer Academic Publishers, 1993. doi:10.1007/978-1-4757-2231-4. [Han09] Reinhard von Hanxleden. “SyncCharts in C—a proposal for light-weight, deterministic concurrency”. In: Proceedings of the 9th ACM & IEEE International conference on Embedded software (EMSOFT’09). Grenoble, France: ACM, Oct. 2009, pp. 225–234. doi:10.1145/1629335.1629366. [Har87] David Harel. “Statecharts: A visual formalism for complex systems”. In: Science of Computer Programming 8.3 (June 1987), pp. 231–274. doi:10.1016/0167-6423(87)90035-9. [HBG17] Reinhard von Hanxleden, Timothy Bourke, and Alain Girault. “Real-time ticks for synchronous programming”. In: Proc. Forum on Specification and Design Languages (FDL ’17). Verona, Italy: IEEE, Sept. 2017, pp. 1–8. doi:10.1109/FDL.2017.8303893. [HCR+91] Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. “The synchronous data flow programming language LUSTRE”. In: Proceedings of the IEEE 79.9 (Sept. 1991), pp. 1305– 1320. doi:10.1109/5.97300. [HDM+13] Reinhard von Hanxleden, Björn Duderstadt, Christian Motika, Steven Smyth, Michael Mendler, Joaquín Aguado, Stephen Mercer, and Owen O’Brien. SCCharts: Sequentially Constructive Statecharts for safety-critical applications. Technical Report 1311. ISSN 2192-6247. Kiel University, Department of Computer Science, Dec. 2013. [HDM+14] Reinhard von Hanxleden, Björn Duderstadt, Christian Motika, Steven Smyth, Michael Mendler, Joaquín Aguado, Stephen Mercer, and Owen O’Brien. “SCCharts: Sequentially Constructive Statecharts for safety-critical applications”. In: Proc. ACM 265 Bibliography SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14). Edinburgh, UK: ACM, June 2014, pp. 372– 383. doi:10.1145/2594291.2594310. [HE22] John Hui and Stephen A. Edwards. “The sparse synchronous model on real hardware”. In: ACM Transactions on Embedded Computing Systems (Dec. 2022). Just Accepted. doi: 10.1145/3572920 . [Hew77] Carl Hewitt. “Viewing control structures as patterns of passing messages”. In: Artificial Intelligence 8.3 (1977), pp. 323–364. doi: 10.1016/0004-3702(77)90033-9. [HG96] David Harel and Eran Gery. “Executable object modeling with statecharts”. In: Proceedings of the 18th International Conference on Software Engineering. ICSE ’96. Berlin, Germany: IEEE Computer Society, 1996, pp. 246–257. isbn: 0-8186-7246-3. doi: 10.1109/2.596624. [HHK03] Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch. “Giotto: a time-triggered language for embedded programming”. In: Proceedings of the IEEE 91.1 (2003), pp. 84– 99. doi:10.1109/JPROC.2002.805825. [HHN01] Michael Hanus, Frank Huch, and Philipp Niederau. “ObjectCurry: an object-oriented extension of the declarative multiparadigm language Curry”. In: Implementation of Functional Languages, 12th International Workshop, IFL 2000, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2001, pp. 89– 106. doi:10.1007/3-540-45361-X_6. [HK02] David Harel and Orna Kupferman. “On object systems and behavioral inheritance”. In: IEEE Transactions on Software Engineering 28.9 (2002), pp. 889–903. doi:10.1109/TSE.2002.1033228. [HK04] David Harel and Hillel Kugler. “The Rhapsody semantics of Statecharts (or, on the executable core of the UML)”. In: Integration of Software Specification Techniques for Applications in Engineering: Priority Program SoftSpez of the German Research Foundation (DFG), Final Report. Vol. 3147. Lecture Notes in 266 Bibliography Computer Science. Berlin, Heidelberg: Springer, 2004, pp. 325– 354. isbn: 978-3-540-27863-4. doi:10.1007/978-3-540-27863-4_19. [HLF+22] Reinhard von Hanxleden, Edward A. Lee, Hauke Fuhrmann, Alexander Schulz-Rosengarten, Sören Domrös, Marten Lohstroh, Soroush Bateni, and Christian Menard. “Pragmatics twelve years later: a report on Lingua Franca”. In: 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). Vol. 13702. Lecture Notes in Computer Science. Springer. Rhodes, Greece, Oct. 2022, pp. 60–89. doi:10.1007/978-3-031-19756-7_5. [HN96] David Harel and Amnon Naamad. “The STATEMATE semantics of statecharts”. In: ACM Transactions on Software Engineering and Methodology 5.4 (Oct. 1996), pp. 293–333. doi: 10.1145/235321. 235322. [HNS+94] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. “Symbolic model checking for real-time systems”. In: Information and Computation 111.2 (1994), pp. 193–244. issn: 0890-5401. doi:10.1006/inco.1994.1045. [HP85] David Harel and Amir Pnueli. “On the development of reactive systems”. In: Logics and models of concurrent systems. NATO ASI Series 13 (1985), pp. 477–498. doi:10.1007/978-3-642-82453-1_17. [HPB+99] Olivier Hainque, Laurent Pautet, Yann Le Biannic, and Eric Nassor. “Cronos: a separate compilation toolset for modular Esterel applications”. In: World Congress on Formal Methods. Vol. 1709. Lecture Notes in Computer Science. Springer, Sept. 1999, pp. 1836–1853. doi:10.1007/3-540-48118-4_47. [HR04] Grégoire Hamon and John Rushby. “An operational semantics for Stateflow”. In: Fundamental Approaches to Software Engineering (FASE). Vol. 2984. Lecture Notes in Computer Science. Barcelona, Spain: Springer, Apr. 2004, pp. 229–243. doi: 10.1007/978-3-540-24721-0_17. 267 Bibliography [ISO12] ISO/IEC 8652:2012. Information technology — Programming languages — Ada. Standard. Geneva, Switzerland: International Organization for Standardization, Dec. 2012. [ISO18] ISO 26262-6:2018. Road vehicles — Functional safety — Part 6: Product development at the software level. Standard. Geneva, Switzerland: International Organization for Standardization, Dec. 2018. [ISO20] ISO/IEC 14882:2020. Programming languages — C++. Standard. Geneva, Switzerland: International Organization for Standardization, Dec. 2020. [JJK+17] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. “RustBelt: securing the foundations of the Rust programming language”. In: Proceedings of the ACM on Programming Languages (POPL’18) (Dec. 2017). doi:10.1145/3158154. [JMO93] Martin Jourdan, Florence Maraninchi, and Alfredo Olivero. “Verifying quantitative real-time properties of synchronous programs”. In: Proc. Computer Aided Verification, 5th International Conference, CAV ’93. Vol. 697. Lecture Notes in Computer Science. Springer, 1993, pp. 347–358. doi:10.1007/3-540-56922-7_29. [Joh13] Gunnar Johannsen. “Hardwaresynthese aus SCCharts”. Master’s thesis. Kiel University, Department of Computer Science, Oct. 2013. url: https://rtsys.informatik.uni-kiel.de/~biblio/ downloads/theses/gjo-mt.pdf. [KHA17] Roland Kuhn, Brian Hanafee, and Jamie Allen. Reactive design patterns. Manning Publications Company, 2017. [KN06] Gerwin Klein and Tobias Nipkow. “A machine-checked model for a Java-like language, virtual machine, and compiler”. In: ACM Transactions on Programming Languages and Systems 28.4 (July 2006), pp. 619–695. issn: 0164-0925. doi: 10.1145/ 1146809 . 1146811. [Kod20] Jeffrey Kodosky. “Labview”. In: Proceedings of the ACM on Programming Languages (June 2020). doi:10.1145/3386328. 268 Bibliography [KS08] Hannes Kegel and Friedrich Steimann. “Systematically refactoring inheritance to delegation in Java”. In: Proceedings of the 30th International Conference on Software Engineering (ICSE’08). New York, NY, USA: ACM, 2008, pp. 138–146. [KS12] Christoph M. Kirsch and Ana Sokolova. “The logical execution time paradigm”. In: Advances in Real-Time Systems. Ed. by Samarjit Chakraborty and Jörg Eberspächer. Berlin, Heidelberg: Springer, 2012, pp. 103–120. isbn: 978-3-642-24349-3. doi: 10.1007/978-3-642-24349-3_5. [Lam78] Leslie Lamport. “Time, clocks, and the ordering of events in a distributed system”. In: Communications of the ACM 21.7 (July 1978), pp. 558–565. issn: 0001-0782. doi:10.1145/359545.359563. [LBL+21] Edward A. Lee, Soroush Bateni, Shaokai Lin, Marten Lohstroh, and Christian Menard. “Quantifying and generalizing the CAP theorem”. In: Computing Research Repository (CoRR) (Sept. 2021). doi:10.48550/arXiv.2109.07771. arXiv: 2109.07771. [LBL+23] Edward A. Lee, Soroush Bateni, Shaokai Lin, Marten Lohstroh, and Christian Menard. “Trading off consistency and availability in tiered heterogeneous distributed systems”. In: Intelligent Computing 2 (2023). doi:10.34133/icomputing.0013. [LBM+23] Marten Lohstroh, Soroush Bateni, Christian Menard, Alexander Schulz-Rosengarten, Jeronimo Castrillon, and Edward A. Lee. “Deterministic coordination across multiple timelines”. In: ACM Transactions on Embedded Computing Systems (Oct. 2023). Just Accepted. doi:10.1145/3615357. [Lee03] Edward A. Lee. Model-driven development – From object-oriented design to actor-oriented design. Extended abstract of an invited presentation at Workshop on Software Engineering for Embedded Systems: From Requirements to Implementation (a.k.a. The Monterey Workshop), Chicago. Sept. 2003. [Lee06] Edward A. Lee. “The problem with threads”. In: IEEE Computer 39.5 (2006), pp. 33–42. doi:10.1109/MC.2006.180. 269 Bibliography [RSM+15] Karsten Rathlev, Steven Smyth, Christian Motika, Reinhard von Hanxleden, and Michael Mendler. “SCEst: Sequentially Constructive Esterel”. In: Proceedings of the 13th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE ’15). Austin, TX, USA, Sept. 2015. doi: 10.1109/MEMCOD.2015.7340462. [RV98] Didier Rémy and Jérôme Vouillon. “Objective ML: an effective object-oriented extension to ML”. In: Theory and Practice of Object Systems 4.1 (1998), pp. 27–50. doi: 10.1002/(SICI)1096-9942(1998) 4:1%3C27::AID-TAPO3%3E3.0.CO;2-4. [RWB16] Raymond Roestenburg, Rob Williams, and Robertus Bakker. Akka in action. Manning Publications Company, 2016. [Sam08] Miro Samek. Practical UML Statecharts in C/C++: event-driven programming for embedded systems. CRC Press, 2008. [San18] Francisco Sant’Anna. “Structured synchronous reactive programming for game development - case study: on rewriting Pingus from C++ to Céu”. In: 17th Brazilian Symposium on Computer Games and Digital Entertainment (SBGames 2018). IEEE Computer Society, 2018, pp. 240–249. doi: 10.1109/SBGAMES.2018.00036 . [Sch10] Klaus Schneider. The synchronous programming language Quartz. Internal Report. Kaiserslautern, Germany: Department of Computer Science, University of Kaiserslautern, 2010. [Sel93] Bran Selic. “An efficient object-oriented variation of the Statecharts formalism for distributed real-time systems”. In: Proceedings of the 11th IFIP WG10.2 International Conference Sponsored by IFIP WG10.2 and in Cooperation with IEEE COMPSOC on Computer Hardware Description Languages and Their Applications (CHDL ’93). Vol. A-32. IFIP Transactions. NLD: NorthHolland Publishing Co., 1993, pp. 335–344. isbn: 0444816410. doi:10.1016/B978-0-444-81641-2.50030-7. 276 Bibliography [SFR97] Manas Saksena, Paul Freedman, and Pawel Rodziewicz. “Guidelines for automated implementation of executable object oriented models for real-time embedded control systems”. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS’97). IEEE, 1997, pp. 240–251. doi:10.1109/REAL.1997.641286. [SGA+17] Aminata Sabané, Yann-Gaël Guéhéneuc, Venera Arnaoudova, and Giuliano Antoniol. “Fragile base-class problem, problem?” In: Empirical Software Engineering 22.5 (Oct. 2017), pp. 2612– 2657. doi:10.1007/s10664-016-9448-2. [SGW94] Bran Selic, Garth Gullekson, and Paul T. Ward. Real-Time Object-Oriented Modeling. John Wiley & Sons, 1994. isbn: 0471-59917-4. [SHL+23a] Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Marten Lohstroh, Soroush Bateni, and Edward A. Lee. “Modal reactors”. In: Computing Research Repository (CoRR) (Jan. 2023). doi:10.48550/ARXIV.2301.09597. arXiv: 2301.09597. [SHL+23b] Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Marten Lohstroh, Soroush Bateni, and Edward A. Lee. “Polyglot modal models through Lingua Franca”. In: Proc. Design, Automation & Test in Europe Conference & Exhibition, DATE 2023. Extended Abstract. Antwerp, Belgium: IEEE, 2023, pp. 1–2. doi:10.23919/DATE56975.2023.10136890. [SHL+23c] Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Marten Lohstroh, Edward A. Lee, and Soroush Bateni. “Polyglot modal models through Lingua Franca”. In: Proceedings of CyberPhysical Systems and Internet of Things Week 2023. CPS-IoT Week ’23. San Antonio, TX, USA: ACM, 2023, pp. 337–342. doi: 10. 1145/3576914.3587498. [SHM+18] Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Frédéric Mallet, Robert de Simone, and Julien Deantoni. “Time in SCCharts”. In: Proc. Forum on Specification and Design Languages (FDL ’18). Munich, Germany, Sept. 2018, pp. 5–16. doi: 10.1109/ FDL.2018.8524111. 277 Bibliography [SHM+20] Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Frédéric Mallet, Robert de Simone, and Julien Deantoni. “Time in SCCharts”. In: Languages, Design Methods, and Tools for Electronic System Design: Selected Contributions from FDL 2018. Ed. by Tom J. Kazmierski, Sebastian Steinhorst, and Daniel Große. Springer, 2020, pp. 1–25. isbn: 978-3-030-31585-6. doi: 10.1007/9783 - 030 - 31585 - 6 _1 . Reproduced with permission from Springer Nature. [SIL+17] Francisco Sant’Anna, Roberto Ierusalimschy, Noemi de La Rocque Rodriguez, Silvana Rossetto, and Adriano Branco. “The design and implementation of the synchronous language CÉU”. In: ACM Transactions on Embedded Computing Systems 16.4 (July 2017), 98:1–98:26. doi:10.1145/3035544. [SIL15] Francisco Sant’Anna, Roberto Ierusalimschy, and Noemi de La Rocque Rodriguez. “Structured synchronous reactive programming with Céu”. In: Proceedings of the 14th International Conference on Modularity, MODULARITY 2015. Fort Collins, CO, USA: ACM, 2015, pp. 29–40. doi:10.1145/2724525.2724571. [SL02] Stéphane S. Somé and Timothy C. Lethbridge. “Enhancing program comprehension with recovered state models”. In: Proceedings 10th International Workshop on Program Comprehension. IEEE, 2002, pp. 85–93. doi:10.1109/WPC.2002.1021325. [SMC95] Sowmitri Swamy, Arthur Molin, and Burton M. Covnot. “OOVHDL: object-oriented extensions to VHDL”. In: Computer 28.10 (1995), pp. 18–26. doi:10.1109/2.467587. [SMH18] Steven Smyth, Christian Motika, and Reinhard von Hanxleden. “Synthesizing manually verifiable code for statecharts”. In: Proc. Reactive and Event-based Languages & Systems (REBLS ’18), Workshop at the ACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH). Boston, MA, USA, Nov. 2018. doi: 10 . 1145 / 3281278 . 3281283. 278 Bibliography [SMR+17] Steven Smyth, Christian Motika, Karsten Rathlev, Reinhard von Hanxleden, and Michael Mendler. “SCEst: Sequentially Constructive Esterel”. In: ACM Transactions on Embedded Computing Systems—Special Issue on MEMOCODE 2015 17.2 (Dec. 2017), 33:1–33:26. doi:doi.org/10.1145/3063129. [SMS+15] Steven Smyth, Christian Motika, Alexander Schulz-Rosengarten, Nis Boerge Wechselberg, Carsten Sprung, and Reinhard von Hanxleden. SCCharts: the railway project report. Technical Report 1510. ISSN 2192-6247. Kiel University, Department of Computer Science, Aug. 2015. [Smy21] Steven Smyth. Interactive model-based compilation — a modellerdriven development approach. Kiel Computer Science Series 20 21/1. Dissertation. Kiel University, Faculty of Engineering. Department of Computer Science, 2021. doi:10.21941/kcss/2021/1. [Spi89] John Michael Spivey. Understanding Z - a specification language and its formal semantics (reprint). Vol. 3. Cambridge tracts in theoretical computer science. Cambridge University Press, 1989. isbn: 978-0-521-33429-7. [SQK18] Wasim Said, Jochen Quante, and Rainer Koschke. “On state machine mining from embedded control software”. In: 2018 IEEE International Conference on Software Maintenance and Evolution (ICSME). IEEE, 2018, pp. 138–148. doi: 10.1109/ICSME.2018.00024 . [SSH+18a] Alexander Schulz-Rosengarten, Steven Smyth, Reinhard von Hanxleden, and Michael Mendler. A sequentially constructive circuit semantics for Esterel. Technical Report 1801. ISSN 21926247. Kiel University, Department of Computer Science, Feb. 2018. [SSH+18b] Alexander Schulz-Rosengarten, Steven Smyth, Reinhard von Hanxleden, and Michael Mendler. “On reconciling concurrency, sequentiality and determinacy for reactive systems — a sequentially constructive circuit semantics for Esterel”. In: 18th International Conference on Application of Concurrency to System 279 Bibliography Design (ACSD’18). June 2018, pp. 95–104. doi: 10.1109/ACSD.2018. 00018. [SSH13] Christian Schneider, Miro Spönemann, and Reinhard von Hanxleden. “Just model! – Putting automatic synthesis of node-link-diagrams into practice”. In: Proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC ’13). San Jose, CA, USA: IEEE, Sept. 2013, pp. 75–82. doi:10.1109/VLHCC.2013.6645246. [SSH14] Christoph Daniel Schulze, Miro Spönemann, and Reinhard von Hanxleden. “Drawing layered graphs with port constraints”. In: Journal of Visual Languages and Computing, Special Issue on Diagram Aesthetics and Layout 25.2 (2014), pp. 89–106. issn: 1045-926X. doi:10.1016/j.jvlc.2013.11.005. [SSH18a] Steven Smyth, Alexander Schulz-Rosengarten, and Reinhard von Hanxleden. “Guidance in model-based compilations”. In: Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA ’18), Doctoral Symposium. Vol. 78. Electronic Communications of the EASST. Limassol, Cyprus, Nov. 2018. doi: 10.1007/978-3030-03418-4_15. [SSH18b] Steven Smyth, Alexander Schulz-Rosengarten, and Reinhard von Hanxleden. Practical causality handling for synchronous languages. Technical Report 1808. ISSN 2192-6247. Kiel University, Department of Computer Science, Dec. 2018. [SSH18c] Steven Smyth, Alexander Schulz-Rosengarten, and Reinhard von Hanxleden. “Towards interactive compilation models”. In: Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). Vol. 11244. Lecture Notes in Computer Science. Limassol, Cyprus: Springer, Nov. 2018, pp. 246–260. doi: 10.14279/tuj.eceasst. 78.1098. 280 Bibliography [SSH19] Steven Smyth, Alexander Schulz-Rosengarten, and Reinhard von Hanxleden. “Practical causality handling for synchronous languages”. In: Proc. Design, Automation and Test in Europe Conference (DATE ’19). Florence, Italy: IEEE, Mar. 2019. doi: 10.23919/DATE.2019.8715081. [SSL19] Eugene Syriani, Vasco Sousa, and Levi Lúcio. “Structure and behavior preserving statecharts refinements”. In: Science of Computer Programming 170 (2019), pp. 45–79. doi: 10.1016/j.scico. 2018.10.005. [SSM19] Alexander Schulz-Rosengarten, Steven Smyth, and Michael Mendler. “Towards object-oriented modeling in SCCharts”. In: Proc. Forum on Specification and Design Languages (FDL ’19). Southampton, UK, Sept. 2019, pp. 1–8. doi:10.1145/3453482. [SSM21] Alexander Schulz-Rosengarten, Steven Smyth, and Michael Mendler. “Toward object-oriented modeling in SCCharts”. In: ACM Transactions on Embedded Computing Systems 20.4 (May 2021). doi:10.1145/3453482. [Sta19] Andreas Stange. “Model checking for SCCharts”. Master’s thesis. Kiel University, Department of Computer Science, May 2019. url: https://rtsys.informatik.unikiel.de/~biblio/downloads/ theses/aas-mt.pdf. [STP05] Robert de Simone, Jean-Pierre Talpin, and Dumitru PotopButucaru. “The synchronous hypothesis and synchronous languages”. In: Embedded Systems Handbook. Ed. by Richard Zurawski. CRC Press, 2005. doi:10.1201/9781420038163.ch8. [Str87] Bjarne Stroustrup. “What is “Object-Oriented Programming”?” In: European Conference on Object-Oriented Programming (ECOOP’ 87). Vol. 276. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1987, pp. 51–70. doi:10.1007/3-540-47891-4_6. [TL18] Stavros Tripakis and Roberto Lublinerman. “Modular code generation from synchronous block diagrams: interfaces, abstraction, compositionality”. In: Principles of Modeling — Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday. 281 Bibliography Ed. by Marten Lohstroh, Patricia Derler, and Marjan Sirjani. Vol. 10760. Lecture Notes in Computer Science. Springer, 2018, pp. 449–477. doi:10.1007/978-3-319-95246-8_26. [TYN13] Ewan Tempero, Hong Yul Yang, and James Noble. “What programmers do with inheritance in java”. In: 27th European Conference on Object-Oriented Programming (ECOOP 2013). Ed. by Giuseppe Castagna. Vol. 7920. Lecture Notes in Computer Science. Montpellier, France: Springer, 2013, pp. 577–601. doi: 10.1007/978-3-642-39038-8\_24. [Weg87] Peter Wegner. “Dimensions of object-based language design”. In: Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications (OOPSLA ’87). Orlando, Florida, USA: ACM, 1987, pp. 168–182. doi:10.1145/38765.38823. [WHR14] Jon Whittle, John Hutchinson, and Mark Rouncefield. “The state of practice in model-driven engineering”. In: IEEE Software 31.3 (2014), pp. 79–85. doi:10.1109/MS.2013.65. [Wie98] Roel J. Wieringa. “A survey of structured and object-oriented software specification methods and techniques”. In: ACM Computing Surveys 30.4 (1998), pp. 459–527. doi:10.1145/299917.299919. [WNS+06] Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip. “An operational semantics and type safety proof for multiple inheritance in C++”. In: Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA ’06). Portland, Oregon, USA: ACM, 2006, pp. 345–362. doi:10.1145/1167473.1167503. [WSS+18] Nis Wechselberg, Alexander Schulz-Rosengarten, Steven Smyth, and Reinhard von Hanxleden. “Augmenting state models with data flow”. In: Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of his 60th Birthday. Ed. by Marten Lohstroh, Patricia Derler, and Marjan Sirjani. Vol. 10760. Lecture Notes in Computer Science. Springer, 2018, pp. 504–523. doi:10.1007/978-3-319-95246-8_28. 282 Bibliography [WSW+06] Ferdinand Wagner, Ruedi Schmuki, Peter Wolstenholme, and Thomas Wagner Thomas. Modeling software with finite state machines: a practical approach. Auerbach Publications, 2006. [ZCC97] Olivier Zendra, Dominique Colnet, and Suzanne Collin. “Efficient dynamic dispatch without virtual function tables: the SmallEiffel compiler”. In: Proceedings of the 12th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA ’97). Atlanta, Georgia, USA: ACM, 1997, pp. 125–141. doi:10.1145/263698.263728. [ZL08] Ye Zhou and Edward A. Lee. “Causality interfaces for actor networks”. In: ACM Transactions on Embedded Computing Systems 7.3 (Apr. 2008), 29:1–29:35. doi:10.1145/1347375.1347382. [ZLL07] Yang Zhao, Edward A. Lee, and Jie Liu. “A programming model for time-synchronized distributed real-time systems”. In: Real-Time and Embedded Technology and Applications Symposium (RTAS). IEEE, 2007, pp. 259–268. doi:10.1109/RTAS.2007.5. 283 Glossary ADT Abstract data type An abstract data type combines a named type with operations to create, combine, and observe values of that type [Coo09]. API Application programming interface A contract for communication or interaction between software components. ASAP As soon as possible A colloquial abbreviation. CCSL Clock Constraint Specification Language A notation to handle clocks and to specify logical and chronometric time constraints [And09]. CFG Control-flow Graph A directed graph notation in which nodes represent instructions or conditions and edges specify control-flow paths [All70]. CPS Cyber Physical System A system that contains behavior defined in both the cyber and the physical domain [LS17]. ELK Eclipse Layout Kernel A framework under the Eclipse umbrella that provides several layout algorithms, as well as the surrounding infrastructure. Available at: https://www.eclipse.org/elk FPGA Field Programmable Gate Array An integrated circuit that is designed to support configuration by a hardware description language after manufacturing. FSM Finite state machine A form of automaton that uses a finite number of states. 285 List of Figures 5.3 The CounterApplication SCChart using Counter class. . . . . . . 188 5.4 Example of an SCChart class with a region. . . . . . . . . . . . 190 5.5 First step in the high-level transformation of the CountingCounterApplication, replacing the SCCharts-based class by a native notation. ...............................191 5.6 Conceptualized second step in the high-level transformation of the CountingCounterApplication with method inlining and simplification of the class data structure. . . . . . . . . . . . . 192 5.7 Examples of inheritance and overriding in SCCharts-based classes. ................................193 5.8 Example for usage of inheritance and overriding (left) and the result after inheritance is statically expanded by the compiler (right). Red arrows indicate where the parts of the model are expandedinto.............................197 5.9 An SCChart with a type parameter for a Counter classes that is instantiated and used to count to ten. . . . . . . . . . . . . . 198 5.10 Screenshot of the ControlledCountingCounter in the KIELER tool...................................201 5.11 The CountingCounterApplication and the involved classes arranged in a UML class diagram style. . . . . . . . . . . . . . . . 202 5.12 Two variants of the CounterApplication using host code. . . . . 204 5.13 An attempt to model the Counter class as a reactor in LF. . . . 206 5.14 The CounterApplication with a host class and a custom schedule. The resulting scheduling instructions are visualized as green arrows.................................209 5.15 The CounterApplication with a host class and a policy automaton. The resulting scheduling instructions are visualized as greenarrows. ............................211 5.16 Logger example modelled using the classical module approach................................217 5.17 The PureSignal class modelled in SCCharts. . . . . . . . . . . . 219 5.18 The AbstractValuedSignal class that carries a generic value and requires the implementation of a combination function. . . . . 220 5.19 The PureSCSignal class extending pure signals by an unemit method with a custom scheduling protocol. . . . . . . . . . . . 222 292 List of Figures 5.20 The Counter class modelled as a classical SCCharts module with boolean variables for interaction. . . . . . . . . . . . . . . 224 5.21 The CounterApplicationDF SCChart using the Counter class with methods in a dataflow region. . . . . . . . . . . . . . . . . . . . 224 5.22 Composition of the main components in the steam boiler controller. ..............................228 5.23 Inheritance relations between main components in the steam boilercontroller............................229 5.24 The different control modes in the Controller SCChart for the steamboiler..............................231 6.1 A mockup of a behavior tree in LF. The two variants illustrate different options for representing the same behavior. . . . . . 240 293 List of Tables 2.1 A brief overview and comparison of key aspects in LF and SCCharts. It covers the current state of the implementation, plus references to extensions made by this thesis. . . . . . . . 16 4.1 Results of the Furuta pendulum simulation. . . . . . . . . . . 147 5.1 Characteristics of OO features in the current implementation ofSCCharts..............................215 295 List of Code Listings 2.1 Abstract implementation of a tick function loop for the PendulumSound SCChartinC. ..................... 36 2.2 Source code of the FurutaPendulum main program in LF. . . . . 39 2.3 Source code of the FurutaPendulum main program in SCCharts................................ 40 2.4 Source code of the PendulumSound component in LF....... 41 2.5 Source code of the PendulumSound component in SCCharts. . . 42 2.6 Source code of the PendulumController component in LF. . . . . 44 2.7 Source code of the PendulumController component in SCCharts................................ 46 3.1 Source code of the PendulumController reactor with modes. . . 63 3.2 Source code of the ToggleLED reactor................ 64 3.3 Source code of the Connection reactor illustrating manual management of a socket connection. . . . . . . . . . . . . . . . 75 3.4 Source code of the ShallowStrongAbortExample reactor. . . . . . 88 4.1 Tick loop example for dynamic ticks. . . . . . . . . . . . . . . 133 4.2 Source code of the TimedAO reactor embedding the SCChart. . 160 5.1 Data structures in Blech and Céu, illustrating a counter with an additional routine that increments the value every tick respectively millisecond. . . . . . . . . . . . . . . . . . . . . . . 172 5.2 A simple generic interface for a stack in Java . . . . . . . . . . 182 5.3 Textual SCCharts-based Counter class. ..............187 6.1 A mockup of the code structure generated by an OO statebased approach in Java for the CountingCounterApplication in Figure 5.4b and CountingCounter with inheritance. . . . . . . . 246 297 List of Algorithms 3.1 Processing of mode transitions at the end of each execution cycle. ................................. 80 299