Specification
Ch. 5
1
Outline
• Discussion of the term "specification"
• Types of specifications
– operational
•
•
•
•
Data Flow Diagrams
(Some) UML diagrams
Finite State Machines
Petri Nets
– descriptive
• Entity Relationship Diagrams
• Logic-based notations
• Algebraic notations
• Languages for modular specifications
– Statecharts
–Z
Ch. 5
2
Specification
• A broad term that means definition
• Used at different stages of software
development for different purposes
• Generally, a statement of agreement
(contract) between
– producer and consumer of a service
– implementer and user
• All desirable qualities must be specified
Ch. 5
3
Uses of specification
• Statement of user requirements
– major failures occur because of
misunderstandings between the producer
and the user
– "The hardest single part of building a
softwarem system is deciding precisely
what to build" (F. Brooks)
Ch. 5
4
Uses of specification (cont.)
• Statement of the interface between the
machine and the controlled
environment
– serious undesirable effects can result due
to misunderstandings between software
engineers and domain experts about the
phenomena affecting the control function
to be implemented by software
Ch. 5
5
Uses of specification (cont.)
• Statement of requirements for
implementation
– design process is a chain of specification (i.e.,
definition)–implementation–verification steps
• requirements specification refers to definition of external
behavior
– design specification must be verified against it
• design specification refers to definition of the software
architecture
– code must be verified against it
Ch. 5
6
Uses of specification (cont.)
• A reference point during maintenance
– corrective maintenance only changes
implementation
– adaptive and perfective maintenance occur
because of requirements changes
• requirements specification must change
accordingly
Ch. 5
7
Specification qualities
• Precise, clear, unambiguous
• Consistent
• Complete
– internal completeness
– external completeness
• Incremental
Ch. 5
8
Clear, unambiguous,
understandable
• Example: specification fragment for a
word-processor
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.
can an area be scattered?
Ch. 5
9
Precise, unambiguous, clear
• Another example (from a real safetycritical system)
The message must be triplicated.
copies must be forwarded through
different physical channels. The
accepts the message on the basis
two-out-of-three voting policy.
The three
three
receiver
of a
can a message be accepted as soon as we receive 2 out of 3
identical copies of message or do we need to wait for
receipt of the 3rd?
Ch. 5
10
Consistent
• Example: specification fragment for a
word-processor
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.
What if the length of a word exceeds the length of the line?
Ch. 5
11
Complete
• Internal completeness
– the specification must define any new
concept or terminology that it uses
• glossary helpful for this purpose
– the specification must document all the
needed requirements
• difficulty: when should one stop?
Ch. 5
12
Incremental
• Referring to the specification process
– start from a sketchy document and
progressively add details
• Referring to the specification document
– document is structured and can be
understood in increments
Ch. 5
13
Classification of
specification styles
• Informal, semi-formal, formal
• Operational
– Behavior specification in terms of some
abstract machine
• Descriptive
– Behavior described in terms of properties
Ch. 5
14
Example 1
• Specification of a geometric figure E:
E can be drawn as follows:
1. Select two points P1 and P2 on a plane
2. Get a string of a certain length and fix its ends
to P1 and P2
3. Position a pencil as shown in next figure
4. Move the pen clockwise, keeping the string
tightly stretched, until you reach the point where
you started drawing
this is an operational specification
Ch. 5
15
Ch. 5
16
A descriptive specification
• Geometric figure E is describe by the
following equation
ax2 + by2 + c = 0
where a, b, and c are suitable constants
Ch. 5
17
Another example
OP
“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
DES permutation of a and is sorted.”
Ch. 5
18
How to verify a
specification?
• “Observe” dynamic behavior of specified
system (simulation, prototyping, “testing”
specs)
• Analyze properties of the specified system
• Analogy with traditional engineering
– physical model of a bridge
– mathematical model of a bridge
Ch. 5
19
Data Flow Diagrams (DFDs)
• A semi-formal operational specification
• System viewed as collection of data
manipulated by “functions”
• Data can be persistent
– they are stored in data repositories
• Data can flow
– they are represented by data flows
• DFDs have a graphical notation
Ch. 5
20
Graphical notation
– bubbles represent functions
– arcs represent data flows
– open boxes represent persistent store
– closed boxes represent I/O
interaction
The function sym bol
The input device sym bol
The data flow symbol
The output device sym bol
The data store symbol
Ch. 5
21
Example
b
+
a d
c
*
specifies evaluation of
(a + b) * (c + a * d)
+
*
Ch. 5
22
A construction “method” (1)
1. Start from the “context” diagram
Input
Input
O utput
1
inform ation
2
Input n
...
system
O utput
...
O utput
Ch. 5
1
2
m
23
A construction “method” (2)
2. Proceed by refinements until you reach
“elementary” functions (preserve
balancing)
A
I
H
I
O
A3
J
A4
A1
A6
P
K
Q
M
A2
S
A5
N
A7
R
K
B2
K2
O
M
B1
K3
K1
T
Ag
B4
B3
N
K4
Ch. 5
24
A library example
Boo k
Boo k requ est
by th e u ser
Sh elv es
Title and au th or
of req uested b ook; name
of th e u ser
Auth or
Boo k
List o f A uthors
Get a bo ok
Boo k
reception
Title
Boo k title;
user n ame
List o f titles
List o f b oo ks bo rrowed
Title
Search by
topics
List o f top ics
Top ic
Top ic
List o f titles
referring to the to pic
Disp lay of
the list of titles
Top ic requ est
by th e u ser
Ch. 5
25
Refinement of
“Get a book”
Book
Shelves
Author
Get
the book
Book
List of Authors
<shelf#, book#>
Title
Find
book
position
Book
reception
List of books borrowed
List of titles
Title and author
of requested book;
name of the user
Book title;
user name
Book request
by the user
Ch. 5
26
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.
N urse
R eport
R equest
P atient
C linical
D ata
R eport
P atient
M onitoring
N urse
A larm
R ecent data
D ata for report
Ch. 5
P ersistent data
27
A refinement
P atient archive
R ecent
D ata
R eport
R equest
D ata for
R eport
N urse
G enerate
R eport
U pdate
archive
R eport
F orm atted data
C entral
M onitoring
L im its
L im its for patient
N urse
A larm
P atient data
L ocal
M onitoring
Ch. 5
C linical
D ata
P atient
28
More refinement
P atient
P ressure
L im its
P ressure, pulse…
T em perature
C heck
lim it
violations
data
decode
P ulse
R esult
F orm at
data
D ate
T im e
clock
produce
m essage
F orm atted data
alarm
Ch. 5
29
An evaluation of DFDs (1)
• Easy to read, but …
• Informal semantics
– How to define leaf functions?
– Inherent ambiguities
A
E
B
• Outputs from A, B, C are
all needed?
• Outputs for E and F are
produced at the same time?
D
F
C
Ch. 5
30
An evaluation of DFDs (2)
• Control information is absent
A
B
Possible interpretations:
(a) A produces datum, waits until B consumes it
(b) B can read the datum many times without
consuming it
(c) a pipe is inserted between A and B
Ch. 5
31
Formalization/extensions
• There have been attempts to formalize
DFDs
• There have been attempts to extend
DFDs (e.g., for real-time systems)
d1
T rigger
d2

.
.
.
dn
Ch. 5
32
UML use-case diagrams
• Define functions on basis of actors and
actions
borrow
book
return
book
librarian
customer
library
update
Ch. 5
33
UML sequence diagrams
• Describe how objects interact by
exchanging messages
• Provide a dynamic view
C usto m er
L ib rarian
C atalo gue
m em b er card +
b o o k req uest
m em b ership
OK
b o o k req uest
tim e
b o o k availab le
b o o k b o rro w ed
Ch. 5
34
UML collaboration diagrams
• Give object interactions and their order
• Equivalent to sequence diagrams
2 : m em b ership O K
1 : m em b er card +
b o o k req uest
C ustom er
3 : b o o k req uest
Librarian
5 : b o o k b o rro w ed
C atalogue
4 : b o o k availab le
Ch. 5
35
Finite state machines
(FSMs)
• Can specify control flow aspects
• Defined as
a finite set of states, Q;
a finite set of inputs, I;
a transition function d : Q x I  Q
(d can be a partial function)
a
q1
a
b
q0
q2
c
b
q3
Ch. 5
36
Example: a lamp
Push switch
Off
On
Push switch
Ch. 5
37
Another example:
a plant control system
H ig h -p re s s u re a la rm
H ig h -te m p e ra tu re a la rm
On
O ff
R e s ta rt
Ch. 5
38
A refinement
Pressure signal
Pressure
Pressure
action
action
Successful
recovery
Temperature signal
Unsuccessful
recovery
Normal
Off
Normal
Off
Successful
recovery
Temperature signal
Unsuccessful
recovery
Temperature
action
Ch. 5
Pressure signal
39
Classes of FSMs
• Deterministic/nondeterministic
• FSMs as recognizers
– introduce final states
• FSMs as transducers
– introduce set of outputs
•...
Ch. 5
40
FSMs as recognizers
q1
e
g
q2
q3
i
q
4
n
b
q0
qf
e
q5
q6
n
d
qf is a final state
Ch. 5
41
FSMs as recognizers
< le tte r>
< d ig it>
q
< le tte r>
0
q1
_
< le tte r>
Legend:
< le tte r>
< d ig it>
q2
< d ig it>
is a n a b b re via tio n fo r a s e t o f a rro w s
la b e le d a , b ,..., z, A ,..., Z ,
re s p e c tive ly
is a n a b b re via tio n fo r a s e t o f a rro w s
la b e le d 0 , 1 ,..., 9 , re s p e c tive ly
Ch. 5
42
Limitations
• Finite memory
• State explosion
– Given a number of FSMs with k1, k2, … kn
states, their composition is a FSM with k1 *
k2 *… * kn. This growth is exponential with
the number of FSMs, not linear (we would
like it to be k1 + k2 +… + kn )
Ch. 5
43
State explosion: an example
p ro d u ce
P ro d u ce r
p1
p2
d e p o sit
get
C o n su m e r
c1
c2
co n su m e
d e p o sit
d e p o sit
S to ra g e
0
1
gCh.
et
5
2
get
44
The resulting FSM
w rite
w rite
< 1 , p ,c >
1 1
< 0 , p ,c >
1 1
consum e
consum e
p ro d u c e
consum e
p ro d u c e
< 0 , p ,c >
2 1
< 2 , p ,c >
1 1
p ro d u c e
< 1 , p ,c >
2 1
< 2 , p ,c >
2 1
re a d
< 0 , p ,c >
1 2
< 1 , p ,c >
1 2
< 2 , p ,c >
1 2
re a d
p ro d u c e
consum e
<0, p , c >
2 2
re a d
w rite
p ro d u c e
consum e
re a d
w rite
< 1 , p ,c >
2 2
Ch. 5
p ro d u c e
consum e
< 2 , p ,c >
2 2
45
Petri nets
A 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} )
Properties:
(1) P  T = Ø
(2) P  T  Ø
(3)F  (P  T)  (T  P)
(4) W: F  N-{0}
Default value of W is 1
State defined by marking: M: P  N
Ch. 5
46
Graphical representation
p la ce s
m a rk in g
tra n sitio n s
P
flo w s
3
w e ig h t
P
2
1
t
1
t
P
3
P
2
P
5
4
t
t
4
3
P
P
7
6
t
5
t
Ch. 5
6
47
Semantics: dynamic evolution
• Transition t is enabled iff
– p  t's input places, M(p)  W(<p,t>)
• t fires: produces a new marking M’ in places
that are either t's input or output places or
both
– if p is an input place: M'(p) = M(p) - W(<p,t>)
– if p is an output place: M'(p) = M(p) + W(<t,p>)
– if p is both an input and an output place:
M'(p) = M(p) - W(<p,t>) + W(<t,p>)
Ch. 5
48
Nondeterminism
• Any of the enabled transitions may fire
• Model does not specify which fires, nor
when it fires
Ch. 5
49
Modeling with Petri nets
• Places represent distributed states
• Transitions represent actions or events
that may occur when system is in a
certain state
• They can occur as certain conditions
hold on the states
Ch. 5
50
after (a) either (b) or (c) may occur, and then (d)
P2
P1
P
P1
2
t1
t1
3
P
P
t4
t3
P
t5
t4
t3
P
P7
6
P7
6
P5
4
P5
4
t5
t6
t6
(b)
(a)
P
P1
t
2
t
P
4
P2
P1
1
P3
P
t2
P
t2
P3
t2
1
P
P
P5
4
5
t4
t3
P
P
6
t4
t3
P
6
7
t5
7
t5
t6
t6
Ch. 5
(c)
t2
P3
51
(d)
Common cases
• Concurrency
– two transitions are enabled to fire in a given state,
and the firing of one does nor prevent the other
from firing
• see t1 and t2 in case (a)
• Conflict
– two transitions are enabled to fire in a given state,
but the firing of one prevents the other from firing
• see t3 and t4 in case (d)
• place P3 models a shared resource between two
processes
– no policy exists to resolve conflicts (known as
unfair scheduling)
– a process may never get a resource (starvation)
Ch. 5
52
How to avoid starvation
P1
P2
P3
t1
P
4
t3
t2
imposes alternation
P
5
t4
P
P
6
7
t
t6
5
Ch. 5
53
A conflict-free net
P
P
1
t1
t
2
2
R
t'3
t'
4
t"
3
this net can
deadlock!
consider
'
'
 t1 , t 3 , t 2, t 4 
t"
4
2
2
t
t
6
5
Ch. 5
54
A deadlock-free net
P
P
1
t1
t
2
2
R
t'3
2
t'
2
4
t"
3
t"
4
t
t
5
2
6
2
Ch. 5
55
A case of partial starvation
t1
t
t3
t
Ch. 5
2
4
56
Producer-consumer example (1)
write
consume
P
1
P
2
C
2
C1
produce
read
separate nets
for the subsystems
read
0
read
1
write
Ch. 5
2
write
57
Producer-consumer example (2)
consume
C1
C2
read
read
one net for the
entire system
0
1
2
write
write
P1
produce
Ch. 5
P2
58
Limitations and extensions
P
channel1
channel2
Token represents a message.
You wish to say that the delivery channel depends
on contents.
How?
Petri nets cannot specifyCh.selection
policies.
5
59
Extension 1
assigning values to tokens
• Transitions have associated predicates
and functions
• Predicate refers to values of tokens in
input places selected for firing
• Functions define values of tokens
produced in output places
Ch. 5
60
Example
P
2
P
1
P
7
3
1
4
4
t1
t2
P
4
P
5
3
Predicate P2 > P1
and function
P4 := P2 + P1
associated with t1
Predicate P3 = P2
and functions
P4 := P3  P2 and
P5 := P2 + P3 are
associated with t2
The firing of t1 by using <3,7> would produce the
value 10 in P4. t2 can then fire using <4, 4>
Ch. 5
61
Extension 2
specifying priorities
• A priority function pri from transitions to
natural numbers:
• pri: T  N
• When several transitions are enabled,
only the ones with maximum priority
are allowed to fire
• Among them, the one to fire is chosen
nondeterministically
Ch. 5
62
Extension 3
Timed Petri nets
• A pair of constants <tmin, tmax> is
associated with each transition
• Once a transition is enabled, it must
wait for at least tmin to elapse before it
can fire
• If enabled, it must fire before tmax has
elapsed, unless it is disabled by the
firing of another transition before tmax
Ch. 5
63
Example
combining priorities and time
P
1
P
t1
t m in = 1
tm a x = 4
p r io r it y = 1
P
2
P
3
t
t
2
t m in = 2
tm a x = 3
p r io r it y = 3
Ch. 5
4
3
t m in = 0
tm a x = 5
p r io r it y = 2
64
Ori ginal m essage
{
tmi n = c1
tmax = k1
M essage trip li cati on
M essage copi es
tmi n =
{ tmax =
c2
k2
M essage copi es transm ission
PC2
PC3
PC1
{
tmi n = 0
tmax = 0
tvoti ng1
tvoti ng2
tvoti ng3
for all three transi ti ons
Precise specification
of message triplication
problem
Case (1)
Forwarded message
Ch. 5
65
Ori ginal m essage
tmi n = c1
tmax = k1
M essage trip li cati on
M essage copi es
tmi n = c2
tmax = k2
M essage copi es transm ission
PC2
PC3
PC1
tmi n = 0
tmax = 0
Precise specification
of message triplication
problem
Case (2)
tvoti ng
Forwarded message
Ch. 5
66
Case study
• An n elevator system to be installed in a building with
m floors
• Natural language specs contain several ambiguities
• Formal specification using PNs removes ambiguities
• Specification will be provided in a stepwise fashion
• Will use modules, each encapsulating fragments of
PNs which describe certain system components
Ch. 5
67
From informal specs…
“The illumination is cancelled when the elevator
visits the floor and is either moving in the desired
direction, or ...”
2 different interpretations (case of up call)
– switch off as the elevator arrives at the floor from below
(obvious restrictions for 1st and last floor)
– switch off after the elevators starts moving up
• in practice you may observe the two cases!
Ch. 5
68
…more analysis of informal
specs
“The algorithm to decide which to service
first should minimize the waiting time
for both requests.”
what does this mean?
• in no other way can you satisfy either request
in a shorter time
– but minimizing for one may require longer for the
other
• the sum of both is minimal
– why the sum?
Ch. 5
69
Initial sketch of movement
Ch. 5
70
Button module
C
P
P ush
0 .0 5 . .0 .0 5
0 .1 . .
On
Set
0 . .0
O ff
R eset
Ch. 5
71
Elevator position (sketch)
Fm
UF
F
DF
m-1
m-1
UF
F
3
DF
3
3
UF 2
m-1
F2
DF
2
F1
Ch. 5
72
More precise description of elevator position
F j+ 1
U F j+ 1
t8
t1 0
t7
UPh
t9
t1 1
t1 2
On
F j"
t
On
DOW Nh
F j'
On
IL B j+ 1
On
t1
t2
t3
t4
t5
t6
IL B h
On
U P j+ 1
Fj
D O W N j+ 1
On
Ch. 5
Assume j+1hm
73
Switch internal button off
Set
IL B j
0..0
On
O ff
R e se t
Fj
Ch. 5
74
Switch external button off
Fj'
UPj
Set
ti'
Fj
On
Off
x..x Reset
x time needed by
a person to enter + pushing button
Ch. 5
75
Specifying policy
A “fair” solution:
Keep the direction unchanged as long as there are
calls that require elevator to go in that direction
[x,x]
U_D
[0,0]
DK
UK
[0,0]
D
U
D_U
[x,x]
t7, t8, t9 have higher priority than t10, t11, t12
Ch. 5
76
A general scheduler
SCHEDULER
...
all transitions
• Each transition has predicate OK(Scheduler)
• Token in SCHEDULER stores information about the
state of the system that is useful for scheduling
transitions to fire
• The token is “permanent” (it is always reproduced after
the firing of any transition)
Ch. 5
77
Declarative specifications
ER diagrams: semiformal specs
Logic specifications
Algebraic specifications
Ch. 5
78
ER diagrams
• Often used as a complement to DFD to
describe conceptual data models
• Based on entities, relationships,
attributes
• They are the ancestors of class
diagrams in UML
Ch. 5
79
Example
NAME
AGE
STUDENT
SEX
ENROLLED_IN
SUBJECT
CLASS
COURSE_ID
MAX_ENROLLMENT
Ch. 5
80
Relations
• Relations can be partial
• They can be annotated to define
– one to one
A
R
B
– one to many
A
R
B
– many to one
A
R
B
A
R
B
– many to many
Ch. 5
81
Non binary relations
D u ratio n
D ata
D irecto r
H ead O f
D ep artm en t
P articip ate
A ssign ed
P ro ject
E m p lo yee
Ch. 5
82
Logic specifications
Examples of first-order theory (FOT) formulas:
• x > y and y > z implies x > z
• x=yy=x
• for all x, y, z (x > y and y > z implies x > z)
• x+1<x–1
• for all x (exists y (y = x + z))
• x > 3 or x < -6
Ch. 5
83
Specifying complete
programs
A property, or requirement, for P is
specified as a formula of the type
{Pre (i1, i2,..., in) }
P
{Post (o1, o2,..., om, i1, i2,..., in)}
Pre: precondition
Post: postcondition
Ch. 5
84
Example
• Program to compute greatest common
divisor
{i1 > 0 and i2 > 0}
P
{(exists z1, z2 (i1 = o * z1 and i2 = o * z2)
and not (exists h
(exists z1, z2 (i1 = h * z1 and i2 = h * z2) and h > o))}
Ch. 5
85
Specifying procedures
{n > 0} -- n is a constant value
procedure search (table: in integer_array; n: in integer;
element: in integer; found: out Boolean);
{found  (exists i (1  i  n and table (i) = element))}
{n > 0 }
procedure reverse (a: in out integer_array; n: in integer);
{for all i (1 i  n) implies (a (i) = old–a (n - i +1))}
Ch. 5
86
Specifying classes
• Invariant predicates and pre/post
conditions for each method
• Example of invariant specifying an array
implementing ADT set
for all i, j (1  i  length and 1  j  length and ij)
implies IMPL[i]IMPL[j]
(no duplicates are stored)
Ch. 5
87
Specifying non-terminating
behaviors
• Example: producer+consumer+buffer
• Invariant specifies that whatever has
been produced is the concatenation of
what has been taken from the buffer
and what is kept in the buffer
input_sequence = append (output_sequence,
contents(CHAR_BUFFER))
Ch. 5
88
A case-study using logic
specifications
• We outline the elevator example
• Elementary predicates
– at (E, F, T)
• E is at floor F at time T
– start (E, F, T, up)
• E left floor F at time T moving up
• Rules
– (at (E, F, T) and on (EB, F1, T) and F1 > F) implies
start (E, F, T, up)
Ch. 5
89
States and events
• Elementary predicates are partitioned into
– states, having non-null duration
– standing(E, F, T1, T2)
» assumption: closed at left, open at right
– events
• instantaneous (caused state change occurs at same time)
• represented by predicates that hold only at a particular time
instant
– arrived (E, F, T)
• For simplicity, we assume
• zero decision time
• no simultaneous events
Ch. 5
90
Events (1)
• arrival (E, F, T)
– E in [1..n], F in [1..m], T  t0, (t0 initial time)
• does not say if it will stop or will proceed, nor where it
comes from
• departure(E, F, D, T)
– E in [1..n], F in [1..m], D in {up, down}, T  t0
• stop (E, F, T)
– E in [1..n], F in [1.. m], T  t0
• specifies stop to serve an internal or external request
Ch. 5
91
Events (2)
• new_list (E, L, T)
– E in [1..n], L in [1.. m]*, T  t0
• L is the list of floors to visit associated with
elevator (scheduling is performed by the
control component of the system)
• call(F, D, T)
– external call (with restriction for 1, N)
• request(E, F, T)
– internal reservation
Ch. 5
92
States
• moving (E, F, D, T1, T2)
• standing (E, F, T1, T2)
• list (E, L, T1, T2)
– We implicitly assume that state predicates
hold for any sub- interval (i.e., the rules
that describe this are assumed to be
automatically added)
• Nothing prevents that it holds for larger interval
Ch. 5
93
Rules relating events and
states
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.
Ch. 5
94
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)
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)
Ch. 5
95
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 + Dts) and
first (L) > F,
implies
departure (E, F, up, Ta + Dts
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 + Dts and list (E, empty, Ta + Dts, Tp) and
first (L) > F
implies
departure (E, F, up, Ch.
Tp5)
96
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 + Dt)
R7: The event of stopping initiates standing for at least Dts.
stop (E, F, T)
implies
standing (E, F, T, T + Dts)
Ch. 5
97
R8: At the end of the minimum stop interval Dts, E remains
standing if there are no floors to service.
stop (E, F, Ts) and
list (E, empty, Ts + Dts, T)
implies
standing (E, F, Ts, T)
R9: Departure causes moving.
departure (E, F, D, T)
implies
moving (E, F, D, T, T + Dt)
Ch. 5
98
Control rules
Express the scheduling strategy (by describing “new_list”
events and “list” states)
Internal requests are inserted in the list from current
floor to top if the elevator is moving up
External calls are inserted in the list of the closest elevator
that is moving in the correct direction, or in a standing
elevator
Ch. 5
99
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, Ta, TR)) and
list (E, L, Ta, TR) and LF = insert_in_order(L, F, E)
implies
new_list (E, LF, TR)
Ch. 5
100
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)
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)
Ch. 5
101
Verifying specifications
• The system can be simulated by providing a state
(set of facts) and using rules to make deductions
standing (2, 3, 5, 7) elevator 2 at floor 3 at least
from instant 5 to 7
list(2, empty, 5, 7)
request(2, 8, 7)
new_list(2, {8}, 7)
 (excluding other events)
departure (2, up, 7 + Dts)
arrival (2, 8, 7 + Dts + Dta *(8-3))
Ch. 5
102
Verifying specifications
• Properties can be stated and proved via
deductions
new_list (E, L, T) and F  L
implies
new_list (E, L1, T1) and F  L1 and T1 > T2
(all requests are served eventually)
Ch. 5
103
Descriptive specs
• The system and its properties are
described in the same language
• Proving properties, however, cannot be
fully mechanized for most languages
Ch. 5
104
Algebraic specifications
• Define a heterogeneous algebra
• Heterogeneous = more than 1 set
• Especially useful to specify ADTs
Ch. 5
105
Example
• A system for strings, with operations for
– creating new, empty strings (operation new)
– concatenating strings (operation append)
– adding a new character at the end of a string
(operation add)
– checking the length of a given string (operation
length)
– checking whether a string is empty (operation
isEmpty)
– checking whether two strings are equal (operation
equal)
Ch. 5
106
Specification: syntax
algebra StringSpec;
introduces
sorts String, Char, Nat, Bool;
operations
new: () String;
append: String, String  String;
add: String, Char  String;
length: String  Nat;
isEmpty: String  Bool;
equal: String, String  Bool
Ch. 5
107
Specification: properties
constrains new, append, add, length, isEmpty, equal so that
for all [s, s1, s2: String; c: Char]
isEmpty (new ()) = true;
isEmpty (add (s, c)) = false;
length (new ()) = 0;
length (add (s, c)) = length (s) + 1;
append (s, new ()) = s;
append (s1, add (s2,c)) = add (append (s1,s2),c);
equal (new (),new ()) = true;
equal (new (), add (s, c)) = false;
equal (add (s, c), new ()) = false;
equal (add (s1, c), add (s2, c) = equal (s1,s2);
end StringSpec.
Ch. 5
108
Example: editor
• newF
– creates a new, empty file
• isEmptyF
– states whether a file is empty
• addF
– adds a string of characters to the end of a file
• insertF
– inserts a string at a given position of a file (the
rest of the file will be rewritten just after the
inserted string)
• appendF
– concatenates two files
Ch. 5
109
algebra TextEditor;
introduces
sorts Text, String, Char, Bool, Nat;
operations
newF: () Text;
isEmptyF: Text  Bool;
addF: Text, String  Text;
insertF: Text, Nat, String  Text;
appendF: Text, Text  Text;
deleteF: Text  Text;
lengthF : Text  Nat;
equalF : Text, Text  Bool;
addFC: Text, Char  Text;
{This is an auxiliary operation that will be needed
to define addF and other operations on files.}
Ch. 5
110
constrains newF, isEmptyF, addF, appendF, insertF, deleteF
so that TextEditor generated by [newF, addFC]
for all [f, f1,f2: Text; s: String; c: Char; cursor: Nat]
isEmptyF (newF ()) = true;
isEmptyF (addFC (f, c)) = false;
addF (f, newS ()) = f;
addF (f, addS (s, c)) = addFC (addF (f, s), c);
lengthF (newF ()) = 0;
lengthF (addFC (f, c)) = lengthF (f) + 1;
appendF (f, newF ()) = f;
appendF (f1, addFC (f2, c)) =
addFC (appendF (f1, f2), c);
equalF (newF (),newF ()) = true;
equalF (newF (), addFC (f, c)) = false;
equalF (addFC (f, c), new ()) = false;
equalF (addFC (f1, c1), addFC (f2, c2) =
equalF (f1, f2) and equalC (c1, c2);
insertF (f, cursor, newS ()) = f;
((equalF (f, appendF (f1, f2)) and (lengthF (f1) = cursor - 1))
implies
equalF (insertF (f, cursor, s), appendF (addF (f1, s), f2))) = true;
end TextEditor.
Ch. 5
111
Requirements for a notation
• Ability to support separation of
concerns
– e.g., separate functional specs from
• performance specs
• user-interface specs
•…
• Support different views
Ch. 5
112
Example of views
document production
data flow view (1)
Predefined
Text skeletons
Predefined
Formats
User
Formatting
options
Customer data
(name, type of
document)
Docum ent
production
Customers
Print
Docum ent
Ch. 5
113
Control flow view (2)
Get user nam e
Search i n
Customers
Get other d ata from
the data base
Get approp ri ate text
skeletons from
predefi ned text l ibrary
Get other rel evant data
from user interacti on
Comp ose the docume nt by choosi ng
form atting opti ons
(thi s i nvol ves interacti on wi th the user and
access to the Formats data base)
Pri nt docum ent
(b)
Ch. 5
114
UML notations
• Class diagrams
– describe static architecture in terms of
classes and associations
– dynamic evolution can be described via
Statecharts (see later)
• Activity diagrams
– describe sequential and parallel
composition of method executions, and
synchronization
Ch. 5
115
An activity diagram
[c1 ]
A
[c3 ]
E
[c4 ]
[c2 ]
(1 )
F
B
C
D
G
end
(2 )
Ch. 5
116
Building modular
specifications
• The case of algebraic specifications
– How to combine algebras taken from a
library
– How to organize them in a hierarchy
Ch. 5
117
Algebras used by StringSpec
algebra BoolAlg;
introduces
sorts Bool;
operations
true ()  Bool;
false ()  Bool;
not : Bool  Bool;
and: Bool, Bool  Bool;
or: Bool, Bool  Bool;
implies: Bool, Bool  Bool;
 : Bool, Bool  Bool;
constrains true, false, not, and, or, implies,  so that
Bool generated by [true, false]
for all [a, b: Bool]
not (true) = false;
not (false) = true;
a and b = not (not (a) or not (b));
a implies b = not (a) or b;
…
end BoolAlg.
Ch. 5
118
Algebras used by StringSpec
(cont.)
algebra NatNumb;
introduces
sorts Nat, Bool;
operations
0: ()  Nat;
Succ: Nat  Nat;
+ : Nat, Nat  Nat;
- : Nat, Nat  Nat;
= : Nat, Nat  Bool;
…
constrains 0, Succ, +, -, =,..., so that
NatNumb generated by [0, Succ]
…
end NatNumb.
Ch. 5
algebra CharAlg;
introduces
sorts Char, Bool;
operations
‘a’: ()® Char;
‘b’ : ()® Char;
…
end CharAlg.
119
StringSpec revisited
algebra StringSpec;
imports BoolAlg, NatNumb, CharAlg;
introduces
sorts String, Char, Nat, Bool;
operations
new: ()  String;
…
end StringSpec.
Ch. 5
120
Incremental specification of
an ADT
• We want to target stacks, queues, sets
• We start from "container" and then
progressively specialize it
• We introduce another structuring clause
– assumes
• defines inheritance relation among algebras
Ch. 5
121
Container algebra
algebra Container;
imports DataType, BoolAlg, NatNumb;
introduces
sorts Cont;
operations
new: ()  Cont;
insert: Cont, Data  Cont;
{Data is the sort of algebra DataType, to which
elements to be stored in Cont belong}
isEmpty: Cont  Bool;
size: Cont  Nat;
constrains new, insert, isEmpty, size so that
Cont generated by [new, insert]
for all [d: Data; c: Cont]
isEmpty (new ()) = true;
isEmpty (insert (c, d)) = false;
size (new ()) = 0;
end Container.
Ch. 5
122
Table specializes Container
algebra TableAlg;
assumes Container;
introduces
sorts Table;
operations
last: Table  Data;
rest: Table  Table;
equalT : Table, Table  Bool;
delete: Table, Data  Table;
constrains last, rest, equalT, delete, isEmpty, new, insert so that
for all [d, d1, d2: Data; t, t1, t2: Table]
last (insert (t, d)) = d;
rest (new ()) = new ();
rest (insert (t, d)) = t;
equalT (new (), new ()) = true;
equalT (insert (t, d), new ()) = false;
equalT (new (), insert (t,d)) = false;
equalT (t1,t2) = equalD(last (t1), last (t2)) and
equalT (rest (t1),rest (t2));
delete (new (), d) = new ();
delete (insert (t,d),d) = delete (t, d);
if not equalD(d1, d2) then
Ch. 5(delete (t, d2), d1);
delete (insert (t, d1), d2) = insert
end TableAlg.
123
Queue specializes Container
algebra QueueAlg;
assumes Container;
introduces
sort Queue;
operations
last: Queue  Data;
first: Queue  Data;
equalQ : Queue , Queue  Bool;
delete:Queue  Queue;
constrains last, first, equalQ, delete, isEmpty, new, insert so that
for all [d: Data; q, q1, q2: Queue]
last (insert (q, d)) = d;
first (insert (new(), d) = d
first (insert (q, d)) = if not isEmpty (q) then first (q);
equalQ (new (), new ()) = true;
equalQ (insert (q, d), new ()) = false;
equalQ (new (), insert (q, d)) = false;
equalQ (insert (q1, d1), insert (q2, d2)) = equalD (d1, d2) and
equalQ (q1,q2);
delete (new ()) = new ();
delete (insert (new (), d)) = new ();
if not equalQ (q, new ()) then
delete (insert (q,d)) = insert (delete
(q), d);
Ch. 5
end QueueAlg.
124
A graphical view
Queue
Algebra
Table
Algebra
Container
Algebra
Bool
Algebra
Legend:
Nat
Algebra
DataType
Algebra
imports relation
assumes relation
Ch. 5
125
A richer hierarchy
Set
M ultiset
Sorted
T able
T ree
Queue
Algeb ra
T able
Algeb ra
Conta iner
Algeb ra
Sorted
DataT ype
Array
Algeb ra
Bool
Algeb ra
Nat
Algeb ra
Ch. 5
DataT ype
Algeb ra
126
From specs to an
implementation
• Algebraic spec language described so
far is based on the "Larch shared
language"
• Several "interface languages" are
available to help transitioning to an
implementation
– Larch/C++, Larch/Pascal
Ch. 5
127
Using Larch/Pascal for
StringSpec
type String exports isEmpty, add, append,...
based on Boolean, integer, character
function isEmpty (s: String) : Boolean
modifies at most [ ] {i.e., it has no side effects};
procedure add (var s : String; c : char)
modifies at most [s]
{modifies only the string parameter s};
function length (s: String) : integer
modifies at most [ ] ;
procedure append (var s1, s2, s3: string)
modifies at most [s3]
{only s3, the result of the operation, is modified};
end StringSpec.
Ch. 5
128
Modularizing finite state
machines
• Statecharts do that
• They have been incorporated in UML
• They provide the notions of
– superstate
– state decomposition
Ch. 5
129
Sequential decomposition
--chemical plant control example-N o rm a l
A n o m a ly D etectio n
R eco v ery S u ccess
R eco v ery
P ress
R eco v ery
Id en tifica tio n
T em p
D one
P ressu re
A ctio n
D one
T em p era tu re
A ctio n
Ch. 5
R eco v ery F a ilu re
130
Parallel decomposition
Idle
start
stop
C oncurrentW ork
w rite
1
P1
w rite
C1
read
produce
0
read
read
w rite
2
P2
P roducer
B uffer
Ch. 5
consum e
C2
C onsum er
131
Object state diagram using
Statecharts
Top
Push(item)
Empty
NotEmpty
y
Pop[stack contains 1 item]
Push(item)
Pop[stack contains more than 1 item]
Ch. 5
132
Modularizing logic
specifications: Z
• System specified by describing state
space, using Z shemas
• Properties of state space described by
invariant predicates
– predicates written in first-order logic
• Operations define state transformations
Ch. 5
133
The elevator example in Z
Ch. 5
134
Complete state space
attempt #1
Ch. 5
135
Complete state space
attempt #2
Ch. 5
136
Complete state space
final
Ch. 5
137
Operations
(1)
Ch. 5
138
Operations
(2)
Ch. 5
139
Specifications for the
end-user
• Specs should be used as common
reference for producer and user
• They help removing ambiguity,
incompleteness, …
• Can they be understood by end-user?
– They can be the starting point for a
prototype
– They can support some form of animation
(e.g., see Petri nets)
Ch. 5
140
Conclusions (1)
• Specifications describe
– what the users need from a system (requirements
specification)
– the design of a software system (design and
architecture specification)
– the features offered by a system (functional
specification)
– the performance characteristics of a system
(performance specification)
– the external behavior of a module (module
interface specification)
– the internal structure of a module (internal
structural specification)
Ch. 5
141
Conclusions (2)
• Descriptions are given via suitable
notations
– There is no “ideal” notation
• They must be modular
• They support communication and
interaction between designers and
users
Ch. 5
142
Descargar

Specification - Higher Education | Pearson