Heterogeneous Modeling: Hybrid SystemsHeterogeneous Modeling: Hybrid Systems Hybrid Models Automotive Powertrain Languages and Verification Problems Simulink and StateFlow CheckMate Charon MasaccioMotivationMotivationHybrid Systems are becoming a major modeling paradigm for embedded systems Capability of modeling controller and plant Use of concurrent multiple levels of abstractionDifficult to verify and design Combination of continuous and discrete dynamics of different types Lack of “operationally strong” theoretical resultsVariety of tools and approaches mutually incompatible due to modeling differencesFoundations of Hybrid ModelFoundations of Hybrid Model Used classic model by J. Lygeros, S. Sastry and C. Tomlin as basis Model consists of three parts: Structure= sets, discrete and dynamical components Time Bases= intervals over which behavior is continuous Hybrid execution= rules according to which we have jumps and continuous flowsObservations: Non deterministic behavior allowed (needed) Fixed interaction structureSystem SpecificationsSystem SpecificationsDriver Vehicleforce, speed, acceleration, jerk, rpm, fuel consumption,...emissions, external noise, temperature, ...Key, Brake, Gas, Transm.Engine &DrivelineControllerspark advance, injection time,throttle angleClosed loop vehicle modelClosed loop vehicle modelFast NegativeForce Transient m in f(D, Mfuel)τ < τmax Force Tracking Fast PositiveForce Transient Speed Tracking n= n(.) n= n(.)Idle &Trasm On .G>0 | t>τ . .G < GB| B=1 .G<0 | t>τ . .G > GAG > 0G = 0 T > 0T=0 T=0(G>0)& (T>0)T=0 fI(n) = 0 & G=0 fI(n,G) > 0 .G=0 & C=1 .G > 0|B = 1T > 0T=0OUTPUT:n - Eng ine Speedn - Eng ine SpeedFFG G - Generated ForceVVGG - Vehicle Speed - Vehicle Speedn=n(G)FG=0Rpm Tr ackingn= argm in(Mfu el)IdleFG=0VG= VG(.)Stopn=0FG=0StartupFG=0n= .G > 0G = 0(n < nmin)| (K=Of f) n > nst art upK = Start(n < nmin)| (K = O ff)FG=FG(G ,T ,n)FG=FG(G ,T ,n)max Dτ < τmaxmin τFG=FG(G ,T ,n)Mfuel < Mmax; D >DminT>0 &G=0INP UTS:G - Gas PedalG - Gas PedalT - Clutch Pedal & Gear StickT - Clutch Pedal & Gear StickB - Brake PedalB - Brake PedalC - Cruise ControlC - Cruise ControlK - KeyD - ComfortfI(n) = 0 & G=0Why Mixed Models of Computation Why Mixed Models of Computation in internal combustion engines control ?in internal combustion engines control ? Specifications Control variables Physical processes in the plant Description of the HW/SW implementation constraintsinput value timeThrottle valveContinuous ContinuousFuel injectionContinuous DiscreteSpark ignitionDiscrete DiscreteModel of PowerModel of Power--traintrainManifold(continuous system)Engine sub-systemDrive-line (continuous system with changing dynamics)Throttle opening angleSpark timingTorqueManifold pressureClutch Insertion/ReleaseGear changeVehicle SpeedSimple?44--stroke enginesstroke enginesEngine and PowerEngine and Power--train Modeltrain ModelCTSCTSIntake ManifoldIntake ManifoldV(t) - throttle motor voltageα (t) - throttle anglen (t) - crankshaft speed p (t) - manifold pressureV(t)α(t)motor dynamicsp(t)air dynamicsn(t)aV(t)PowerPower--traintrainT (t) - generated torqueαe(t) - torsion anglen(t) - crankshaft speedθ(t) - crankshaft angleωp(t) - wheel speedT(t)power-train dynamicsζ(t)ζ(t)θ(t)Engine and PowerEngine and Power--train Modeltrain Modelcylindersintake manifoldpower-trainHybrid Systems in the Hybrid Systems in the TaggedTagged--Signal Models (Signal Models (TSMsTSMs) Framework) FrameworkHybrid systems can be seenas formalismsfor describing a complex system using mixed models of computation when a single one is not powerful, expressive or practical enough. An event e ∈ V×T: V is the set of values and T is the set of tags e.g. universal time (T is the set of real numbers) discrete time (T is a totally ordered discrete set),a signal is a set of events, a process with N channels is a subset of the set of N-tuples of signals.Models of ComputationModels of Computation A Finite State Machine (FSM)is a synchronous TSM process in which the tags take values in N and the inputs, outputs and states take values on finite sets. A Sequential System (SS)is a synchronous TSM process in which the tags take values in N and the inputs, outputs and states assume values on infinite sets. A Discrete-Event System (DES)is a timed TSM process in which the tags are order-isomorphic with N (and denote instants of time). A Continuous-Time System (CTS)is a timed TSM process in which the tags take values in a connected set on which a metric is defined (and denote instants of time). A Discrete-Time System (DTS)is a synchronous DES.Hybrid TaggedHybrid Tagged--Signal Model of a Single Signal Model of a Single CylinderCylinderengine cycletorque profiletorque generation delayair intakeEngine Cycle (FSM)Engine Cycle (FSM) positive spark advance:the spark is given before the TDC between the compression and expansion strokes. negative spark advance:the spark is given after the TDC between the compression and expansion strokes.Sequential SystemContinuous-Time SystemTorque Generation Delay (SS)Torque Generation Delay (SS)tTi(t)real profilepiece-wise profilesparkk - 2 k - 1 k k+1 aI BS PA AS HTorque Profile (CTS)Torque Profile (CTS)Engine and PowerEngine and Power--train Modeltrain Modelcylindersintake manifoldpower-trainMean-Value Model: accurate over a longer time window regulation control problems low performance transient problemsHybrid Model: cycle accurate transient control problems stability of delay-sensitive control algorithms high performance control algorithmsHybrid Model vs MeanHybrid Model vs Mean--Value ModelValue ModelOutlineOutline Hybrid Models Languages and Verification Problems Simulink and StateFlow CheckMate Charon MasaccioWhat is a simulator?What is a simulator? Given a mathematical model of the system, computes its evolutionand its outputs under a pre-determined set of inputs The mathematical model expresses heterogeneity and concurrency The simulator computes the response of the model by mapping it onto the “device” used to carry out the computation In general, the computing device has limited resources and is digital We must embed the model of time of the model into the
View Full Document