1 How good is your embedded esign, if at all?Holger Hermanns dependable systems and software Saarland University Saarbrücken, Germany

2

3

4 The German Energy Turn-AroundRenewables are on the rise! In Germany … and elsewhere On residential rooftops 2009: 10 GW 2013: 36 GW

5 The German Energy Turn-AroundRenewables are on the rise! In Germany … and elsewhere On residential rooftops. 2009: 10 GW 2013: 36 GW That is so great! Is it? European Grid: 15 GW ≈ 1 Hz Target: [49.8, 50.2] Hz

6 The German Energy Turn-AroundRenewables are on the rise! All over Germany, masses of photovoltaic microgenerators are rolled out: They jointly influence the stability of the European grid. Current state of control: In Germany … and elsewhere On residential rooftops. "on-off" controller EN 50438:2007, in force since 2007: Switch off when frequency > 50.2 Hz VDE-AR-N 4105, required today: Output linear function of frequency in [50.2, 51.5] Hz Emergency switchoff above 51.5 Hz "linear" controller Switch on again when < Hz for 1 minute

7  The Distributed Turn-Around Each controller is a gambler.Let a die decide whether you must leave the grid. Size of dice depends on grid frequency. ... as in e (linearly) Let another die decide when you can resume. Size of dice depends on length of overload. ... as in Ethernet (exponentially)

8 Quantitative Models

9 All models are wrong, but some are usefulGeorge E. P. Box

10 Useful Quantitative Modelsfinite automata dark light x==50 off! on? x:=0; dark light

11 all running at the same speedUseful Quantitative Models finite automata with clocks all running at the same speed dark light x==50 off! on? x:=0; dark light Timed Automata

12 incurred as time advancesUseful Quantitative Models finite automata with clocks and with costs incurred as time advances 40 mA 0 mA dark light x==50 off! on? x:=0; dark light Priced Timed Automata

13 Useful Quantitative Modelsfinite automata with clocks and with costs modular: composition of automata 40 mA 0 mA dark light x==50 off! on? x:=0; someone y>d on! y:=0; d:=U[5,55]; dark light Automata Networks

14 Useful Quantitative Modelsfinite automata with clocks and with costs modular: composition of automata with probability distributions Exp[5] Pr(“on!” >t) 40 mA 0 mA dark light T>85 && x==50 off! on? x:=0; someone y>d on! y:=0; d:=Exp[5]; 2% 98% dark light Stochastic Timed Automata

15 Useful Quantitative Modelsfinite automata with clocks and with costs modular: composition of automata with probability distributions and continuous dynamics Exp[5] Pr(“on!” >t) 40 mA 0 mA dark light T>85 && x==50 off! on? x:=0; someone y>d on! y:=0; d:=Exp[5]; 2% 98% dark light Stochastic Hybrid Automata

16 Model Checking

17 Model Checking Real System Requirements Modelling Formalising

18 Requirement SpecificationModel Checking Real System Requirements Modelling Formalising Formal System Model possible behaviour Requirement Specification allowed behaviour

19 Requirement SpecificationModel Checking Real System Requirements Modelling Formalising Formal System Model possible behaviour Requirement Specification allowed behaviour  Model Checker

20 Requirement SpecificationModel Checking Real System Requirements Modelling Formalising Formal System Model possible behaviour Requirement Specification allowed behaviour  Model Checker done No Counterexample YES

21 Requirement SpecificationModel Checking Real System Requirements Modelling Formalising Formal System Model possible behaviour Requirement Specification allowed behaviour  Model Checker Next Requirement done No Counterexample YES

22 What 3 items would you taketo a deserted island?

23 What 3 items up to 1 kg and 1 liter would you taketo a deserted island?

24 What 3 items up to 1 kg and 1 liter would you taketo a deserted island?

25 ESA 'Fly Your Satellite!' programWhat 3 items up to 1 kg and 1 liter would you take into space? Cube Satellites, educational / scientific use Limits: Up to 1 kg & 1 liter Mission time: up to 4 years

26

27 GOMX-1 2U CubeSat (2 liter) Launched in November 2013 Payloads:software defined receiver for aircraft signals color camera for earth observation Telemetry transmitted on amateur radio frequency Massive amounts of data collected battery voltage, temperature, solar infeed, … Runs our calibration experiments. SENSATION

28 Battery Kinetics

29 Battery Kinetics 100 % 0 %

30 Battery Kinetics B A “Kinetic Battery Model”, or KiBaM

31 Battery Kinetics B A “Kinetic Battery Model”, or KiBaM

32 Battery Kinetics full B A A empty B “Stochastic” KiBaM

33 Battery Kinetics full B A A empty B “Stochastic” KiBaM

34 Battery Kinetics full B A A empty B “Stochastic” KiBaM

35 Battery Kinetics full B A A empty B “Stochastic” KiBaM

36 Battery Kinetics full B A A empty B “Stochastic” KiBaM

37 Battery Kinetics full B A A empty B “Stochastic” KiBaM

38 Battery Kinetics full B A A empty B “Stochastic” KiBaM

39 Battery Kinetics full B A A empty B “Stochastic” KiBaM

40 Battery Kinetics full B A A empty B “Stochastic” KiBaM

41 GOMX-2 2U CubeSat (2 liter)Shipped in October with Cygnus CRS-3 towards ISS Payloads: Optical communication experiments from NUS Highspeed UHF and SDR receiver Shipping failed after liftoff Satellite was recovered from wreckage and returned to manufacturer SENSATION

42

43 GOMX-3 mission planningVery tight power budget Needs dynamic and battery aware scheduling What we do: Priced Timed Automata modelling with linear battery Generate optimal schedules for 1 week or 1 day horizon Evaluate schedules on “stochastic“ KiBaM for robustness Send to orbit, observe behaviour, update model SENSATION

44 GOMX-3 mission planningVery tight power budget Needs dynamic and battery aware scheduling What we do: Priced TA modelling with linear battery model Generate optimal schedules for 1 week horizon Evaluate schedules on random KiBaM for robustness Prepare for updates of model state based on orbit data SENSATION

45 A one-day schedule and its depletion risk SENSATION

46 Meeting Reality, SafelySENSATION

47 Meeting Reality

48 On-line and Compositional Learning of Controllers with Application to Floor HeatingKim G. Larsen, Marius Mikucionis, Marco Muniz, Jiri Srba, Jakob H. Taankvist Aalborg University, DK DG Verification and Validation of Real-Time and Embedded Systems Professor Kim G Larsen CISS, Aalborg University Denmark Model-driven development has been proposed as a way to deal with the increasing complexity of real-time and embedded systems, while reducing the time and cost to market.  The use of models should permit early assessment of the functional correctness of a given design as well as requirements for resources (e.g. energy, memory, and bandwidth) and real-time and performance guarantees. In the lecture we will introduce the tool UPPAAL providing an integrated environment for modeling, validation, verification and synthesis of real-time systems modeled as networks timed automata, extended with data types and user-defined functions. The lectures will provide details on the expressive power of timed automata in relationship to embedded systems as well as details on the power and working of the UPPAAL verification engine. Particular attention  will be  given to the  theory of  the underlying formalisms of UPPAAL, including timed automata, priced timed  automata,  and  (priced)  timed  games addressing  a  number  of associated decision problems  related to  model-checking  and optimal scheduling and strategies.  Also, the frontier of decidability will be drawn including pointing out a number of open problems. The lectures will also emphasize the research effort in design algorithms and datastructures for efficient analysis on practical and industrial cases. FSEN’09 This talk will introduce various recent extensions of the by know well-established formalism of timed automata. The talk apply these extension to verification, optimal scheduling, performance analysis and controller synthesis of real-time and embedded systems. The timed automata extensions considered -- priced timed automata, game timed automata as well as probabilistic timed automata -- are all supported by various branches of the real-time verificaiton tool UPPAAL (www.uppaal.com) which will be demonstrated during the talk.  Also, the development of algorithms and datastructures applied by UPPAAL for the efficient analysis of these models is provided. Validation, Performance Analysis and Synthesis of Embedded Systems Kim G Larsen Within the upcoming European Joint Technology Initiative ARTEMIS as well as several national initiatives such as CISS (www.ciss.dk) and DaNES (http://www.danes.aau.dk/),  model-driven development is a key to dealing with the increasing complexity of embedded systems, while reducing the time and cost to market.  The use of models should permit early assessment of the functional correctness of a given design as well as  requirements for resources (e.g. energy, memory, and bandwidth) and real-time and performance guarantees.  Thus, there is a need for quantitative models allowing for timed, stochastic and hybrid phenomenas to be modeled an analysed. UPPAAL and the branches CORA and TIGA provide an integrated tool environment for modelling, validation, verification and synthesis of real-time systems modelled as networks timed automata, extended with data types and user-defined functions. The talk will provide details on the expressive power of timed automata in relationship to embedded systems as well as details on the power and working of the UPPAAL verification engine. In this talk we demonstrate how UPPAAL has been applied to the validation, performance analysis and synthesis of embedded control problems.  The applications include so-called task graph scheduling and MPSoC systems consisting of application software running under different RTOS on processors interconnected through an on-chip network. Also we show how CORA and TIGA has been used to synthesize optimal (e.g. wrt. energy or memory) scheduling strategies given applications, including Dynamic Voltage Scaling and a climate controller.

49 Stochastic Hybrid SystemsPlayer 1 A Bouncing Ball Player 2 Pr[<=20](<>(time>=12 && Ball1.p>4)) simulate 1 [<=20]{Ball1.p, Ball2.p} On The Power of SMC 2 SSFT15/UPPAAL SMC/Hybrid

50 Other Applications On The Power of SMC 2 FIREWIRE BLUETOOTH10 node LMAC Schedulability Analysis for Mix Cr Sys Markov Chain or Stochastic Timed Automata .. By simulation runs we may check (test) whether the model satisfy a given property with a desired level of confidence (significance). Show something from UPPAAL SMC and what we can do! Also recall the testing theory for probabilistic bisimulation Smart Grid Demand / Response Energy Aware Buildings Battery Scheduling Genetic Oscilator (HBS) Passenger Seating in Aircraft On The Power of SMC 2

51 Floor Heating ScenarioEach room has a hot water loop that can be opened/closed Loops are controlled via activating / deactivating valves. Rooms equipped with wireless temperature sensors (report every 15 minutes). Each room has its user-defined target temperature. Control Task: maintain room temperatures as close as possible to target temperatures TACAS 2016

52 Additional Factors and RestrictionsHeat exchange among the rooms (influenced by the door positions). Pipes are traversing under several rooms. Outside temperature and weather forecast. Capacity of the heating system. Temperature user-profiles for the different (groups of) rooms. Control Task: maintain room temperatures as close as possible to target temperatures TACAS 2016

53 1-Room / 1-Window Game Room Monitor TACAS 2016

54 1-Room / 1-Window Game Window U[6,7] U[7,8] U[11,12] U[24,24] U[12,13]Find strategy 𝜎 that minimizes expectation of TACAS 2016

55 Compositional SynthesisSplit the valves into controllable and fixed (controlled via Bang-Bang) Synthesize a strategy for controllable valves Swap the controllable and fixed valves and synthesise another strategy Merge strategies. 𝟐 𝟓𝒉 + 𝟐 𝟔𝒉 instead of 𝟐 𝟏𝟏𝒉 decision choices (in our case ℎ=3) TACAS 2016

56 Latest News TACAS 2016

57 Latest News TACAS 2016

58 Latest News 3 day scenario Evaluation of undermodified parameters (0-20%) TACAS 2016