WBS_ARP_v1_crosslevel.oss 1.97 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
COMPONENT simple system

INTERFACE

INPUT PORT Pedal_Pos1: boolean;
INPUT PORT Pedal_Pos2: boolean;
OUTPUT PORT Brake: boolean;

CONTRACT brake
  assume: Pedal_Pos1 iff Pedal_Pos2;
  guarantee: (Pedal_Pos1 or Pedal_Pos2) implies (in the future Brake);

REFINEMENT

SUB bscu: BSCU;
SUB hydr: Hydraulic;

CONNECTION bscu.Pedal_Pos1 := Pedal_Pos1;
CONNECTION bscu.Pedal_Pos2 := Pedal_Pos2;
CONNECTION Brake := hydr.Brake;
CONNECTION hydr.CMD_AS := bscu.CMD_AS;
CONNECTION hydr.Valid := bscu.Valid;

CONTRACT brake REFINEDBY bscu.bscu1.cmd, bscu.bscu2.cmd,
                         bscu.bscu1.valid, bscu.bscu2.valid,
                         bscu.switch.select, hydr.brake;

COMPONENT BSCU

INTERFACE

INPUT PORT Pedal_Pos1: boolean;
INPUT PORT Pedal_Pos2: boolean;
OUTPUT PORT CMD_AS: boolean;
OUTPUT PORT Valid: boolean;


REFINEMENT

SUB bscu1: subBSCU;
SUB bscu2: subBSCU;
SUB switch: Select_Switch;

CONNECTION bscu1.Pedal_Pos := Pedal_Pos1;
CONNECTION bscu2.Pedal_Pos := Pedal_Pos2;
CONNECTION Valid := bscu1.Valid or bscu2.Valid;
CONNECTION switch.In1 := bscu1.CMD_AS;
CONNECTION switch.In2 := bscu2.CMD_AS;
CONNECTION switch.Select := bscu1.Valid;
CONNECTION CMD_AS := switch.Out;

COMPONENT subBSCU

INTERFACE

INPUT PORT Pedal_Pos: boolean;
OUTPUT PORT CMD_AS: boolean;
OUTPUT PORT Valid: boolean;

CONTRACT cmd
assume: true;
guarantee:
  always ( Pedal_Pos implies then CMD_AS); 

CONTRACT valid
assume: true;
guarantee:
  Valid and always ((Pedal_Pos and not then CMD_AS) iff then not Valid);



COMPONENT Select_Switch

INTERFACE

INPUT PORT In1: boolean;
INPUT PORT In2: boolean;
INPUT PORT Select: boolean;
OUTPUT PORT Out: boolean;

CONTRACT select
assume:
  TRUE;
guarantee:
  always ((Select implies (In1 implies Out)) and
  	  ((not Select) implies (In2 implies Out)));


COMPONENT Hydraulic

INTERFACE

INPUT PORT CMD_AS: boolean;
INPUT PORT Valid: boolean;
OUTPUT PORT Brake: boolean;

CONTRACT brake
assume:
  TRUE;
guarantee:
  always ((CMD_AS or not Valid) implies (in the future (Brake) ));