Transcript (Union) states

Requirements, their Consistency
and Completeness
RSML Formulation of TCAS II
Discussed as an example of a precise and formal capturing of
a real-world software engineering specifications
SWE 623
(Thanks to Prof. Mats P. E. Heimdahl for references)
SWE 623
Duminda Wijesekera
1
TCAS II
• Traffic alert and collision avoidance system.
• Airborne device functioning independent of ground
based traffic control.
• All commercial and larger commuter and business
aircrafts (with 10-30 seats) must have this on aboard.
• TCAS I provided proximity warning (traffic
advisories) and assist the pilot in visualizing intruder
aircrafts.
• TCAS II recommends escape maneuvers (resolution
advisories) in a vertical direction to avoid collusions.
SWE 623
Duminda Wijesekera
2
Brief History
• Collision avoidance systems are 25 years old.
• Minimal Operational Performance Standards
Document (MOPS-1983) was written in a
combination of English and pseudocode. –
– Revised extensively six times.
– Had difficulty in certification, so Government
started rewriting the document and UCI started an
experimental formal specification and safety
analysis.
SWE 623
Duminda Wijesekera
3
System View
• System = Collection of components working together.
• Process control= input output behavior in the presence
of disturbances.
– Disturbances due to chemical, aerodynamic, thermal or
physical laws.
• Operating Constraints
–
–
–
–
Range constraints for input/output variables.
Operating conditions.
Limits design choices
May be results of quality control, resource bounds, physical
limitations, process characteristics etc.
SWE 623
Duminda Wijesekera
4
TCAS Examples
• Maintain minimum separation between
aircrafts
• Constraints
– No interfering with ground based air traffic
control (ATC) functions.
– Acceptably low level of unwanted alarms.
– Minimizing deviation from ATC assigned
tracks.
SWE 623
Duminda Wijesekera
5
Difference between Goals and Requirements
• Goal= Avoid near misses = (I.e. aircrafts
violating minimum separation distance)
• A legitimate goal, but cannot determine if it is
achievable in a given operating environment.
• Therefore cannot be a requirement of the
system design.
• The system can strive to minimize near misses.
SWE 623
Duminda Wijesekera
6
Basic Process Control Model
• Control variables ( Vc )
– Process monitored through
these
Disturbances
• Manipulated variables ( Vm )
– Controlled through these
Process Fp
• Sensors ( Fs )
– Monitor actual behavior of
process
• Actuators ( Fa )
Manipulated
Variables
Actuator
Controlled
Variables
Sensors
– Devices designed to manipulate
process behavior
• Controller ( Fc)
Controller Fc
– Device used to implement
control function
SWE 623
Command Signal
Duminda Wijesekera
7
RSML Approach
Desired
process
control
behavior
Black-box
specification
of controller
behavior
Specifying
Controller
Design Based
on functional
decomposition
Implementation
• Black-box behavior specified using state machine model
– Outputs of the controller specified with respect to
state change in the model as information received
about current state via controlled variables Vc.
– Control function Fc specified using a model of the
state of all other aircraft within host’s space.
SWE 623
Duminda Wijesekera
8
Basic Definitions
•
•
•
•
•
•
•
Input Variables: Is,,Output Variables: Os
Controlled Vars: Vc ManipulatedVars: Vm
Disturbances: D
Process Function: Fp: Vm x Is x D x t  Os x Vc
Sensor Function: Fs: Vc x t  Is
Actuator Function: FA: Os x t  Vm
Control Function: Fc: Is x Vc x t  Os
SWE 623
Duminda Wijesekera
9
Fc : Controller Function
• Modeled as a state machine
– Iteratively refined during requirements
specification.
• An abstraction of the current understanding of
real world control loop.
• Most control functions are non-linear equations.
• Modeling errors represent mismatches between
real world view and state machine view.
SWE 623
Duminda Wijesekera
10
Design Criteria
• Need black-box behavior, not internal design
information.
• Minimality and simplicity.
• Formal, concise, coherent notation.
• Readability, reviewability
• Best use of graphics, tables and symbolic.
• Ability to formally analyze safety,
completeness and consistency.
SWE 623
Duminda Wijesekera
11
Properties of Statecharts
• And/Or hierarchies.
• Conditions (conditional connectives in RSML)
– I.e. guard determines which Or state to transition as a
consequence of an even triggering.
• Arrays of state machines.
– Example: array of other aircraft (statechart)
• Additions:
– Directed communication (unidirectional explicit FIFO
queue) between state charts
– Broadcast mechanisms with some limitations
SWE 623
Duminda Wijesekera
12
Interface Definitions and
Communication Mechanisms
• State-charts modeled components, hence had to
write interface definitions between models.
• Communication
– Sending machine execute SEND(msg, destination) I.e. receivers name
– Triggers RECEIVE event in destination machine.
– No synchrony hypothesis in communication
SWE 623
Duminda Wijesekera
13
State Machine Descriptions
• Input variables, output variables and graphical state
machines
• Attributes of variable include
–
–
–
–
–
–
Location (machine name),
Source/destination (external component, eg Altimeter)
Type (eg integer) , Expected Range 9eg 1 to 1000,
Granularity (10s) , Units meters), Load (frequency of change)
Exception handling (what to do for out of range)
Traceability information (MOPS document reference)
SWE 623
Duminda Wijesekera
14
Format of
RSML State
Machines
SWE 623
Duminda Wijesekera
15
Example RSML State-chart
SWE 623
Duminda Wijesekera
16
SWE 623
Duminda Wijesekera
17
SWE 623
Duminda Wijesekera
18
Encoding States
SWE 623
Duminda Wijesekera
19
Example
State
Definition
SWE 623
Duminda Wijesekera
20
Transitions
• TRANSITION:
North
East
North
East
•Had a notation for locations such as
•Location: Other_aircraft > Tracked > Intruder_status_52
SWE 623
Duminda Wijesekera
21
Notation for Guarding Conditions
• Conditions written in disjunctive normal form
and tabulated
SWE 623
Duminda Wijesekera
22
Example: Table vs. Logic
SWE 623
Duminda Wijesekera
23
Example: Table vs. Logic
SWE 623
Duminda Wijesekera
24
Analysis
• Completeness: Robustness
– Responsiveness to every possible input and input
sequence.
– Logical OR of transition condition is a tautology.
– Every state having a timeout transition behavior.
• Consistency
– Free of conflicting requirements.
– Free of undesired non-determinism.
SWE 623
Duminda Wijesekera
25
Completeness: D-completeness
• D-Completeness:
– The system must respond in real time to any input
and input sequence. Involves following steps
– At atomic states,
• all behaviors are defined (I.e. all external input changes
are accounted for) and
• There are no conflicting requirements (source of nondeterminism)
SWE 623
Duminda Wijesekera
26
Completeness: OR States Cont..
– At OR (Union) states,
• Transition conditions are disjoint.
– Guards of transitions triggered by the same event are mutually
exclusive.
• Entire domain is covered (OR of conditions is True)
– OR of all guards of conditions triggered by same event is TRUE.
• (I.e. one and ONLY ONE satisfiable transition out of
every state)
• AND/OR tabular representation of guards is very helpful
for analysis.
• In general, this problem is NP complete (3-sat is NP
hard), but Used BDD’s to manipulate conditions.
SWE 623
Duminda Wijesekera
27
Completeness: OR - Continued
– At OR (Union) states: Problems Encountered,
• BDD’s are only good for symbolic manipulations, hence a
lot of potential errors in the specifications are reported.
• Conversely, theorem proving approach will cover some of
these problems, but is VERY expensive to do by itself.
• Would like a hybrid of BDD’s talking to theorem provers,
but such things do not exist yet!
• See Heimdahl, Czerney article in High Assurance
Systems Engineering Conference 1999 on this point.
SWE 623
Duminda Wijesekera
28
Completeness: AND States
• Two transitions in parallel AND state triggers
by same event
• If truth value of the guard of one component
affects the truth value of the other guards, then
non-determinism may result.
• So RSML check for such dependencies.
• Costly to check, but rare in TCAS
specifications.
SWE 623
Duminda Wijesekera
29
Completeness: Serial Composition
• Transition triggering one event may trigger
another event.
• In order to achieve this effect, the the
domain of the second must be included in
the range of the first.
• Thirdly, if an event is generated as a
consequence of some action, and it is never
caught any where else, then the
specification is incomplete.
SWE 623
Duminda Wijesekera
30
Consequences
• RSML specs are now the official specs for TCAS II.
• There are some tools to check d-completeness.
• Many incomplete specifications were detected during
analysis phase.
• It is difficult to provide guidance in eliminating
incompleteness's and inconsistencies.
• Sensitivity of the TCAS system: How close an intruder
is allowed to get? RSML specifications can be
parametrized on sensitivity levels. –
• Sensitivity analysis.
SWE 623
Duminda Wijesekera
31