Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Design of Embedded Systems Models Validation and Synthesis EE 249 Lecture 9 Prof Dr Reinhard von Hanxleden Christian Albrechts Universita t Kiel Department of Computer Science Real Time Systems and Embedded Systems Group 2 October 2007 Last compiled 4th October 2007 15 09 hrs Synchronous Languages Esterel Fall 2007 EE 249 Slide 1 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Overview Introduction to Safe State Machines and Esterel Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Fall 2007 EE 249 Slide 2 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Introduction to Esterel I I I Imperative textual concurrent language Developed since early 1980s Ge rard Berry Based on synchronous model of time I I I I I I Program execution synchronized to an external clock Like synchronous digital logic Suits the cyclic executive approach Same model of computation as SyncCharts Safe State Machines SSMs EsterelStudio generates Esterel from SSMs as intermediate code Currently undergoing IEEE standardization Esterel v7 Thanks to Stephen Edwards http www1 cs columbia edu sedwards for providing part of the following material Fall 2007 EE 249 Slide 3 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Introduction to Esterel Time is divided into discrete ticks also called cycles steps instants Two types of statements I Those that take zero time execute and terminate in same tick e g emit I I Correspond to Connectors in SSMs Those that delay for a prescribed number of ticks e g await I Correspond to States in SSMs Fall 2007 EE 249 Slide 4 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Signals I I Esterel programs SSMs communicate through signals These are like wires I I I I Each signal is either present or absent in each tick Can t take multiple values within a tick Presence absence not held between ticks Broadcast across the program I Any process can read or write a signal Fall 2007 EE 249 Slide 5 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Signals I I Status of an input signal is determined by input event and by local emissions Status of local or output signal is determined per tick I I I Default status absent Must execute an emit S statement to set signal S present await A I Waits for A and terminates when A occurs Fall 2007 EE 249 Slide 6 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Synchrony Hypothesis I Computations are considered to I I take no time be atomic G Luettgen 2001 Fall 2007 EE 249 Slide 7 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Synchronous Model of Computation To summarize the synchronous model of computation of SSMs Esterel is characterized by 1 Computations considered to take no time synchrony hypothesis 2 Time is divided into discrete ticks 3 Signals are either present or absent in each tick Sometimes synchrony refers to just the first two points e g in the original Statecharts as implemented in Statemate to explicitly include the third requirement as well we also speak of the strict synchrony Fall 2007 EE 249 Slide 8 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages The ABRO Example I Consider the following controller specification I I I Emit the output O as soon as both the inputs A and B have been received Reset the behavior whenever the input R is received This is still a bit ambiguous to complete I I I If R occurs emit nothing Do nothing at initialization time Input signals may be simultaneous Fall 2007 EE 249 Slide 9 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages The ABRO Example Mealy Style S0 R R S1 R ABR ABR ABR O S2 BR O S3 AR O S4 Fall 2007 EE 249 Slide 10 Introduction to Safe State Machines and Esterel Esterel Language Overview Esterel SSM Pragmatics Interfacing with the Environment Property Verification Signals and Synchrony The ABRO Example Write Things Once The multiform notion of time Uses Advantages Disadvantages Write Things Once I The disadvantage of this flat notation I I I The answer I I I Size grows exponentially A little change to the specification may incur a major change to the automaton often ends with full rewriting Add hierarchy More generally Write Things Once WTO Analogy from language theory I Use regular expressions to represent large possibly infinite sets of strings Fall 2007
View Full Document
Unlocking...