this is an assignement question from software engineering course and its a text book question..need help with the assignement as soon as possible!! please!and the textbook is fundamentals of software engineering second addition by carlo ghezzi and mehdi

Chapter5.pdf

Home >Computer Science homework help >this is an assignement question from software engineering course and its a text book question..need help with the assignement as soon as possible!! please!and the textbook is fundamentals of software engineering second addition by carlo ghezzi and mehdi

Chapter 5: Specification

CSI 5390

Department of Computer Science and Engineering

Oakland University

Dae-Kyoo Kim

Specification

• Types of specifications – Operational (imperative)

• Data Flow Diagrams

• UML Sequence diagrams

• Finite State Machines

• Petri Nets

– Descriptive (declarative) • Entity Relationship Diagrams

• Logic-based notations

• Algebraic notations

Specification

• A statement of agreement (contract)

between producer and consumer

Specification

• Requirements specs

– Between client and developer

– What implementation must achieve

– Reduce misunderstandings

– Verification point of implementation

– The hardest part in software development

• Design specs

– Between designer and implementer

Specification

• Interface specs

– Between designer and implementer

• Input (signals or commands)

• Output (controlled data, response)

• Module specs

– Between programmer and tester

Use of Specification

• Reduce misunderstanding

• A verification point during development

• A reference point during product maintenance – Corrective, adaptive, perfective

Specification Qualities

• Usability

• Maintainability

• Understandability (clarity) – e.g., a word processor

• Can an area be scattered?

• What if the length of a word exceeds the line length?

– e.g., a safety-critical system • Can a message be accepted as soon as we receive 2 out of 3 identical copies or do we

need to wait for the 3rd?

• Consistency

• Completeness – Internal completeness

• Defining new concepts or terminologies

– External completeness • About FRs and NFRs • NFRs are often implicit and commonsense

• Specs may be informal purposely – To give implementation freedom

Ambiguous Specification

Selecting is the process of designating

areas of the document that you want to

work on. Most editing and formatting

actions require two steps: first you

select what you want to work on,

such as text or graphics; then you

initiate the appropriate action.

A word processor

Ambiguous Specification

The whole text should be kept in lines

of equal length. The length is specified

by the user. Unless the user gives an

explicit hyphenation command,

a carriage return should occur only

at the end of a word.

A word processor

Ambiguous Specification

The message must be triplicated. The three

copies must be forwarded through three

different physical channels. The receiver

accepts the message on the basis of a

two-out-of-three voting policy.

A real safety-critical system

Specification Styles

• Informal

– Informal syntax + informal semantics

• Semiformal

– Formal syntax + informal semantics

– e.g., TDN, GDN, UML

• Formal

– Formal syntax + formal semantics

Specification Styles

• Operational

– Describe desired behavior

– e.g., drawing an ellipse

• Select → Put a string and fix → Position a pencil →

Move clockwise

• Descriptive

– Describe desired properties (e.g., mathematical

equations)

– e.g., drawing an ellipse

• X2/a2 +y2/b2 = 1 (a>b>0, k2=a2-b2)

Operational: Drawing an Ellipse:

Descriptive: Drawing an Ellipse

(-k, 0) (k, 0)

(x, y)

Specification Styles

• Sorting an array

– Operational

• Selection sort

– Descriptive

• Given p’’ = sorted (p’)

• size (p’) = size (p’’) 

•  a:p’ • a  p’’

• p’’(n) > p’’(n-1)

Sorting an Array

“Let a be an array of n elements. The result of its sorting

is an array b of n elements such that the first element of

b is the minimum of a (if several elements of a have the

same value, any one of them is acceptable); the second

element of b is the minimum of the array of n-1

elements obtained from a by removing its minimum

element; and so on until all n elements of a have been

removed.”

“The result of sorting array a is an array b which is a

permutation of a and is sorted.”

DES

Verification of Specs

• Two approaches

– Simulation

• Observing dynamic behaviors

• Possible automation

• Helps to build prototypes

– Property analysis

• Checking consistency

• Checking correctness (true/false)

Dataflow Diagram

• Describing data flow in terms of functions

• Start from the “context” diagram

• Refine until “elementary” functions

Graphical notation

The function symbol

The data flow symbol

The data store symbol

The in put device symbol

The output device symbol

Figure 5.2

5.5.1. Dataflow Diagrams

(continued)

+ * +

a d c

Figure 5.3. Specifying evaluation of (a + b) * (c + a * d)

Dataflow Diagram

... ...

Input 1

Input 2

Input n

Output 1

Output 2

Output m

information

system

Dataflow Diagram

B3 B4

I O

P Q

Library Example

Sh elves

List of Autho rs

List of t it les

List of t opics

T itle an d autho r

of request ed book ; name

of t he user

Get a bo ok

Boo k

List of bo oks borro wed

Boo k title;

user name

T op ic request

by t he user

Search by

t opics

Boo k request

by t he user

Boo k

recept io n

T op ic List of t it les

referring t o t he t op ic

Boo k

Aut ho r

T itle

Disp lay of

t he list of t itles

T op ic

T itle

Figure 5.4

Library Example

Shelves

List of Authors

List of titles

Title and author

of reques ted book;

name of the us er

Book

List of books borrowed

Book title;

us er name

Book request

by the user

Book

reception

Book

Author

Title Find

book

position

Get

the book

Figure 5.5

Patient monitoring systems

The purpose is to monitor the patients’ vital factors--blood,

pressure, temperature, …--reading them at specified frequencies

from analog devices and storing readings in a DB. If readings fall

outside the range specified for patient or device fails an alarm

must be sent to a nurse. The system also provides reports.

Patient monitoring systems

Patient

Nurse

Patient

Monitoring Nurse

Persistent data

Report

Alarm

Data

Clinical

Report Request

Recent data

Data for report

First Refinement

Nurse

Patient archive

Report Request

Limits for patient

Monitoring

Central

Limits

Update

archive

Generate Report

Data for Report

Recent Data

Formatted data

Alarm

Patient Clinical DataMonitoring

Local

Patient data

Report

Second Refinement

Limits

Formatted data alarm

data Patient

decode

Check

violations limit

Temperature

Pulse

Pressure

Result

Pressure, pulse…

Format

data clock Date

Time produce

message

Dataflow Diagram

• Easy to read, but informal semantics

– Semantics is described through identifiers

– e.g., for “Find book position” • Both title and author are needed?

• No control aspects

– Solution: add control flow

All outputs of A, B,

C needed? Outputs to E and F at

the same time?

Trigger (allReceived)

Dataflow Diagram

• No synchronization

– Two possible interpretations (semiformal)

1. Synchronous: produce and wait until consumed

2. Asynchronous: use buffer in B

UML Use Case Diagram

• Describing the system context in terms of

use cases and actors

borrow

book

return

book

library

update

librarian

customer

UML Sequence Diagram

• Describing interaction behaviors in terms

of objects and messages

• Describing a scenario

UML Sequence Diagram

Librarian Catalogue

member card +

book request membership

book request

book available

book borrowed

time

Customer

UML Collaboration Diagram

Customer Librarian Catalogue

1: member card +

book request

2: membership OK

3: book request

4: book available 5: book borrowed

Finite State Machine

• Describing the system behaviors in terms of

states

• Recognizing a string x over a language L

• AKA as finite automata (automaton)

Finite State Machine

• A quintuple (Q, ∑, q0, δ, A)

– Q: a finite set of states

– ∑: a finite set of symbols

– q0∈Q: the start state

– δ (delta): Qⅹ∑ →Q • transition function

• total function

– A ⊆Q: a set of accepting states

FSM: Example 0

• Q = {q0}

• ∑ = {a}

• A = {q0}

• δ (q0,a) = q0

Finite State Machine

• Sink state

– Accepting states or trap states which cannot

leave once entered

• Non-sink state

– Trap-free

– Any missing transitions are assumed to lead

to a trap state

• One transition per state-and-symbol pair

FSM: Example 1

A C

b c

a, b, c

trap state

a, b

FSM: Example 1 Revised

A C a

b c

Without a trap state

while accepting the same language

FSM: Example 2

• Draw an FSM with no trap state

L = {x | x ∈ {a, b}* and every a precedes every b}

= {x | x = yz and y ∈ {a}* and z ∈ {b}*}

= {x | x ∈{a, b}* and there is no occurrence of ba in x}

q0 q1 b

a b

trap state

Example 3

• L = {x | x  {a, b}* and there is no odd

block of bs in x}

q0 q1

a b

Example 4

• Draw an FSM for L over ∑={a, b, c, d} that contains strings x such that – (i) x begins with dc

– (ii) x ends in a substring cd. Note: “c” is different from “c” in (i)

– (iii) between these substrings there is no other occurrence of cd.

d A

d c c

a,b,d

It should not accept dcaaacbbbcd, dcccd,…

Example 4: Revision

d A

d c c

a,b,d c

a,b

Modeling Tips

• Use a constraint on sequences as a base

• Assigning a transition for each alphabet in the constraint

– e.g., “all strings must start with xy” • Assign the first two transitions for each of x and y

– e.g., “all strings must end with xy” • Assign the last two transitions for each of x and y

– e.g., “there is only one x in the middle” • Assign a transition in somewhere in the middle of

the FSM for x

Non-Deterministic Finite Automata

• May have more than one transition for a

symbol out of a state

Example

• An NFA for for L = {ab, ac}

b C

(A, a) -> {B, D}

(B, b) -> {C}

(D, c) -> {E}

Definition 4

• Nondeterministic finite automata

– δ: Qⅹ∑ →Q_set

Example

• L = {x | x ∈ {a,b}* and x end with ab}

• e.g., no abba

b a

q0 q1 a

q2 b

a, b

DFA

NFA

M=({q0,q1,q2}, {a,b}, q0, δ, {q2}) {q0, q1} {q0}

{} {q2}

{} {}

δ =

a b

q0 q1 q2

Finite State Machine

a a

Figure 5.12

Finite State Machine

On Off

Push swi tch

Figure 5.13: A lamp

Finite State Machine

On Off

High-pressure alarm

High-temperature alarm

Restart

Figure 5.14: A plant control system

Finite State Machine

Pres s ure s ignal Temperat ure s ignal

Suc c es sf ul

rec ov ery

Uns uc c ess f ul

rec ov ery

O ffNormal

Pressure action

Of fNormal

Pres s ure

ac tion

Temperat ure s ignal Temperat ure

ac tion

Suc c es sf ul

rec ov ery Uns uc c ess f ul

rec ov ery

Pres s ure s ignal

Figure 5.15: A refinement

abnormal

Finite State Machine

q q q q

q q

e g i

1 2 3 4

5 6

Figure 5.16: An FSM accepting “begin” and “end”

Finite State Machine

Identifier Recognizer

• Start with a letter

• May have hyphens, digits, and letters

• End with a digit or a letter

• Can’t end with a hyphen

Finite State Machine

• Limitations

– Limited expressive power due to finite memory

– Exponential state explosion • e.g., 28 states for an eight-bit register

– No concurrent support • One action in a state at a time

Example of State Explosion

• Producer – Produces messages and put into a buffer

• Consumer – Reads messages and remove from the buffer

• Buffer: two-slot

• Compose by cartesian product for synchronization

Example of State Explosion

Producer

p 1

c 2

Storage

produce

write

read

consume

write

read read

write

p 2

Consumer

c 1

2 0

Example of State Explosion

<0, p ,c >

consume

produce

consume

produce

consume

produce

consume

produce

produce produce

consume consume

write

read

write

read

write

read

write

1 2

<0, p , c >

2 2

<1, p ,c >

<0, p ,c >

1 1

<1, p ,c>

<1, p ,c >

2 1

1 2

2 2 <2, p ,c > 2 2

<2, p ,c > 1 2

<2, p ,c > 2 1

<2, p ,c > 1 1

Figure 5.19: The resulting FSM

Petri Nets

• Designing concurrent systems

• Quadruple: (P,T,F,W)

P: places

T: transitions (P, T are finite)

F: flow relation (F  (PT)  (TP))

W: weight function (W: F → N – {0} )

Petri Nets

• Token

– A condition to be satisfied

– If satisfied, an action or event can occur and

the resource becomes available (transition

can fire)

Petri Nets

• Properties

– P  T = Ø

– P  T  Ø

– F  (P  T)  (T  P)

– W: F → N - {0} (default: 1)

Petri Nets

• Marking (defining states) – M: P → N

– N: the number of tokens

– A transition f from a place p is enabled if M(p) ≥ W(f)

– State x = (M(p1), M(p2), ..., M(pn))

• Marked petri net – (P,T,F,W,x0)

– x0 : the initial marking • e.g., [(p1,1), (p2,2), (p3,0), (p4,3)]

Petri Nets

places

transitions flows

marking

3 weight P

Petri Nets

• Steps

1. Fire

2. Remove tokens (equal to the weight)

3. Insert tokens (same # of tokens)

Petri Nets

• Non-deterministic

– Any enabled transition may fire

– Model does not specify which one and when

fires

• Concurrent

– Two enabled transitions can fire at the same

time if tokens are sufficient

t P

(a) (b)

Non-Determinism

Petri Nets

• Conflict – Firing one prevents another

• Example – t3 and t4 are mutually exclusive

• Solution – Use more resources

P P

t t

5 6

2 2

Conflict Free (possible deadlock)

Petri Nets

• Starvation – The same transition cannot fire repeatedly

– Due to non-determinism

• Example – t3 and t4 are mutually exclusive

– t4 in hold until t5 fires

– If t1 fires and t3 again, the other flow starves

• Solution – Use alternation

P P

t t

P P

t t

1 2

Starvation Free

Partial starvation

Petri Nets

• Deadlock

– No transition is enabled

– No deadlock is said to be “live”

• Solution

– Re-design flow

P P

t t

5 6

2 2

Deadlock Free

Buffer Example Revisited

P P

write

produce

consume

0 1 2

re ad re ad

write write

re ad

Buffer Example Revisited

C1 C2

consu me

0 1 2

rea d

write write

rea d

P1 P2 pro duce

Buffer Example Revisited

• Complexity reduced significantly

• Concurrency – Concurrently firing when <1, P1, C2>

– Both the consume transition in the consumer and the write transition between 1 and 2 are enabled

Limitations of Perti Nets

• Tokens are anonymous

– Only shows the presence of a message

– Requiring non-determinism

• Solution

– Use parity bits in tokens

channel 1 channel 2

Limitations of Perti Nets

(normal) (error)

even # of 1s odd # of 1s

Tokens with parity bits

Limitations of Perti Nets

• No time consideration

– Can’t model real-time systems

– e.g., Figure 5.21 (a)

• If t1, t3, t5 take 1 second and t2 takes 5 seconds to

fire

• Then <t1, t2, t3, t5, t4> is infeasible

• Because t2 can’t fire at time 2

• Then, it should be <t1, t3, t5, t1, t3, t5, t2>

Extensions of Perti Nets

• Assign values to tokens

– Associate transitions with predicates and

functions

P P

3 4

7 1 4

t t1 2

4 5

1 2

If (P3 = P2)

P4 := P3 − P2

P5 := P2 + P3

If (P2 > P1)

P4 := P2 + P1

Tokens with Values

Extensions of Perti Nets

• Use priority for transitions

– Pri: T → N

– Only those with highest priority are allowed to

fire

Extensions of Perti Nets

• Using time for transition

– <tmin, tmax>

• Tmin: minimum waiting time before firing

• Tmax: maximum waiting time to fire

– In original PN, tmin=0, tmax=∞

– Can be used with priority

• e.g., only those with highest priority can fire

P P

t t t

t m in = 1 t m a x = 4

t m in = 2 t m a x = 3

t m in = 0 t m a x = 5

p r ior it y = p r ior it y = p r ior it y = 1 3 2

1 2

Timed and Prioritized Petri Net

Extensions of Perti Nets

• Case1

– t1 can’t fire if not fire within time 2 because t2 has a higher priority

• Case2

– t1 can’t fire if P4 has a token at time 1

because t3 has a higher priority

Extensions of Perti Nets

• Revisiting the ambiguous requirements

– “The message must be triplicated …”

• Interpretation 1

– Considered to be received as soon as two

received

• Interpretation 2

– Wait until all three are received

Original mes s age

Mes s age t riplic ation

Mes s age c opies

Mes s age c opies t rans mis s ion

t min =

t max =

t min =

t max =

t min =

t max = 0

f or all three t rans it ions

PC1

PC2

PC3

c 1

k 1

c 2 k 2

F orwarded m es s age

t v ot ing1 t v ot ing2 t v ot ing3

{

Original mes s age

Mes s age t riplic ation

Mes s age c opies

Mes s age c opies t rans m is s ion

t min =

t max =

t min =

t max =

t min = 0

t max = 0

PC1

PC2

PC3

c 1

k 1

c 2 k 2

t v ot ing

F orwarded m es s age

Case Study: Elevator System

An n-elevator system is to be installed in a building with m floors. The manufacturer supplies the elevators and the control mechanisms. The internal mechanisms of each are assumed given. The problem concerns the logic to move elevators between floor according to the following constrains:

1. Each elevator has a set of buttons, one for each floor. The buttons light up when pressed and cause the elevator to visit the corresponding floor. The lights switch off when the elevator visits the floor.

2. Each floor other than the ground floor and the top floor has two buttons, one to request an up elevator and one to request a down elevator. These buttons light up when pressed. The light switch off when the elevator visits the floor and either is moving in the desired direction or has no outstanding requests. In the latter case, if both floor-request buttons are pressed, only one is canceled. The algorithm to decide which to service first should minimize the waiting time for both requests.

3. When an elevator has no requests to service, it should remain at its final destination with its doors closed and await further requests.

4. All requests for elevators from floors must be serviced eventually, with all floors given equal priority.

5. All requests for floors within elevators must be serviced eventually, with floors being serviced sequentially in the direction of the elevator’s travel.

6. Each elevator has an emergency button that, when pressed, causes a warning signal to be sent to the site manager. The elevator is then deemed “out of service.” Each elevator has a mechanism to cancel it’s “out of service” status.

Case Study: Elevator System

• Ambiguities – “Each floor other than the ground floor and the

top floor has two buttons, …” • The ground and top floor are assumed to have one

button?

– “The light switches off when the elevator visits the requested floor and is either moving in the desired direction or has no outstanding requests”

• Interpretation 1 – As soon as reaching the floor

• Interpretation 2 – After reaching the floor and starts moving

Case Study: Elevator System

• “The algorithm to decide which floor to service first should minimize the waiting time for both requests” – Infeasible (no way to minimize both)

– The sum of both should be minimized

– The anticipated minimized time can’t be guaranteed

Case Study: Elevator System

5 time 4 time

May be a request at 2 while

Moving up

Initial Design

Case Study: Elevator System

• Apply modularity

– Position module

– Button module

– Scheduler module

• Apply generality

– Parameterized concepts

• Generic floor j

• Generic floor button j

Case Study: Elevator System

Modularization

Elevator

Position Scheduler Button

Internal External

Case Study: Elevator System

• Incomplete – No external buttons

– No resetting

– No interruption during moving

Button Module

C P Push

Set

Off

Reset

0.1. .

0.05. .0.05

0. .0

(for both internal and external buttons)

Button Module

• Using timed PN

• tmin(set) = tmax(set) = 0 for “c”

– immediate firing

• tmin(push) = 0.1

– Idle to allow for “c” to consume a token

• tmax(c) = 0.005

– Any time less than 0.1 to consume a token

within the idle time

Position Module F

F DFUF

UF F DF

m-1

m-1 m-1

3 3

2 2

(1st version)

Position Module

• Associate time with transitions for speed

(2nd version)

Position Module Fj+1 UFj+1

Fj"

t Fj'

UPh

DOWNh

ILBh

DOWNj+1

ILBj+1

t1 t2 t3 t4 t5 t6

t10

t11 t12

UPj+1

higher priority

Position Module

• ILBj+1, UPj+1, DOWNj+1 might occur

during transition

Internal Button Module

ILBj

Set

Reset

OffOn 0..0

External Button Module

Set

x..x Reset

ti'

Fj'

On Off

UPj

x..x

Internal button

for Fh is on

Time to enter into the elevator

priority=2

priority=1

Scheduler Module

• Keep the direction unchanged if there is a

request on that direction. Otherwise,

change the direction

– Satisfies “All requests must be served

eventually”

– No consideration of minimizing waiting times

Scheduler Module

priority=2

priority=1

priority=2

priority=1

priority=2

priority=3

Integrating Scheduler

Fj+1 UFj+1

Fj"

Fj'

UPh

DOWNh

ILBh

DOWNj+1

ILBj+1

t1 t2 t3 t4 t5 t6

t10

t11 t12

UPj+1

Integrating Scheduler + External Button

priority=2

priority=1

priority=2

priority=3

x..x

Module Integration

Fj+1 UFj+1

Fj"

Fj'

UPh

DOWNh

ILBh

DOWNj+1

ILBj+1

t1 t2 t3 t4 t5 t6

t10

t11 t12

UPj+1

same

priority=2

priority=1

priority=2

priority=3

x..x

Module Integration

Fj+1 UFj+1

Fj"

Fj'

UPh

DOWNh

ILBh

DOWNj+1

ILBj+1

t1 t2 t3 t4 t5 t6

t10

t11 t12

UPj+1

same

Integrating Scheduler + External Button + Internal Button

SCHEDULER

... al l transitions

General Scheduler

• The token has all information about the

state of the system to determine what to

fire

• The token is kept being reproduced

• Attach predicates to all the transitions

based on the scheduling policy

Scenario

“Suppose that i) the elevator is at floor 1, ii)

a passenger pressed the external up

button on floor 1, iii) walked into the

elevator, and iv) pressed the internal

button 2. After ∆t seconds later, the

elevator will reach floor 2 and the internal

button will be reset”

Simulation

• set (ExtB)-> set (InteB) -> t1 -> t -> t7

Descriptive Specifications

• Describing properties rather than

behaviors

• Based on mathematical logic

Entity-Relationship Diagrams

• Describing data relationships

• ERD focusing on data while DFD focusing operations

• DFD + ER diagram = class diagram

• Not standardized

• Semiformal

• Can’t specify predicates – e.g., “A class exists only if # of students > 5 and ≤

MAX_ENROLL”

STUDENT

CLASS

ENROLLED_IN

NAME

SEX

AGE

SUBJECT

COURSE_ID

MAX_ ENROLLMENT

(may have properties, e.g., proficiency)

A R B

A R B many to many

one to one

one to many

many to one

Logic Specifications

• Boolean expressions described in logical

connectives

• May have quantifiers

• Types

– Boolean ground terms

– Propositions

– Predicates

Logic Specifications

• Logical connectives

– : or

– : and

– : not

– : implication

– : logical equivalence (a.k.a. )

– : universal quantifier

– : existential quantifier

Logic Specifications

• General expression

– Free-variable expression

• E

– Bound-variable expression

• Qx:T•E

Logic Specifications

• Examples

– x > y  y > z  x > z

– x = y  y = x

–  x, y, z • x > y  y > z  x > z

– x + 1 < x – 1

–  x •  y • y = x + z

– x > 3  x < -6

tautology

free variables

bound variables

closed contradiction

Logic Specifications

• Closure

– Quantifying all free variables with the “for all”

quantifier

– If the free-variable formula is false, its closure

is also false

• e.g., x+1 < x-1: it’s false, its closure is also false

• x • x+1<x-1

– The same is true for true

Logic Specifications

• Operation semantics

• Data invariants

Operation Specifications

• Operation specification

– pre: i1, i2,..., in

– P (i1, i2,..., in) = (o1, o2,..., om)

– Post: o1, o2,..., om, i1, i2,..., in

• If “pre” holds before P, “post” must hold

after P

Example

• Division – pre: i1>i2 – divide (i1, i2) = (q,r)

– post: i1=i2*q + r and r ≥ 0 and i2>r

Example

• Greatest Common Divisor

– pre: i1 > 0 and i2 > 0

– GCD (i1, i2) = o

– post: z1, z2 • i1 = o * z1 and i2 = o * z2 and

(h • i1 = h * z1 and i2 = h * z2 and h > o)

Example

• Reversing sequence

– pre: len(i1, i2, ...,in) > 0

– Rev(i1, i2, ...,in) = (o1, o2, ..., on)

– post: k:1 k  n • ok=in-k+1

Example

• Searching

– pre: size(t) > 0

– search (t: int_array, e: int) = f: Bool

– post: f = true ≡ i:1  i  size(t) • t(i) = e

Example

• Sorting

– pre: size(a) > 0, let size(a) = n

– sort (a: int_array): a’:int_array

– post: i:1 ≤ i < n• a’(i) ≤ a’(i+1) and

i:1 ≤ i ≤ n• j: 1 ≤ j ≤ n • a’(j) = a(i) and

|a| = |a’|

Example

• Deleting

– pre: i: 1 ≤ i ≤ size(a) • a[i]=x

– del(a:array, x:element): a’:array

– post: i: 1 ≤ i ≤ size(a’) • a’[i] ≠ x and |a’| = |a|

- 1

Example

• Invariant for an array a as a set

– i, j • 1 ≤ i, j ≤ size(a) • i≠j  a[i] ≠ a[[j]

Case Study: Elevator System

• Define in terms

– States and events as predicate functions

– Rules defined over states and events

• Assumptions

– Zero decision times

– No simultaneous events

Case Study: Elevator System

• State – A condition holding for a certain time period

– e.g., standing (E, F, T1, T2) • assumption: closed at left, open at right

• Event – A condition holding at a particular time

– e.g., arrived (E, F, T)

• Rules – Relating states and events

– LHS implies RHS

Events

• arrival (E, F, T)

– E:1..n, F:1..m, T  t0 (initial time)

• departure (E, F, D, T)

– D: {up, down}

• stop (E, F, T)

• new_list (E, L, T)

– L: [1.. m]*, list of floors to visit

Events

• call (F, D, T)

– External call

• request (E, F, T)

– Internal request

States

• standing (E, F, T1, T2)

– T1: Inclusive, T2: Exclusive

– T0  T1  T2

• moving (E, F, D, T1, T2)

– F: last visited floor

• list (E, L, T1, T2)

– L is valid for the interval [T1, T2]

Rules

R1:When E arrives at floor F, it continues to move if there is no request for service from F and the list is empty. If the floor to serve is higher, it moves upward; otherwise it moves downward.

arrival (E, F, Ta) and list (E, L, T, Ta) and first (L) > F

implies departure (E, F, up, Ta)

A similar rule describes downward movement.

Passing F

R2: Upon arrival at F, E stops if F must be serviced (F appears as first of the list)

arrival (E, F, Ta) and list (E, L, T, Ta) and first (L) = F

implies stop (E, F,Ta)

Serving F

Rules

R3: E stops at F if it gets there with an empty list

arrival (E, F, Ta) and list (E, empty, T, Ta)

implies stop (E, F, Ta)

Stop at F

Rules

R4: Assume that elevators have a fixed time to service a floor. If the list is not empty at the end of such interval, the elevator leaves the floor immediately.

stop (E, F, Ta) and list (E, L, T, Ta + Ts) and first (L) > F,

implies departure (E, F, up, Ta + Ts )

Move up after stop

Rules

standing time

Rules

R5: If the elevator has no floors to service, it stops until its list becomes nonempty.

stop (E, F, Ta) and list (E, L, Tp, T) and Tp > Ta + Ts and list (E, empty, Ta + Ts, Tp) and first (L) > F

implies departure (E, F, up, Tp)

Wait for request

R6: Assume that the time to move from on floor to the next is known and fixed. The rule describes movement.

departure (E, F, up, T) implies

arrival (E, F + 1, T + Tt)

Rules

transition time

Arrive at F

Rules

R7: The event of stopping initiates standing for at least Dts.

stop (E, F, T) 

standing (E, F, T, T + Ts)

R8: At the end of the minimum stop interval Dts, E remains standing if there are no floors to service.

stop (E, F, Tst) and list (E, empty, Tst + Ts, T)

implies standing (E, F, Tst, T)

Rules

R9: Departure causes moving.

departure (E, F, D, T) implies

moving (E, F, D, T, T + Tt)

R10: Reserving F from inside E, which is not standing at F, causes immediate update of L according to previous policy

request (E, F, Tr) and not (standing (E, F, T, Tr)) and list (E, L, T, Tr) and LF = insert_in_order(L, F, E)

implies new_list (E, LF, Tr)

Rules

request time

R11: Effect of arrival of E at floor F

arrival (E, F, Ta) and list (E, L, T, Ta) and F = first (L) and Lt = tail (L)

implies new_list (E, Lt, Ta)

Rules

R12: How list changes

new_list (E, L, T1) and not (new_list (E, L, T2) and T1 < T2 < T3)

implies list (E, L, T1, T3)

If L is the new list at T1 and it is not new at T2 until T3,

then L is the list from T1 to T3.

Rules

R13: All requests will eventually be served

new_list (E, L, T) and FL implies

new_list (E, L1, T1) and FL1and T1  T

Verification

• “Elevator 2 standing at floor 3 at time 5 till

time 7 with no outstanding request will

arrive at floor 8 at time 7+5Tt when an

internal request is made for floor 8 at time

7.”

Verification

• Given states and events

a. standing (2, 3, 5, 7) • “elevator 2 at floor 3 at least from instant 5 to 7”

b. list(2, empty, 5, 7) • “with no outstanding request”

c. request(2, 8, 7) • “when an internal request is made for floor 8 at

time 7”

d. {8} = insert_in_order(empty, 3, 2) • Derived from a, b, and c

Verification

• Applying rules e. new_list(2, {8}, 7) by R10

f. list(2, {8}, 7, 7+Ts) by R12

g. stop(2, 3, 5) by R7

h. First ({8}) > 3 derived from f

i. departure (2, 3, up, 7) by R5 (departure)

j. arrival (2, 4, 7+Tt) by R6 (arrival)

k. departure (2, 4, up, 7+Tt) by R1 (passing)

l. arrival (2, 5, 7+Tt+Tt) by R6 (arrival)

…

* departure (2, 7, up, 7+4Tt) by R1 (passing)

* arrival (2, 8, 7+5Tt) by R6 (arrival)