Lecture 4
Component Behavioral Modeling
with REMES
CBSE graduate course
Page 1,
Agenda
 Background and Motivation
 REMES
 Connecting REMES and ProCom
 REMES Editor
 Lab2
CBSE graduate course
Page 2,
Background and Motivation

Embedded systems

“Computer that does not look like computer”

Part of a larger system or machine

Typical requirements
 Low cost
 Constantly react to changes in the environment
 Dependability
 Compute certain results in real-time without delay
 Limited available resources
 Manage the growing complexity of software

Need for solutions that
 Alleviate software complexity
 Ensure predictable system behavior
CBSE graduate course
3
Background and Motivation
{RB} > {RC1}
B
{RB
C1
{RC1}
Repository
C2
{RC2}
C3
Cn
{RC3}
{RCn}
CBSE graduate course
Page 4,
Background and Motivation
 Challenge

construct component model for ES design enriched with
behavioral information

support predictable system development and as such guarantee
absence or presence of certain properties

prediction methods should be available already at early design
stage

bottom-up  resource analysis can guide the selection of components

top-down  resource analysis could help in correct decomposition of
system’s specification
CBSE graduate course
Page 5,
REMES behavioural language
CBSE graduate course
Page 6,
Classification of resources
 Resource consumption- annotated with c;
accumulated resource usage up to some time point
 c’ - rate of consumption over time
 Classification of resources:

discrete or continuous nature

referable or non-referable
Resource Class
Characteristics
A
(memory)
discrete c´=0 or c’=inf
referable
B
(CPU, bandwidth)
C
(CPU, energy)
discrete c’=0 or c´=inf
non-referable
continuous c´=n, n in Z - {-inf,+inf}
non-referable
CBSE graduate course
Page 7,
REMES – REsource Model for Embedded Systems
 Behavioral model intended to describe the resource-wise
behavior of interacting embedded components
 Behavior of a component is a mode
 Modes

atomic

composite
CBSE graduate course
Page 8,
REMES - modes
 Mode M (SM, V, In, Out, E, RC, Inv, CC)

Control points In: (Init point, Entry point), Out: (Write point, Exit point)

Variables (V) (boolean, natural, integer, array, clock, history variables)

Actions over edges (E)


discrete A (guard, body)

delay/timed
Constraints

set of invariants (Inv)

set of res. diff equations (RC)

Conditional connectors (CC)

Nested submodes (SM)
Entry Point
Init Point
Exit Point
Write Point
M
submode3
C
submode1
submode2
Inv1
RC1
Page 9,
Example1- internal behaviour of Control component in REMES
Control
Credentials
t<=30,
cpu’=2
Init
logged==false
Entry
C
Exit
Air_conditioning
cpu’=10
eng’=2
Initialization
resource mem:TA;
resource eng:TC;
resource cpu:TC;
t:clock
CBSE graduate course
Page 10,
Analysing REMES based ES
 REMES modes have access to R1,…, Rn
 Goal

analyze various scenarios of system’s resource usage
 Analysis model for REMES
rtot  def w1  r1  w 2  r2    w n  rn

rtot total accumulated resource consumption for R1,…, Rn

r1,…, rn accumulated consumption of R1,…, Rn

w1,…, wn relative importance of r1,…, rn
CBSE graduate course
Page 11,
Analysing REMES based ES
 Translating REMES into Priced timed automata or Multi PTA


TA + costs on locations and edges

REMES atomic submode
 PTA location(s)

REMES discrete edge
 PTA edge

REMES discrete step


REMES conditional connectors are removed
PTA transition
Automated translation
 Types of analysis

Feasibility

Optimal/ worst-case resource consumption

Trade-off analysis
2015-10-03
12
Page 12,
Analysing REMES based ES
•
PTA waits in location Start for
system startup
•
Init, Entry, Write and Exit
locations created
•
Transformation of Submode2
•
Internal execution rounds - PTA
edge connecting locations Write
and Submode1
•
Synchronization with other
components
Page 13,
Analysing REMES based ES
PTA / MPTA
yes
Model Checker
(Uppaal Cora)
resource-aware
property
EF cos t  n v
error trace
Assumptions from
hardware abstraction:
Memory budget, Bandwidth, Cost model
CBSE graduate course
Page 14,
Analysing REMES based ES
ProCom component
REMES model of
component behavior
Attribute Framework
 Managing and integrating properties
 Each ProCom component has an attribute with a complex value:

Reference to a REMES model file

Reference to a mapping file between ProCom and REMES interfaces
CBSE graduate course
Page 15,
Connecting ProCom and REMES
 ProSave level

trigger port  REMES interface boolean variable

data port
 REMES interface data variable
 ProSys level

input message port  REMES read boolean variable
and REMES read data variable of the
same type as the port type

output message port  REMES write boolean variable
and REMES write data variable
CBSE graduate course
Page 16,
Example2- Temperature control system

core is heated at some given rate

core temperature should be maintained
between a minimum and a maximum

when max temp. is reached, designed
to be cooled down by inserting one of
two existing rods , which cool at
different rates R1 or R2

a rod is available again after T time
units
CBSE graduate course
Page 17,
Example2- Temperature control system
 Model of the architecture and behaviour

System modeled with 3 ProSave components

Each component has a behavior depicted by a REMES mode

Assume memory and cpu usage

Formal analysis

ProCom + REMES  PTA
CBSE graduate course
Page 18,
Example2- Temperature control system
CBSE graduate course
Page 19,
Example2- Temperature control system
CBSE graduate course
Page 20,
Example2- Temperature control system – Analysis in Uppaal
Just for illustration!
Page 21,
CBSE graduate course
Page 22,
REMES tool-chain
CBSE graduate course
Page 23,
REMES tool-chain
 The REMES tool-chain consists of

REMES model editor

REMES simulator to test timing and resource
behavior prior to formal analysis

Automated transformation from REMES to PTA
for formal analysis and UppaalLite editor
CBSE graduate course
CBSE graduate course
Page 24,
CBSE graduate course
Page 25,
REMES editor
CBSE graduate course
Page 26,
CBSE graduate course
Page 27,
REMES language elements



Composite mode 

Compartments  for declaration variables, resources, constants
CBSE graduate course
Page 28,
REMES language elements




Submodes 


Invariant – time is allowed to pass until invariant is violated
Non-lazy – does not contain any.invariant, Time is allowed to pass in a non-lazy mode until at
least one of the guards of the outgoing discrete actions evaluates to true

Urgent – time is not allowed to pass (invariant is false)

.
CBSE graduate course
Page 29,
REMES language elements





Input and output 

Init-, entry-, exit-, write – points (local exit points not presented here)
CBSE graduate course
Page 30,
REMES language elements







Control flow

Edges with guards and actions 

Conditional connectors 
CBSE graduate course
Page 31,
Introduction to Lab2
CBSE graduate course
Page 32,
Objectives
 Learn how to model behaviors of component-based
embedded systems

Model internal behavior of components

Think about modes, actions, resources, invariants etc.

Get familiar with the REMES editor
CBSE graduate course
Page 33,
Expected Output
 Same system as for Lab1

Archive files only (no folder) named ”Lab2_X_Y.zip”
where X_Y=first student name_second student name
1 report explaining your design choices
The Project folder for your system
 Individual work/ group of two students

And nothing else!
 Do not copy solutions from others !
CBSE graduate course
Page 34,
Deadline
 Thursday 21 February 2013 23:59 (FIRM Deadline!)
 If you submit your work late, you fail one submission opportunity
 Remember

Lab2 needs to be aproved for passing the course
CBSE graduate course
Page 35,
The assignment
 In 2 exercices

Modelling behavior of simple Touch-Lamp
system

Modeling behavior of an abstracted version of a
Baking Conveyor System
CBSE graduate course
Page 36,
Exercise 1- Touch Lamp System
 Lamp has two modes of light operation
• Dim – 1 touch
• Bright – 2 successive touches within 15 sec
CBSE graduate course
Page 37,
Exercise 2- Industrial Baking Conveyor System
 Main parts
•Oven
•Conveyor Belt
•Orchestrator
CBSE graduate course
Page 38,
Usage Scenario
Ensure that the conveyor belt
and the oven are working
together
Orchestrator
Oven
Conveyor
Belt
Carries the cookies
from point A to point B
in passing by the oven
Oven monitors the temperature and humidity and
determines 1. if the heat should be increased or
decreased and 2. displays the status of the cookies
CBSE graduate course
Page 39,
Exercise 1 and 2- What do you need to do?
 To model the behaviour of the system components

Lamp component for Exercise 1

Orchestrator, Oven and Conveyor Belt component for
Exercise 2
 Tips

Start by understanding REMES
 think about different types of modes that exist in REMES

Use pen and paper before using REMES editor

Once you are sure of your solution. Model it in
the REMES editor
CBSE graduate course
Page 40,
CBSE graduate course
Page 41,
Descargar

Managing Component-Based Systems with Configuration …