Model

---

System

Component description:

Type	Notes
System

Local Attributes:

Name	Type
error	Integer

Input ports:

Name	Type
speed	Real

Output ports:

Name	Type
sensed_speed	Real
sensed_speed_is_present	Boolean

Subcomponents:

Name	Type
sensor1	SpeedSensor
sensor2	SpeedSensor
selector	Selector
monitor2	MonitorPresence
monitor1	MonitorPresence

Connections:

Connected Port	Connecting Port	Iterative Condition
sensor2.speed	speed
sensor1.speed	speed
monitor2.input_is_present	sensor2.sensed_speed_is_present
monitor1.input_is_present	sensor1.sensed_speed_is_present
selector.input2	sensor2.sensed_speed
selector.input1	sensor1.sensed_speed
selector.input1_is_present	sensor1.sensed_speed_is_present
selector.input2_is_present	sensor2.sensed_speed_is_present
sensed_speed	selector.output
sensed_speed_is_present	selector.output_is_present
selector.switch_current_use	monitor1.absence_alarm or monitor2.absence_alarm
monitor1.enabled	( selector.current_use=1 )
monitor2.enabled	( selector.current_use=2 )

Contracts:

CONTRACT Sense
assume: /--assuming that: - at the beginning the speed is 0 - the acceleration/deceleration is below a threshold --/ speed=0 & G( (next(speed) - speed)<=1 and (next(speed) - speed)>=-1 ) ;
guarantee: /--we expect that: - there is always a sensed speed - the delta between the speed and the sensed speed is <= 2 --/ always ((sensed_speed - speed <= 2) and (sensed_speed - speed >= - 2) and sensed_speed_is_present) ;

Contract Refinements:

CONTRACT Sense
refined by: sensor1.Sense,sensor2.Sense,selector.Select,selector.Switch,monitor2.Monitor,monitor1.Monitor

---

SpeedSensor

Component description:

Type	Notes
SpeedSensor

Input ports:

Name	Type
speed	Real

Output ports:

Name	Type
sensed_speed	Real
sensed_speed_is_present	Boolean

Contracts:

CONTRACT Sense
assume: /--assuming that: - at the beginning the speed is 0 - the acceleration/deceleration is below a threshold --/ speed=0 & G( (next(speed) - speed)<=1 and (next(speed) - speed)>=-1 ) ;
guarantee: /--we expect that: - there is always a sensed speed - the delta between the speed and the sensed speed is <= 1 --/ always ((sensed_speed - speed <= 1) and (sensed_speed - speed >= - 1) and sensed_speed_is_present) ;

---

Selector

Component description:

Type	Notes
Selector

Input ports:

Name	Type
input1	Real
input1_is_present	Boolean
input2	Real
input2_is_present	Boolean
switch_current_use	Boolean

Output ports:

Name	Type
current_use	Interval1_2 - Range [1 .. 2]
output	Real
output_is_present	Boolean

Contracts:

CONTRACT Select
assume: true ;
guarantee: /-- we expect that: - at the beginning the sensed speed is 0 - the sensed speed will be measured by the current sensor --/ (output=0 and output_is_present = TRUE) and always ((next(current_use=1) implies (next(output)=input1 and next(output_is_present)=input1_is_present)) and (next(current_use=2) implies (next(output)=input2 and next(output_is_present)=input2_is_present))) ;

CONTRACT Switch
assume: true ;
guarantee: /--we expect that : - the switch of the sensor depends only on the input boolean port 'switch_current_use' --/ always ( ((current_use=1 and switch_current_use) implies next(current_use)=2) and ((current_use=2 and switch_current_use) implies next(current_use)=1) and ((not switch_current_use) implies not change(current_use))) ;

---

MonitorPresence

Component description:

Type	Notes
MonitorPresence

Input ports:

Name	Type
input_is_present	Boolean
enabled	Boolean

Output ports:

Name	Type
absence_alarm	Boolean

Contracts:

CONTRACT Monitor
assume: /-- assuming that: - at the beginning the sensor associated to this monitor is working --/ input_is_present=TRUE ;
guarantee: /-- we expect that: - an alarm is triggered whenever the monitor is enabled and the input is not present (is absent) --/ always ((absence_alarm) iff (enabled and not(input_is_present))) ;

---

Validation and Verification Results

Properties Validation Results:

Results not available.

---

Assume/Guarantee Properties Validation Results:

Results not available.

---

Check Contract Refinement Results:

Main class: System

Contract	Status
[System] Sense	Success

---

Check Contract Composite Implementation Results:

Main class: System

Contract	Status
[System] Sense	Success
[Selector] Switch	Success
[Selector] Select	Success
[SpeedSensor] Sense	Success
[MonitorPresence] Monitor	Success

---

Contract-based Fault Tree Analysis Results:

Results not available.

---

Model Checking Results:

Results not available.

---

Fault Tree Analysis Results:

Main class: System
Conditions: property::sensor1.sensed_speed_is_present=TRUE

Main class: System
Conditions: property::sensor1.sensed_speed_is_present=FALSE

---

Failure Modes and Effects Analysis Results:

Results not available.