-
Notifications
You must be signed in to change notification settings - Fork 6
/
RequirementAnalysisExample.sadl
153 lines (125 loc) · 3.96 KB
/
RequirementAnalysisExample.sadl
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
uri "http://arcos.rack/examples/RequirementAnalysis".
import "http://arcos.rack/PROV-S".
import "http://arcos.rack/ANALYSIS".
import "http://arcos.rack/REQUIREMENTS".
import "http://arcos.rack/AGENTS".
import "http://arcos.rack/MODEL".
/* This goes in an overlay */
SADL_REQUIREMENT is a type of REQUIREMENT.
SADL_ONTOLOGY is a type of DATA_DICTIONARY_TERM.
RAE_MODEL is a type of MODEL.
RAE is a type of ANALYSIS.
RAE_OUTPUT is a type of ANALYSIS_OUTPUT
described by cvr with values of type CONTROLLED_VARIABLE_RESULT.
CONTROLLED_VARIABLE_RESULT is a class
described by cvrCheck with a single value of type RAE_CHECK
described by cvrResult with a single value of type RAE_RESULT.
RAE_RESULT is a class must be one of {Passed, Failed, Indeterminate}.
RAE_CHECK is a type of THING.
/* This goes in the data */
ASSERT-RAE is a ENTITY.
russell-d-e is a PERSON.
/***********************************************
* REQUIREMENTS and DATA_DICTIONARY
***********************************************/
REQ-1 is a REQUIREMENT
description "SYSTEM shall set output_1 to true
when
input_1 > input_2.".
REQ-2 is a REQUIREMENT
description "SYSTEM shall set output_1 to true
when
input_1 < input_2.".
REQ-3 is a REQUIREMENT
description "SYSTEM shall set output_2 to true
when
input_1 > input_2.".
REQ-4 is a REQUIREMENT
description "SYSTEM shall set output_2 to true
when
input_1 <= input_2.".
input_1 is a SADL_ONTOLOGY.
input_2 is a SADL_ONTOLOGY.
output_1 is a SADL_ONTOLOGY.
output_2 is a SADL_ONTOLOGY.
SYSTEM is a SADL_ONTOLOGY.
/***********************************************
* RAE Model
***********************************************/
output_1_SYSTEM is a RAE_MODEL
models REQ-1
models REQ-2
models input_1
models input_2
models output_1.
output_2_SYSTEM is a RAE_MODEL
models REQ-3
models REQ-4
models input_1
models input_2
models output_2.
/***********************************************
* RAE Analysis
***********************************************/
SYSTEM_analysis is a RAE
analyzedWith ASSERT-RAE
runBy russell-d-e
used output_1_SYSTEM
used output_2_SYSTEM.
/***********************************************
* RAE Output
***********************************************/
output_1_SYSTEM_output is a RAE_OUTPUT
analyzes output_1_SYSTEM
wasGeneratedBy SYSTEM_analysis
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck InnerContingency)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck Contingency)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck GlobalContingency)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck PairConflict)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Failed
cvrCheck Completeness).
output_2_SYSTEM_output is a RAE_OUTPUT
analyzes output_2_SYSTEM
wasGeneratedBy SYSTEM_analysis
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck InnerContingency)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck Contingency)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck GlobalContingency)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck PairConflict)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck Completeness)
cvr (a CONTROLLED_VARIABLE_RESULT
cvrResult Passed
cvrCheck Surjectivity).
/***********************************************
* RAE Check Definitions
***********************************************/
InnerContingency is a RAE_CHECK
with title "Inner Contingency".
Contingency is a RAE_CHECK
with title "Contingency".
GlobalContingency is a RAE_CHECK
with title "Global Contingency".
PairConflict is a RAE_CHECK
with title "Pair-Conflict".
Completeness is a RAE_CHECK
with title "Completeness".
Surjectivity is a RAE_CHECK
with title "Surjectivity".