Introduction to Safe State Machines and EsterelSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesEsterel Language OverviewSignal emission + testing, pausingEsterel's model of timeParallelismSignal awaiting, loopingPreemption, exceptions, suspensionEsterel/SSM PragmaticsPeople Counter ExampleVending Machine ExampleTail Lights ExampleTraffic-Light Controller ExampleInterfacing with the EnvironmentEsterel Signal TypesOption 1: Single pure signalOption 2: Two pure signalsOption 3: Boolean valued signalProperty VerificationIntroductionExample: ABROIntroduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationDesign of Embedded Systems: Models, Validationand Synthesis (EE 249)—Lecture 9Prof. Dr. Reinhard von HanxledenChristian-Albrechts Universit¨at KielDepartment of Computer ScienceReal-Time Systems and Embedded Systems Group2 October 2007Last compiled: 4th Octob er 2007, 15:09 hrsSynchronous Languages:EsterelFall 2007 EE 249 Slide 1Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesOverviewIntroduction to Safe State Machines and EsterelSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationFall 2007 EE 249 Slide 2Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesIntroduction to EsterelIImperative, textual, concurrent languageIDeveloped since early 1980s (G´erard Berry)IBased on synchronous model of timeIProgram execution synchronized to an external clockILike synchronous digital logicISuits the cyclic executive approachISame model of computation as SyncCharts/Safe StateMachines (SSMs)IEsterelStudio generates Esterel from SSMs as intermediatecodeICurrently undergoing IEEE standardization (Esterel v7)Thanks to Stephen Edwards (http: // www1. cs. columbia. edu/~sedwards/ ) forproviding part of the following materialFall 2007 EE 249 Slide 3Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesIntroduction to EsterelTime is divided into discrete ticks (also called cycles, steps,instants)Two types of statements:IThose that take “zero time” (execute and terminate in sametick, e.g., emit)ICorrespond to Connectors in SSMsIThose that delay for a prescribed number of ticks (e.g.,await)ICorrespond to States in SSMsFall 2007 EE 249 Slide 4Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesSignalsIEsterel programs/SSMs communicate through signalsIThese are like wiresIEach signal is either present or absent in each tickICan’t take multiple values within a tickIPresence/absence not held between ticksIBroadcast across the programIAny process can read or write a signalFall 2007 EE 249 Slide 5Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesSignalsIStatus of an input signal is determined by input event, and bylocal emissionsIStatus of local or output signal is determined per tickIDefault status: absentIMust execute an “emit S” statement to set signal S presentIawait A:IWaits for A and terminates when A occursFall 2007 EE 249 Slide 6Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesSynchrony HypothesisIComputations are considered toItake no timeIbe atomicG. Luettgen 2001Fall 2007 EE 249 Slide 7Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesSynchronous Model of ComputationTo summarize: the synchronous model of computation ofSSMs/Esterel is characterized by:1. Computations considered to take no time (synchronyhypothesis)2. Time is divided into discrete ticks3. Signals are either present or absent in each tickSometimes, “synchrony” refers to just the first two points (e. g., inthe original Statecharts as implemented in Statemate); to explicitlyinclude the third requirement as well, we also speak of the strictsynchronyFall 2007 EE 249 Slide 8Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesThe ABRO ExampleIConsider the following controller specification:IEmit the output O as soon as both the inputs A and B havebeen received.IReset the behavior whenever the input R is received.IThis is still a bit ambiguous; to complete:IIf R occurs, emit nothingIDo nothing at initialization timeIInput signals may be simultaneousFall 2007 EE 249 Slide 9Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and SynchronyThe ABRO ExampleWrite Things OnceThe multiform notion of timeUses, Advantages, DisadvantagesThe ABRO Example—Mealy StyleS0S1S2 S3S4ABR/ ABR/ABR/OR/BR/OR/AR/OR/Fall 2007 EE 249 Slide 10Introduction to Safe State Machines and EsterelEsterel Language OverviewEsterel/SSM PragmaticsInterfacing with the EnvironmentProperty VerificationSignals and
View Full Document
Unlocking...