Sqp 2005 L5 Defect Detection 2003

2162ICT Software Quality Principles

Detecting Defects in Functional Requirements Geoff Dromey Software Quality Institute GRIFFITH UNIVERSITY

© R.G.Dromey, Griffith University, 2005

QUESTION Why should we be interested in detecting defects in function requirements?

Two Reasons 1.

65 – 85% of all software defects can ultimately be traced back to defects in the functional requirements.

3.

The earlier a defect is detected and removed the less costly it is to fix. (Fixing defects in released software can sometimes cost 10 to 100 times that of fixing the problem at the point of injection).

NASA – Case Study ◆

Studied the impact of varying levels of effort to remove errors in the requirements phase.

◆ Assessed

runs.

against cost over-

The Lesson from this “The more you invest in sorting out requirements problems the lower the risk of cost over-runs” “65 – 85% problems can be traced back to requirements” - Daniel Berry – NASA Study Requirements Translation & integration makes this practical and effective.

Nature of Requirements Defects In abstract logical terms functional requirements defects ultimately boil down to: ◆ Incompleteness problems ◆ Inconsistency problems ◆ Redundancy problems

Incompleteness

What is Incompleteness? Incompleteness manifests itself in many different ways both in text and in formal notations like behavior trees. It usually is much easier to detect requirements problems in a formal notation than in text.

Incompleteness - Examples ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆

Missing cases/alternatives Missing preconditions (or too weak/strong) Missing events Missing component-states Missing constraints Missing behavior fragments Missing sources or sinks Missing data descriptions

Inconsistency

What is Inconsistency? ◆

Inconsistency means there is conflict, disagreement or variation among a set of facts, behaviors or constraints.

◆

Alternatively, the conflict, disagreement or variation can be within a single fact, behavior or constraint.

Inconsistency - Examples Aliasing – calling same thing by different names ◆ Logical contradictions (or inaccuracies) between statements about a particular behavior/constraint ◆

Redundancy

What is Redundancy? ◆

Redundancy is the complement or dual or opposite of incompleteness.

◆

It means that some behavior/constraint is included more than once. Redundant behavior is unnecessary.

◆

It can cause confusion when carrying out requirements integration, and other steps etc.

Redundancy - Examples ◆

In describing two or more behavior fragments the same information is included more than once

◆

There is overlap in the description of behavior fragments

◆

Preconditions, constraints or other behavior, that is logically unnecessary or redundant are included.

STRATEGIES FOR REQUIREMENTS DEFECT DETECTION 1. 2. 3. 4. 5. 6. 7. 8. 9.

Requirements translation (to BTs) Requirements Integration (of BTs) Condition/case analysis of DBT Event Analysis of DBT DBT Leaf Node recursion check Component Interaction Analysis (state-to-state) Component Behavior Projection (CBT) CBT Leaf Node recursion check Component state set analysis

REQUIREMENTS TRANSLATION

Defects In Natural Language Functional Requirements

Inconsistency – “set” & “activated” S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo llo w in g d e ta ils a p p ly : R 1 . T h e s e c u r ity a la r m h a s a d e te c to r th a t s e n d s a tr ip s ig n a l w h e n m o tio n is d e te c te d . R 2 . T h e s e c u r ity a la r m is a c tiva te d b y p r e s s in g th e S e t b u tto n . R 3 . T h e se t b u tto n i s i l l u m i n a te d w h e n th e se c u ri ty a l a rm i s se t. R 4 . I f a t r i p s i g n a l o c c u r s w h i l e t h e s e c u r i t y a l a r m is s e t, a h ig h - p itc h e d to n e ( a la r m ) is e m itte d .

R5. R6. R7.

A th r e e - d ig it c o d e m u s t b e e n te r e d to tu r n o ff th e a la r m to n e . C o r r e c t e n tr y o f th e c o d e d e a c tiva te s th e s e c u r ity a la r m . If a m is ta ke is m a d e w h e n e n te r in g th e c o d e , th e u s e r m u s t p r e s s th e C le a r b u tto n b e fo r e th e c o d e c a n b e r e e n te r e d .

Inconsistency – “set” & “activated” S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo l lo w i n g d e ta il s a p p ly :

R 2 . T h e s e c u r i t y a la r m i s a c t i v a t e d b y p r e s s in g th e S e t b u tto n . R 3 . T h e s e t b u t t o n i s i llu m i n a t e d w h e n t h e s e c u r i t y a la r m i s s e t . Aliasing Problem

2.2.1 Report Satellite Health Satellite health information is requested to aid in planning required satellite maintenance. MG2) The SCS shall process each HR (satellite health request) command message received from the GCS. MG2.1) An HR command message shall be the first message received after the initiation of each "Manage Satellites" transaction. MG2.2) The SCS may receive a satellite health request message anytime during a "Manage Satellites" transaction. (Describes order during transaction.) MG2.3) A satellite health request command message will only be accepted by the SCS during an active "Manage Satellites" transaction. (Describes condition under which an HR may be received.) MG3) The SCS shall prepare and send an HA (satellite health acknowledgment) message to the GCS in response to an HR (satellite health request) command message.

Inconsistency – “first” & “anytime” 2.2.1 Report Satellite Health

Satellite health information is requested to aid in planning required satellite maintenance. MG2.1) An HR command message shall be the first message received after the initiation of each "Manage Satellites" transaction. MG2.2) The SCS may receive a satellite health request message anytime during a "Manage Satellites" transaction. (Describes order during transaction.) Possible contradiction between “first” and “anytime”

Ambiguity – “first” & “anytime” 2.2.1 Report Satellite Health

Satellite health information is requested to aid in planning required satellite maintenance. MG2.1) An HR command message shall be the first message received after the initiation of each "Manage Satellites" transaction. MG2.2) The SCS may receive a satellite health request message anytime during a "Manage Satellites" transaction. (Describes order during transaction.) Is there only one HR message – can there be more than one?

Incomplete – “HR - undefined” 2.2.1 Report Satellite Health

Satellite health information is requested to aid in planning required satellite maintenance. MG2.1) An HR command message shall be the first message received after the initiation of each "Manage Satellites" transaction. MG2.2) The SCS may receive a satellite health request message anytime during a "Manage Satellites" transaction. (Describes order during transaction.)

HR message – undefined structure and content

Issues 2.2.1 Report Satellite Health Reference MG2.1 MG2.2

MG2.3 MG3 Integration*

Description The HR message is undefined in terms of its content/structure Conflict/ambiguity between MG2.1 and MG2.2 because 2.1 says HR is first message and 2.2 says SCS can receive HR “any time” during a “manage satellites” transaction. Question is can it receive more than one HR during a “manage Satellites”? and because of “any time” can it interrupt other messages Does not say what should happen if a HR is rejected. Also not clear what system state it then reverts to. “Received” and “accepted” appear muddled. The HA message is undefined in terms of its content/structure While is clear when HR starts the uncertainty about more than one HR message during a maintenance time-slot causes integration problems.

Classification Undefined Ambiguity

Incomplete Undefined

Assumptions 2.2.1 Report Satellite Health Reference MG2 Integration

Description Assumed HR-processed only when HA has been sent. Assumed only one HR per maintenance time-slot. This may or may not be correct.

State - start SYSTEM[Manage Satellites.1]

2 . 2 . 1 R e p o r t S a t e l li t e H e a l t h

M G 2 .1 C

S Y S TEM [ M a n a g e S a t e llit e s . 1 ]

M G 2 .1 C

GCS ??

---

??

M G 2 .2 C

SCS > HR <

M G 2 .3 C

S Y S TEM ? M a n a g e S a t e llit e s ?

M G 2 .3 C

? N O T : M a n a g e S a te llite s ?

M G 2 .3 C

SCS [ H R -Pro c e s s e d ]

M G 2 .3 C

SCS [ H R - R e je c t e d ]

M G3

SCS [H A - P r e p a r e d ]

M G 2 .3 C

S Y S TEM

M G3

SCS < HA >

M G3

GCS > HA <

M G2

S Y S TEM [H R - P r o c e s s e d .2 ]

H R : U n d e fin e d

S Y S TEM

???

H A : U n d e fin e d

INCOMPLETENESS PROBLEMS

Missing Precondition

Missing Precondition A functional requirement will frequently neglect to state the precondition for the behavior it encapsulates.

Missing Precondition Missing preconditions can be detected either at the requirements translation stage or subsequently when we try to integrate the requirements into the design behavior tree and find we cannot do so.

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c tio n a l R e q u ir e m e n ts T h e fo llo w in g d e t a ils a p p ly : R 1 . T h e s e c u r ity a la r m h a s a d e te c to r th a t s e n d s a tr ip s ig n a l w h e n m o tio n is d e te c te d . R 2 . T h e s e c u r ity a la r m is a c tiva te d b y p r e s s in g th e S e t b u tto n . R 3 . T h e se t b u tto n i s i l l u m i n a te d w h e n th e se c u ri ty a l a rm i s se t. R 4 . I f a t r i p s i g n a l o c c u r s w h i l e t h e s e c u r i t y a l a r m is s e t, a h ig h - p itc h e d to n e ( a la r m ) is e m itte d .

R5. R6. R7.

A th r e e - d ig it c o d e m u s t b e e n te r e d to tu r n o ff th e a la r m to n e . C o r r e c t e n tr y o f th e c o d e d e a c tiva te s th e s e c u r ity a la r m . If a m is ta ke is m a d e w h e n e n te r in g th e c o d e , th e u s e r m u s t p r e s s th e C le a r b u tto n b e fo r e th e c o d e c a n b e r e e n te r e d .

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo llo w in g d e ta ils a p p ly :

R1.

T h e s e c u rity a la rm h a s a d e te c to r th a t s e n d s a trip s ig n a l w h e n m o tio n is d e te c te d .

Missing Precondition

R1

D ETEC TOR ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TOR < T r ip - S ig n a l >

Does not say what condition(s) must apply for motion to be detected and a trip-signal sent

Strategy for Detection Always ask the question for each FR: “What precondition must exist for this behavior to happen?” ◆

Domain knowledge or context used to resolve such problems.

Precondition Added R1 +

S E C U R IT Y - A L A R M [ A c tiva te d ]

R1

D ETEC TOR ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TOR < T r ip - S ig n a l >

The detector can only usefully perform it function as part of the system if the security alarm is first activated

Missing Precondition - Actor Frequently missing precondition correspond to leaving out the actor the initiates or performs the action. Example:

When the door is opened the light goes on.

Missing Precondition

R1

D OOR [OPEN ]

R1

L IG H T [On ]

Does not say who/what causes the door to open

Strategy for Detection Always ask the question for each FR: “What (or who) may have caused the behavior to happen?” ◆

Domain knowledge or context used to resolve such problems.

Precondition Added R1 +

U SER ?? D O O R [ O pen] ??

R1

D OOR [ O pen ]

R1

L IG H T [On ]

The USER causes the behavior to happen

Missing Postcondition

Missing Postcondition A functional requirement will sometimes neglect to state or incorporate the postcondition for the behavior it encapsulates.

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c tio n a l R e q u ir e m e n ts T h e fo llo w in g d e t a ils a p p ly : R 1 . T h e s e c u r ity a la r m h a s a d e te c to r th a t s e n d s a tr ip s ig n a l w h e n m o tio n is d e te c te d . R 2 . T h e s e c u r ity a la r m is a c tiva te d b y p r e s s in g th e S e t b u tto n . R 3 . T h e se t b u tto n i s i l l u m i n a te d w h e n th e se c u ri ty a l a rm i s se t. R 4 . I f a t r i p s i g n a l o c c u r s w h i l e t h e s e c u r i t y a l a r m is s e t, a h ig h - p itc h e d to n e ( a la r m ) is e m itte d .

R5. R6. R7.

A th r e e - d ig it c o d e m u s t b e e n te r e d to tu r n o ff th e a la r m to n e . C o r r e c t e n tr y o f th e c o d e d e a c tiva te s th e s e c u r ity a la r m . If a m is ta ke is m a d e w h e n e n te r in g th e c o d e , th e u s e r m u s t p r e s s th e C le a r b u tto n b e fo r e th e c o d e c a n b e r e e n te r e d .

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo llo w in g d e ta ils a p p ly :

R1.

T h e s e c u rity a la rm h a s a d e te c to r th a t s e n d s a trip s ig n a l w h e n m o tio n is d e te c te d .

Missing Postcondition

R1

D ETEC TOR ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TOR < T r ip - S ig n a l >

Does not say where trip-signal is sent

Missing Postcondition R1 +

S E C U R IT Y - A L A R M [ A c tiva te d ]

R1

D ETEC TOR ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TOR < T r ip - S ig n a l >

Does not say where trip-signal is sent

Strategy for Detection Always ask the question for each FR: “Is the behavior self-contained and complete – if not what is missing?” ◆

Domain knowledge or context used to resolve such problems. Anything sent should also be received, etc.

Postcondition Added R1 +

S E C U R IT Y - A L A R M [ A c tiva te d ]

R1

D ETEC TOR ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TOR < T r ip - S ig n a l >

R1 +

S E C U R IT Y _ A L A R M > T r ip - S ig n a l <

CONDITION or CASE ANALYSIS of DBT

Missing Cases/Alternatives

FR5

CAR-SYSTEM Integrated Functional Requiremnts

C A R -S Y S T E M [L o c ke d ]

FR4

S E C U R IT Y - A L A R M [O n ]

FR5

D R IV E R ? ? P r e s s e s - K e y? ?

FR4

W IN D O W ? ? B r o ke n ? ?

FR5

KEY [P r e s s e d ]

FR4

D OOR ??F orced??

FR4

S E C U R IT Y - A L A R M [S o u n d i n g ]

FR2

SEAT ? ? O c c u p ie d ? ?

FR2

S E A T -B E LT ? N o t- F a s te n e d ?

FR2

D A S H - L IG H T [O n ]

FR5

D OOR [U n l o c k e d ]

FR5

C A R -S Y S T E M [U n l o c k e d ]

FR6

D R IV E R ? ? G e ts - In - C a r ? ?

FR6

D R IV E R ? ? P u ts - C a r - i n - P a r k? ?

FR1

C A R -S Y S T E M [ P ark ]

FR1

D R IV E R ? ? In s e r ts - K e y? ?

FR1

D R IV E R ? ? T u r n s - K e y? ?

FR1

IG N IT IO N [o n ]

FR1

C A R -S Y S T E M [S ta r te d ]

FR5

S E C U R IT Y - A L A R M [O ff]

FR3

H A N D -B R A K E ?O n?

FR3

B R A K E - L IG H T [O n ]

CAR-SYSTEM Missing Cases

FR2

SEAT ? ? O c c u p ie d ? ?

FR2

S E A T -B E LT ? N o t- F a s te n e d ?

FR2

D A S H - L IG H T [O n ]

FR1

IG N IT IO N [o n ]

FR1

C A R -S Y S T E M [S ta r te d ]

FR3

H A N D -B R A K E ?O n?

FR3

B R A K E - L IG H T [O n ]

CLAIM It is much easier to detect incompleteness and inconsistency defects in a formal representation of functional requirements like behavior trees than in their natural representation.

“A man’s thought varies according to the language in which he speaks” Schopenhauer

My take on this.

“We change what we see and the way we think when we change representations”

EVENT ANALYSIS of DBT

Event Incompleteness Detection

Missing Events A statement of requirements that contains events will frequently leave out important requirements where a mentioned event needs to occur in some other part of the system.

Microwave Oven – Shlaer & Mellor   STATEMENT OF REQUIREMENTS 1. There is a single control button available for the user of the oven. If the oven is idle with the door is closed and you push the button, the oven will start cooking (that is, energize the power-tube for one minute). 2. If the button is pushed while the oven is cooking it will cause the oven to cook for an extra minute. 3. Pushing the button when the door is open has no effect (because it is disabled). 4. Whenever the oven is cooking or the door is open the light in the oven will be on. 5. Opening the door stops the cooking. Event 6. Closing the door turns off the light. This is the normal idle state, prior to cooking when the user has placed food in the oven. 7. If the oven times-out the light and the power-tube are turned off and then a beeper emits a sound to indicate that the cooking is finished.

Example: Missing Event Mentioned Event: User can open door when oven is cooking. Missing Event: User can open door when oven is idle.

L IG H T [O n ]

4C

1

U SER ? ? B u tto n - P u s h ? ?

1

BU TTON [P u s h e d ]

1

P O W E R -T U B E [E n e r g iz e d ]

1

OVEN [C o o kin g ]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTON [P u s h e d ]

2

O VEN [E x tr a - M i n u te ]

5

2

OVEN * [C o o kin g ]

6

OVEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D OOR [C lo s e d ]

6

L IG H T [O ff]

1

OVEN [Id le ]

BU TTO N [E n a b le d ]

3C

M is s in g E v e n t U ser can open door w h e n O v e n is Id le

7

O VEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

D OOR [O p e n ]

7

BEEPER [S o u n d e d ]

5

P O W E R -T U B E [O ff]

7

O VEN [C o o kin g - F in is h e d

5

OVEN [C o o kin g - S to p p e d ]

5

U SER ??D oor-O pened??

7

L IG H T [O ff]

3C

BU TTON [D is a b le d ]

QUESTION Is there a systematic process we can use to detect missing events?

STRATEGY Use event precondition weakening

Event Precondition Weakening ◆

Identify the precondition for an event.

◆

Weaken the event precondition

◆

Use domain knowledge to see if event can occur.

Example: Event Precondition Event: User can open door when oven is cooking. Precondition: Oven[Cooking] = DOOR[Closed] ∧ LIGHT[On] ∧ POWER-TUBE[On]

Example: Event Precondition Precondition: Oven[Cooking] = DOOR[Closed] ∧ LIGHT[On] ∧ POWER-TUBE[On]

Weaker Precondition: = DOOR[Closed]

Example: Event Precondition Weaker Precondition: = DOOR[Closed] Process Look for places where this precondition holds and see if the “user opens door event is applicable”.

Missing Event Included

L IG H T [O n ]

4C

6

O VEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D OOR [C lo s e d ]

6

L IG H T [O ff]

1

O VEN [Id le ]

BU TTON [E n a b l e d ]

3C

1

U SER ? ? B u tto n - P u s h ? ?

8

U SER ??D oor-O pened??

1

BU TTON [P u s h e d ]

8

D OOR [O p e n ]

1

P O W E R -T U B E [E n e r g iz e d ]

1

OVEN [C o o kin g ]

L IG H T [O n ]

4C

M is s in g E vent

8

BU TTON [D is a b le d ]

8

O VEN ^ [O p e n ]

7

OVEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTON [P u s h e d ]

2

OVEN [E x tr a - M i n u te ]

5

D OOR [O p e n ]

7

BEEPER [S o u n d e d ]

2

O VEN * [C o o kin g ]

5

P O W E R -T U B E [O ff]

7

OVEN [C o o kin g - F in is h e d

5

O VEN [C o o kin g - S to p p e d ]

5

U SER ??D oor-O pened??

7

L IG H T [O ff]

3C

BU TTON [D is a b le d ]

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo llo w in g d e ta ils a p p ly : R 1 . T h e s e c u r ity a la r m h a s a d e te c to r th a t s e n d s a tr ip s ig n a l w h e n m o tio n is d e te c te d . R 2 . T h e s e c u r ity a la r m is a c tiva te d b y p r e s s in g th e S e t b u tto n . R 3 . T h e se t b u tto n i s i l l u m i n a te d w h e n th e se c u ri ty a l a rm i s se t. R 4 . I f a t r i p s i g n a l o c c u r s w h i l e t h e s e c u r i t y a l a r m is s e t, a h ig h - p itc h e d to n e ( a la r m ) is e m itte d .

R5. R6. R7.

A th r e e - d ig it c o d e m u s t b e e n te r e d to tu r n o ff th e a la r m to n e . C o r r e c t e n tr y o f th e c o d e d e a c tiva te s th e s e c u r ity a la r m .

Event

If a m is ta ke is m a d e w h e n e n te r in g th e c o d e , th e u s e r m u s t p r e s s th e C le a r b u tto n b e fo r e th e c o d e c a n b e r e e n te r e d .

Example: Missing Event Mentioned Event: User can enter 3-digit code and turn off alarm when it is sounding. Missing Event: User can turn off alarm when it is Activated but not sounding.

R1

D ET E C T O R || ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TO R < T r ip - S ig n a l >

R 2 @ +

S E C U R IT Y -A L A R M [ D e a c tiv a te d ]

R2

U SER ? ? [p r e s s e s ]S e t- B u tto n ? ?

R2

S E T -B U T T O N [ P ressed ]

R 2 @

S E C U R I T Y -A L A R M [ A c tiva te d ]

R3

S E T -B U T T O N [ Illu m in a te d ]

R9

S E T -B U T T O N [ N O T : Illu m in a te d ]

M IS S IN G EVENT U s e r c a n e n te r 3 -d ig it c o d e a n d tu r n o ff th e a la r m w h e n it is a c tiv a te d b u t n o t s o u n d in g

R 1 @ +

S E C U R IT Y -A L A R M > T rip -S i g n a l <

R4 @

S E C U R IT Y -A L A R M [ H ig h -P itc h e d -T o n e ]

R5 +

U SER = ? ? < 3 - D ig it- C o d e > ? ?

R 5 @

S E C U R IT Y -A L A R M > 3 -D ig i t-C o d e <

R 6

S E C U R IT Y -A L A R M ? 3 -D i g i t -C o d e [ C o rre c t ] ?

R 7

S E C U R IT Y -A L A R M ? 3 -D i g i t-C o d e [In c o rre c t ]?

R 6 +

S E C U R IT Y -A L A R M [N O T :H i g h -P i tc h e d -T o n e ]

R7

U SER ?? C LE A R [ P ressed ] ??

R6

S E C U R IT Y -A L A R M ^ [ D e a c tiva te d ]

R7

C LEAR [ Pressed ]

R7 +

U SER ^ ? ? < 3 - D ig it- C o d e > ? ?

Event Precondition Weakening ◆

Identify the precondition for an event.

◆

Weaken the event precondition

◆

Use domain knowledge to see if event can occur.

Example: Missing Event Mentioned Event: User can enter 3-digit code and turn off alarm when it is sounding. Missing Event: User can turn off alarm when it is Activated but not sounding.

Example: Missing Event Event: User can enter 3-digit code and turn off alarm when it is sounding. Precondition: = SECURITY-ALARM[High-Pitched-Tone]

Example: Event Precondition Precondition: = SECURITY-ALARM[High-Pitched-Tone]

Weaker Precondition: = SECURITY-ALARM[Activated]

Example: Event Precondition Weaker Precondition: = SECURITY-ALARM[Activated]

Process Look for places where this precondition holds and see if the “user enters 3-digit code event is applicable”.

Missing Event Included

R2 @ +

S E C U R IT Y -A L A R M [ D e a c ti v a te d ]

R2

U SER ? ? [p r e s s e s ]S e t- B u tto n ? ?

R2

S E T -B U T T O N [ P ressed ]

R2 @

S E C U R IT Y -A L A R M [ A c ti v a te d ]

R3

S E T -B U T T O N [ Illu m in a te d ]

R1

D E T E C T O R || ? ? M o tio n - d e te c te d ? ?

R1

D ETEC TOR < T r ip - S ig n a l >

R 1 @ +

S E C U R IT Y -A L A R M > T ri p -S ig n a l <

R4 @

S E C U R IT Y -A L A R M [ H i g h -P i tc h e d -T o n e ]

R5 +

U SER = ? ? < 3 - D ig it- C o d e > ? ?

R 5 @

S E C U R I T Y -A L A R M > 3 -D i g i t -C o d e <

R 6

S E C U R I T Y -A L A R M ? 3 -D i g i t -C o d e [C o rre c t ] ?

R7

S E C U R I T Y -A L A R M ? 3 -D i g i t-C o d e [ I n c o rre c t ]?

R 6 +

S E C U R I T Y -A L A R M [N O T :H i g h -P i t c h e d -T o n e ]

R7

U SER ?? C LE A R [ P ressed ] ??

R6

S E C U R I T Y -A L A R M ^ [ D e a c ti v a te d ]

R7

C LE A R [ P ressed ]

R7 +

U SER ^ ? ? < 3 - D i g i t- C o d e > ? ?

R9

S E T -B U T T O N [ N O T : Illu m in a te d ]

R8 -

U S E R = || ? ? < 3 - D ig it- C o d e > ? ?

M is s in g Event

Initialization Problems and Checkout Process

Initialization and the DBT It is very important to pay attention to the initialization of component’s states when setting up and implementing from design behavior trees – otherwise the behavior of the system will have defects.

Example – Microwave DBT With this DBT it can start out either in an “open” or an “idle” state as potential start ($) states for the system. However the OVEN[Open] state is undefined in terms of its component’s states – whereas OVEN[Idle] is defined.

Missing Initialization

L IG H T [O n ]

4C

6

O VEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D OO R [C lo s e d ]

6

L IG H T [O ff]

6

OVEN [Id le ]

BU TTON [E n a b le d ]

3C

1

U SER ? ? B u tto n - P u s h ? ?

8

U SER ??D oor-O pened??

1

BU TTON [P u s h e d ]

8

D O OR [O p e n ]

1

P O W E R -T U B E [E n e r g iz e d ]

1

O VEN [C o o kin g ]

L IG H T [O n ]

4C

3C

BU TTON [D is a b le d ]

3C

O VEN [O p e n ]

7

O VEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTO N [P u s h e d ]

2

OVEN [E xtr a - M in u te ]

5

D O OR [O p e n ]

7

BEEPER [S o u n d e d ]

2

OVEN * [C o o kin g ]

5

P O W E R -T U B E [O ff]

1

O VEN [C o o kin g - F in is h e d

5

OVEN [C o o kin g - S to p p e d ]

5

U SER ??D oor-O pened??

7

L IG H T [O ff]

3C

BU TTON [D is a b le d ]

Missing Initialization

1

U SER ? ? B u tto n - P u s h ? ?

6

OVEN $ [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D O OR [C lo s e d ]

6

L IG H T [O ff]

6

O VEN $ [Id le ]

W h e n t h e O v e n S y s t e m t r a n s it io n s fr o m " O p e n " t o " Id le " fo u r c o m p o n e n t s - u s e r , d o o r , lig h t , a n d b u t t o n r e a liz e s t a t e s . In it ia liz a t io n m u s t a c c o u n t f o r t h e s t a t e v a lu e s o f e a c h o f t h e s e c o m p o n e n t s p r io r t o t h e ir r e s p e c t iv e s t a t e c h a n g e s .

3C

8

BU TTO N [E n a b le d ]

U SER ??D oor-O pened??

Missing Initialization U SER [ D oor-O pen] D OOR [ O pen ] BU TTON [ D is a b le d ] L IG H T [On ]

Missing Initialization Added U SER [ D oor-O pen] D OOR [ O pen ]

R e q u ir e d In itia liz a tio n fo r M ic r o w a v e O v e n

BU TTON [ D is a b le d ] L IG H T [On ]

1

U SER ? ? B u tto n - P u s h ? ?

6

OVEN $ [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D OOR [C lo s e d ]

6

L IG H T [O ff]

6

OVEN $ [Id l e ]

3C

8

BU TTON [E n a b le d ]

U SER ??D oor-O pened??

Initialization Checkout Process To find the appropriate component initializations for the root-node systemstate of a DBT we identify which components achieve states in transitioning from the root node to some other system state(s). These components need to be initialized

LEAF-NODE REVERSION CHECK of DBT

Missing Leaf-Nodes

L IG H T [O n ]

4C

6

O VEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D OO R [C lo s e d ]

6

L IG H T [O ff]

6

OVEN [Id le ]

BU TTON [E n a b le d ]

3C

1

U SER ? ? B u tto n - P u s h ? ?

8

U SER ??D oor-O pened??

1

BU TTON [P u s h e d ]

8

D O OR [O p e n ]

1

P O W E R -T U B E [E n e r g iz e d ]

1

O VEN [C o o kin g ]

L IG H T [O n ]

4C

3C

BU TTON [D is a b le d ]

3C

O VEN [O p e n ]

7

O VEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTO N [P u s h e d ]

2

OVEN [E xtr a - M in u te ]

5

D O OR [O p e n ]

7

BEEPER [S o u n d e d ]

2

OVEN * [C o o kin g ]

5

P O W E R -T U B E [O ff]

1

O VEN [C o o kin g - F in is h e d

5

OVEN [C o o kin g - S to p p e d ]

5

U SER ??D oor-O pened??

7

L IG H T [O ff]

3C

BU TTON [D is a b le d ]

Missing Leaf-Nodes 2

U SER ? ? B u tto n - P u s h ? ?

7

OVEN ? ? T im e d - O u t ? ?

2

BU TTON [P u s h e d ]

7

P O W E R -T U B E [O ff]

2

OVEN [E xtr a - M in u te ]

5

D OOR [O p e n ]

7

BEEPER [S o u n d e d ]

2

OVEN * [C o o kin g ]

5

P O W E R -T U B E [O ff]

1

OVEN [C o o kin g - F in is h e d

5

OVEN [C o o kin g - S to p p e d ]

5

U SER ??D oor-O pened??

7

L IG H T [O ff]

3C

BU TTON [D is a b le d ]

First Attempt at Defect Correction

Missing Leaf-Nodes 7

OVEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTON [P u s h e d ]

2

OVEN [E xtr a - M in u te ]

5

D OOR [O p e n ]

7

BEEPER [S o u n d e d ]

2

OVEN * [C o o kin g ]

5

P O W E R -T U B E [O ff]

1

OVEN [C o o k in g - F in is h e d

5

OVEN [C o o k in g - S to p p e d ]

7

OVEN ^ [ Id le ]

Added R e v e r s io n B e h a v io r

5

U SER ??D oor-O pened??

7

5

OVEN ^ [ O pen ]

L IG H T [O ff]

3C

BU TTON [D is a b le d ]

Added R e v e r s io n B e h a v io r

Complete System

Oven Component Behavior

1

6

OVEN [O p e n ]

1

O VEN [Id le ]

OVEN [C o o k in g ]

6

OVEN ^ [O p e n ]

2

OVEN [E xtr a - M in u te ]

5

OVEN [C o o k in g - S to p p e d ]

7

O VEN [T im e d - O u t]

2

OVEN ^ [C o o kin g ]

5

O VEN ^ [ O pen ]

1

O VEN [C o o kin g - F in is h e d

5

REQUIREMENTS Missing Original

OVEN ^ [ Id le ]

Reversion Inconsistency Defect

Reversion Inconsistency Simply adding system-state leaf nodes is not the complete solution to this kind of defect – we need to check that the corresponding composite component behavior resulting from the reversion is consistent.

Reversion Inconsistency

L IG H T [O n ]

4C

1

6

OVEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D O OR [C lo s e d ]

6

L IG H T [O ff]

6

OVEN [Id l e ]

1

U SER ? ? B u tto n - P u s h ? ?

8

U SER ??D oor-O pened??

1

BU TTON [P u s h e d ]

8

D OOR [O p e n ]

1

P O W E R -T U B E [E n e r g iz e d ]

L IG H T [O n ]

4C

OVEN [C o o kin g ]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTON [P u s h e d ]

2

OVEN [E xtr a - M in u te ]

5

2

O VEN * [C o o k in g ]

Simply adding the reversion OVEN^[Idle] would fail to restore BUTTON[Enabled]

BU TTO N [E n a b le d ]

3C

3C

BU TTO N [D is a b le d ]

3C

OVEN [O p e n ]

7

OVEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

D OO R [O p e n ]

7

BEEPER [S o u n d e d ]

5

P O W E R -T U B E [O ff]

1

OVEN [C o o kin g - F in is h e d

5

OVEN [C o o k in g - S to p p e d ]

7

OVEN ^ [ Id le ]

7

OVEN ^ [ Id le ]

5

U SER ??D oor-O pened??

7

3C

L IG H T [O ff]

BU TTON [D is a b le d ]

M IS S IN G

Reversion Inconsistency There are two ways to tackle and overcome reversion inconsistency problems: (a) Compare

system state definitions (b) Make sure the behavior of ALL components in a DBT are consistent and complete

Reversion Defect - Strategy (a)

Compare System-State definitions for inconsistencies with their component states.

Reversion Inconsistency O r ig in a l - " Id le " S t a t e

6

OVEN [Id l e ]

6

D OOR [C lo s e d ]

6

L IG H T [ O ff ]

3C

BU TTON [E n a b le d ]

R e v e r s io n - " Id le " S t a t e 7

OVEN ^ [Id le ]

1

BU TTON [ P ushed ]

6

D OO R [C lo s e d ]

7

P O W E R -T U B E [ O ff ]

7

L IG H T [ O ff ]

7

BEEPER [ S ounded ]

Reversion Inconsistency Simply applying the OVEN^[Idle] reversion Would leave the button in the residual state BUTTON[Pushed] Whereas to be consistent with the original OVEN[Idle] state it needs the button to be in BUTTON[Enabled]

Lesson Learned What we have learned from this example is that when a component realizes a System State either by reversion or initially the states associated with the components that define that behavior must be compared to make sure that they are consistent – such a comparison often identifies missing behaviour as our example has illustrated

Reversion Inconsistency Corrected

L IG H T [O n ]

4C

1

6

OVEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D O OR [C lo s e d ]

6

L IG H T [O ff]

6

OVEN [Id l e ]

1

U SER ? ? B u tto n - P u s h ? ?

8

U SER ??D oor-O pened??

1

BU TTON [P u s h e d ]

8

D OOR [O p e n ]

1

P O W E R -T U B E [E n e r g iz e d ]

L IG H T [O n ]

4C

OVEN [C o o kin g ]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTON [P u s h e d ]

2

OVEN [E xtr a - M in u te ]

5

2

O VEN * [C o o k in g ]

Simply adding the reversion OVEN^[Idle] would fail to restore BUTTON[Enabled]

BU TTO N [E n a b le d ]

3C

3C

BU TTO N [D is a b le d ]

3C

OVEN [O p e n ]

7

OVEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

D OO R [O p e n ]

7

BEEPER [S o u n d e d ]

5

P O W E R -T U B E [O ff]

1

OVEN [C o o kin g - F in is h e d

5

OVEN [C o o k in g - S to p p e d ]

7

OVEN ^ [ Id le ]

7

OVEN ^ [ Id le ]

5

U SER ??D oor-O pened??

7

3C

L IG H T [O ff]

BU TTON [D is a b le d ]

M IS S IN G

7

BU TTON [E n a b le d ]

Reversion Defect - Strategy (b)

Make sure the behaviour of each component is consistent and complete.

Projected Component - Incomplete Raw projected BUTTON Component – has a number of defects

1

2

BU TTON { P ushed }

3C

BU TTON { P ushed }

3C

BU TTON [E n a b le d ]

3C

BU TTON { D is a b le d }

BU TTON { D is a b le d }

ISSUE

L IG H T [O n ]

4C

1

6

O VEN [ O pen ]

6

U SER ? ? D o o r - C lo s e d ? ?

6

D OO R [C l o s e d ]

6

L IG H T [O ff]

6

O VEN [Id le ]

BU TTON [E n a b l e d ]

3C

1

U SER ? ? B u tto n - P u s h ? ?

8

U SER ??D oor-O pened??

1

BU TTON [P u s h e d ]

8

D OO R [O p e n ]

1

P O W E R -T U B E [E n e r g iz e d ]

L IG H T [O n ]

4C

OVEN [C o o kin g ]

2

U SER ? ? B u tto n - P u s h ? ?

2

BU TTO N [P u s h e d ]

2

OVEN [E xtr a - M in u te ]

5

2

O VEN * [C o o kin g ]

3C

BU TTO N [D i s a b l e d ]

3C

OVEN [O p e n ]

7

O VEN ? ? T im e d - O u t ? ?

7

P O W E R -T U B E [O ff]

D OOR [O p e n ]

7

BEEPER [S o u n d e d ]

5

P O W E R -T U B E [O ff]

1

O VEN [C o o kin g - F in is h e d

5

O VEN [C o o kin g - S to p p e d ]

7

O VEN ^ [ Id l e ]

7

O VEN ^ [ Id l e ]

5

U SER ??D oor-O pened??

7

3C

L IG H T [O ff]

BU TTON [D is a b le d ]

W h a t h a p p e n s to B U T T O N s ta te h e re ?

Projected Component - Corrected Implied reversions and missing behaviours are shown in yellow and red respectively. 3C

2

BU TTON ^ { Pushed }

1

BU TTON { Pushed }

3C

BU TTON ^ { D is a b le d }

7

BU TTON [E n a b le d ]

BU TTON ^ { E n a b le d }

3C

BU TTON { D is a b le d }

8

BU TTON ^ [ E n a b le d ]

Projected Component - Corrected Notice that after timing out Button needs to revert to the “Enabled” state rather than remain in the pushed state.

2

BU TTON ^ { P ushed }

1

BU TTON { Pushed }

3C

BU TTON ^ { D is a b le d }

3C

7

BU TTON [E n a b le d ]

BU TTON ^ { E n a b le d }

Originally Missing

3C

BU TTON { D is a b le d }

8

BU TTON ^ [ E n a b le d ]

Originally Missing

BUTTON - Projected Component - Corrected

3C

2

BU TTON ^ { P ushed }

1

BU TTON { Pushed }

3C

BU TTON ^ { D is a b le d }

7

BU TTON [E n a b le d ]

BU TTON ^ { E n a b le d }

3C

BU TTON { D is a b le d }

8

BU TTON ^ [ E n a b le d ]

Lesson Learned Here we had three alternative event branches emanating from a particular state OVEN[Cooking] but the original requirements indicated that the component BUTTON was changed in only two of the branches – this suggests a potential inconsistency and missing behaviour in the third event sub-tree – examination projected component behaviour and respective sub-trees can both show up this inconsistency and incompleteness problem. The incompleteness causes an inconsistency.

Missing Behavior

Missing Postcondition A functional requirement will sometimes neglect to state or incorporate the postcondition for the behavior it encapsulates.

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo llo w in g d e ta ils a p p ly : R 1 . T h e s e c u r ity a la r m h a s a d e te c to r th a t s e n d s a tr ip s ig n a l w h e n m o tio n is d e te c te d . R 2 . T h e s e c u r ity a la r m is a c tiva te d b y p r e s s in g th e S e t b u tto n . R 3 . T h e s e t b u t t o n i s i l l u m i n a t e d w h e n t h e s e c u r i t y a l a r m i s s e t . Implied R 4 . I f a t r i p s i g n a l o c c u r s w h i l e t h e s e c u r i t y a l a r m is s e t, a h ig h - p itc h e d to n e ( a la r m ) is e m itte d .

R5. R6. R7.

A th r e e - d ig it c o d e m u s t b e e n te r e d to tu r n o ff th e a la r m to n e . C o r r e c t e n tr y o f th e c o d e d e a c tiva te s th e s e c u r ity a la r m . If a m is ta ke is m a d e w h e n e n te r in g th e c o d e , th e u s e r m u s t p r e s s th e C le a r b u tto n b e fo r e th e c o d e c a n b e r e e n te r e d .

Security Alarm – Prowell, et al S E C U R IT Y A L A R M - F u n c t io n a l R e q u ir e m e n t s T h e fo llo w in g d e ta ils a p p ly :

R 3 . T h e s e t b u t t o n is illu m in a t e d w h e n t h e s e c u r it y a la r m is s e t .

Missing Behavior

R3 +

S E C U R IT Y - A L A R M [ A c tiva te d ]

R3

S E T -B U T T O N [ Illu m in a te d ]

From this we see that the Security Alarm and the Set Button Interact

This gives us the clue that there may be other State combinations for which they interact.

Missing Behavior Leaves out what should happen when the Security-Alarm is deactivated The fact that the Security Alarm and the Set Button are linked gives us a clue that there may be missing behavior.

Strategy for Detection Whenever architecture suggests two components interact we need to consider all state-to-state interactions ◆ This

allows us to detect missing behavior.

Security Alarm – Prowell, et al S E C U R IT Y _ A L A R M

DETECTO R

US ER

CLEA R

S ET-B U TTO N

Security Alarm – Prowell, et al C o m p o n e n ts S e c u r ity A la r m C a u s a lly A ffe c ts S E C U R IT Y _ A L A R M

DETECTO R

U S ER

S ET-B U TTO N

R U L E : C o m p le te n e s s C h e c k W h e n e v e r s e c u r ity a la r m in te r a c ts c a u s a lly w ith o n e o f th e s e th r e e c o m p o n e n ts , C H E C K if h a s a c a u s a l e f f e c t o n t h e o t h e r t w o . T h is r u le p ic k s u p p r o b le m th a t s e t-b u tto n n e e d s to g e ts tu rn e d o f f w h e n s e c u r ity - a la r m is d e a c tiv a te d .

Pairwise Component Interactions S E C U R IT Y - A L A R M /S E T - B U T T O N In t e r a c t io n M a t r ix S ET -B U T T O N C O M P O N EN T S E C U R I T Y A L A R M

IN T E R A C T IO N

Illu m in a t e d

A c tiv a te d

X

D e a c t iv a t e d

N O T :I l l u m i n a t e d

X

T r ip -s ig n a l

(X )

3 -d ig it -c o d e

(X )

H ig h -p itc h e d

(X )

N O T :H i g h - P i t c h e d

(X )

W h a t t h e ( ) s h o w is s t a t e is u n c h a n g e d w h e n g o t o t h e s e s t a t e s - is o n ly t w o c a u s a l s t a t e s . T h is c o m p le t e ly c a p t u r e s t h e s e m a n t ic s o f t h e in t e r a c t io n b e tw e e n th e tw o c o m p o n e n ts .

M is s in g B e h a v io r

Component Interaction Table S E C U R I T Y A L A R M

IN T E R A C T IO N

D ETEC TO R

A c t iv a te d

? ? M o t io n ? ?

D e a c t iv a te d

USER

S E T -B U T T O N

S E C U R IT Y - A L A R M

Il l u m i n a t e d ? ? S e t- B u tto n [P r e s s e d ]? ?

T r ip -s ig n a l

N O T :Illu m in a te d

A c t iv a t e d H ig h - P it c h e d

3 -d ig it- c o d e H ig h -p it c h e d N O T :H ig h - P it c h e d

? ? 3 - D ig it- C o d e ? ?

D e a c t iv a t e d

Behavior Added

R1

D ET EC T O R || ? ? M o tio n - d e te c te d ? ?

R2 @ +

S E C U R IT Y -A L A R M [ D e a c tiva te d ]

R2

U SER ? ? [p r e s s e s ]S e t- B u tto n ? ?

R2

S E T -B U T T O N [ P ressed ]

R 2 @

S E C U R IT Y -A L A R M [ A c tiv a te d ]

R3

S E T -B U T T O N [ Illu m in a te d ]

R9

S E T -B U T T O N [ N O T : Illu m in a te d ]

Missing Component Behavior

Complete System

Oven Component Behavior

1

6

OVEN [O p e n ]

1

O VEN [Id le ]

OVEN [C o o k in g ]

6

OVEN ^ [O p e n ]

2

OVEN [E xtr a - M in u te ]

5

OVEN [C o o k in g - S to p p e d ]

7

O VEN [T im e d - O u t]

2

OVEN ^ [C o o kin g ]

5

O VEN ^ [ O pen ]

1

O VEN [C o o kin g - F in is h e d

5

REQUIREMENTS Missing Original

OVEN ^ [ Id le ]

Inconsistency Defects

Inconsistency and Integration Requirements Integration helps find incompleteness problems but it DOES NOT prevent us from creating a design behavior tree (DBT) that contains inconsistent behavior

A Model for Inconsistency The clue to building a model for inconsistency is given by Kipling’s “six honest serving men” – who, what, why, when, where and how.

A Model for Inconsistency ◆Spacial

Inconsistency (where) - a person or object cannot be in two places at once. ◆Temporal Inconsistency (when) – an event can not happen at two different times in the same time zone

A Model for Inconsistency ◆Existential

Inconsistency (who) – cannot have two different people responsible for some actions. ◆Causal Inconsistency (how) – cannot have two different causes responsible for some behavior

Strong - Inconsistency Inconsistency arises in a description of behavior when a single component appears to occupy, at the same time, two states that are incompatible with our understanding of reality and our understanding of the use of language to describe reality. There is also a corresponding inconsistency for two components.

Weak - Inconsistency Inconsistency arises in a description of behavior when a single component appears to occupy, a sequence of states that are incompatible with our understanding of reality and our understanding of the use of language to describe reality. There is also a corresponding inconsistency for two components. Domain knowledge is needed to detect weak inconsistency.

Inconsistency and Domain Knowledge If someone said “it was 400C and snowing” most people would consider this to be inconsistent. However if you know nothing about snow then this may not seem inconsistent. Determining just what is inconsistent is an informal activity – not something that can be easily formalized.

Inconsistency – Basic Patterns C o m p o n e n t-S ta te P a tte rn

R e p r e s e n t a t io n f o r D e t e c t io n

( i)

A [s 1 ] ∧ A [s 2 ]

R u n n in g S y s t e m - s t a t e

( ii)

A [s 1 ] ∧ B [s 2 ]

R u n n in g S y s t e m - s t a t e

( iii)

A [s 1 ] → A [s 2 ]

CBT

( iv ) A [ s 1 ] → B [ s 2 ]

DBT

(v ) A [s 1 ] → ... → A [s 2 ]

CBT

( v i) A [ s 1 ] → . . . → B [ s 2 ]

DBT

All more complex inconsistencies are built from these primitive inconsistency patterns.

Example – Inconsistency Detection

Detecting Inconsistencies in DBTs

Use of behaviorally complete running system states is an important representation for finding many types of inconsistency problems.

Inconsistent Requirements R 1 . W h e n e v e r t h e d o o r is o p e n e d t h e lig h t g o e s o f f . R 2 . W h e n a c u s to m e r a p p ro a c h e s , th e d o o r o p e n s w h ic h c a u s e s t h e lig h t t o g o o n a n d t h e b u z z e r to s o u n d .

Inconsistent Requirements - RBTs R1 C

R1 C

D OOR [Open ]

R2

C U STOMER ? ? A p p ro a c h e s ? ?

R2

D OOR [Open ]

L IG H T [ O ff ]

R2

L IG H T [On ]

R2

BU ZZER [Sounds ]

R2

SYSTEM [ C U S T O M E R [ D e te c te d ] ]

Integrated Requirements – with Inconsistency

R 2

R 2

S YS TE M [ Id l e ]

R 2

C U STO MER ? ? A p p ro a c h e s ? ?

R 2 @

D OOR [Open ]

L IG H T [On ]

R 2

BU ZZER [Sounds ]

R 2

S YS TE M [ C U S T O M E R [ D e te c te d ] ]

R 1 C

L IG H T [ O ff ]

Inconsistency Detection Using Running System-State

Detecting Inconsistencies SYSTEM STATE SYSTEM [C U S T O M E R [D e te c te d ] ] := C U S T O M E R [A p p ro a c h e s ] & D O O R [O p e n ] & L IG H T [ O n ] & B U Z Z E R [S o u n d s ] & L IG H T [ O f f ]

Cannot have a SYSTEM STATE where the light is both OFF and ON at the same time

Exercise – Defect Detection