Submodule construction
for specifications with
input assumptions and
output guarantees
Gregor v. Bochmann
School of Information Technology and Engineering (SITE)
University of Ottawa
FORTE conference, Houston, November 2002
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
1
Thanks

I would like to express my thanks to




Philip Merlin with whom I did the first work in this
area in 1969
My PhD students Tao and Drissi whose work was on
equation solving
Nina Yevtushenko for some joint work in this area and
for identifying the generalization as a goal
My colleague Cory Butz who gave a talk on stochastic
databases during which I saw that databases provide
a very general framework for equation solving
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
2
Equation solving: Integer division


Multiplication: R1 * R2 = ?
Equation solving: R1 * X = R3


What is the value of X ?
Solution: definition of the division operation


Written “ X = R3 / R1 ”
What does it mean ?


X = biggest Y such that R1 * X ≤ R3
Note: in many cases, there is no exact solution, that
is, there is no X such that R1 * X = R3

For instance: 7 / 3 = 2, and 3 * 2 = 6 ≤ 7
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
3
Context of this talk

Multiplication  Machine composition
Division  Submodule construction

Example:

(“equation solving”)
?
a2
R1
a3
a1
R2
a2
R3
R1
a1
a3
X
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
4
Overview







Machine composition and equation solving
Applications
Solution formulas
A generalization: Relational databases
The cases of labelled transition systems (LTS)
and synchronous LTS
The case of specifications based on assumptions
and guarantees: e.g. synchronous FSMs, IOAutomata and asynchronous FSMs
Conclusions
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
5
Equation solving for machines
a2
R3
R1


a1
a3
X
Given machine R1 and specification R3 for the
behavior of the composition of R1 with X, find a
behavior of machine X such that
hide a3 in (R1 ∞ X) ≤ R3
Meaning of ≤ : set inclusion of possible
execution sequences (“traces”, i.e. sequences of
interactions), also called trace inclusion
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
6
Applications of
machine equation solving

Communication protocols





Protocol design (Merlin-Bochmann, 1980)
Design of communication gateways
Controller design for discrete event
systems
Component reuse, e.g. in software
engineering
Embedded testing
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
7
Communication protocol design
a2
R3
PE1
a1
PE2
a2
R3
R1
a1
a3
X
S

Protocol entities PE1 and PE2 use the underlying
service S and provide the service R3 to the users
of the protocol



PE1 and S are given
PE2 is to be found
R1 corresponds to (PE1 ∞ S)
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
8
Communication gateways
E2E
a2
R3
PE1
adapter
a1
PE2
S

a1
PE’1
PE’2
S’
Given



a2
R’3
desired end-to-end communication service E2E
Protocols in the two networks (different)
To be found: gateway behavior (shown by red box)
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
9
Controller design
a2
a1
Desired properties
System to be
controlled

Controller
Applications in process control, robotics, etc.


a3
Also called “Discrete event systems” (a separate
research community, e.g. [Ramage-Wonham, 1989]
and many subsequent papers)
Distinction between non-controllable and
controllable interactions (like input/output)
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
10
Component reuse
a2
a1
Module to be built
Submodule
to be re-used


a3
New subm.
to be built
A given submodule does not completely
correspond to the specification of the system to
be built
An additional submodule to be built (and
designed throught equation solving) makes up
the “difference”
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
11
Embedded testing
a2
a1
Properties of composed system
Component
assumed
correct


a3
Component
under test
If internal interactions (i.e. a3 ) are not visible, only the
properties of the composed system can be observed
The most general behavior of the SUT that leads to
conforming behavior for the composed system, is the
solution of submodule construction.

This behavior is often more general than the specification for the SUT;
the difference can not be observed.
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
12
Equation solving for
labelled transition systems
a2
R3

Rendezvous interactions




R1
a1
a3
X
a3: between R1 and X
a2: between R1 and environment
a1: between X and environment
Behavior definition

set of allowed execution sequences

e.g. for X: execution sequences over interactions at
a3 or a1
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
13
The problem and its solution

Problem:

hide a3 in (R1 ∞ X) ≤ R3
Solution: X = (a1U a3)* \ (minus)
Find most general X (largest set of execution
sequences) such that
any sequence that could lead to an observable execution sequence not in R3 , i.e.
hide a2 in (R1 ∞ ( (a1U a2)* \ R3 ) )
a2
R3
R1
a1
a3
R3
a2
X
R1
a1
a3
X
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
14
A comment
Since all execution sequences of X must go in interaction
with R1 and R3, we may replace the chaos for X with all
sequences that are obtained by the composition of R1 and
R3, that is [Merlin and Bochmann, 1980]


Solution: X = hide a2 in (R1 ∞ R3 ) \ (minus)
hide a2 in (R1 ∞ ( (a1U a2)* \ R3 ) )
a2
R3
R1
a1
a3
R3
a2
X
R1
a1
a3
X
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
15
Equation solving for
synchronous automata

Synchronous communication
Simultaneous interactions at all
interfaces; at each clock pulse,
there is a vector of interactions


a2
R3
R1
a1
a3
X
Behavior definition

set of allowed sequences of interaction vectors

e.g. for X: the interaction vectors include interactions at a3 and a1
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
16
Solution of equation solving

Identical form of formulas

Meaning of operators have changed


∞ : synchronous composition
hide operator

ignores a component of the vector
[Yevtushenko et al., 1999]
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
17
Relational database (intro)


A DB is a set of relations
A relation is a table




Each column is an attribute
Each row is an “object”
An element at position (ai, ok) in the table
represents the value that object ok takes for
attribute ai
With each attribute ai is associated a set of
possible values Di
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
18
Relational database concepts
Formal definitions:



Attributes: A = {a1, a2, … an}
Attribute values: D = U Di
Relation over Ar (Ar  A), written R[Ar]:
(possibly infinite) set of mappings T: Ar  D
with T(ai) ε Di
Note: each mapping corresponds to a row
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
19
Example
R1
R2 Name
Project
Name
Age
Salary
Fred
53
50000
Fred
BigOne
Paul
50
60000
Alice
BigOne
Alice
21
40000
Fred
SmallOne
Suzanne
35
50000
Suzanne
SmallOne
Bob
20
30000
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
20
Relational operators

Projection
Given R[Ar] and Ax  Ar ,
the projection of R[Ar] onto Ax , written projAx (R) ,
is a relation over Ax with
T ε projAx (R) iff exists T’ ε R s.t.  ai ε Ax: T(ai) = T’(ai)

Join
Given R1[A1] and R2[A2], the join of R1 and R2 , written R1 ∞ R2 , is
a relation over A1 U A2 with
T ε (R1 ∞ R2) iff projA1 (T) ε R1 and projA2 (T) ε R2

Chaos
Given Ax  A, the chaos over Ax , written Ch[Ax], is the relation
which includes all mappings T: Ax  D with T(ai) ε Di
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
21
Example
R1
R2 Name
Project
Name
Age
Salary
Fred
53
50000
Fred
BigOne
Paul
50
60000
Alice
BigOne
Alice
21
40000
Fred
SmallOne
Suzanne
35
50000
Suzanne
SmallOne
Bob
20
30000
Project


Proj{Project} (R2) =
R1 ∞ R2 =
BigOne
SmallOne
Name
Age
Salary
Project
Fred
Fred
Alice
Suzanne
53
53
21
35
50000
50000
40000
50000
BigOne
SmallOne
BigOne
SmallOne
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
22
Equation solving for
relational databases

We consider



R1
a1
a3
Three attributes a1, a2 , a3
Two relations R1 [{a3, a2 }], R3 [{a1, a2 }]
Problem:
satisfying

a2
R3
X
What is the biggest relation X [{a1, a3 }]
proj{a1, a2 }(R1 ∞ X)  R3
Solution: X = Ch[{a1, a3 }] \
proj{a1, a3 }(R1 ∞ (Ch[{a1, a2 }] \ R3 ) )

Proof: see paper

Greneralization to more complex attribute structures is also easy
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
23
An example



a2
R3
R1
D1 = {e}
D2 = {aa, ab, ba, bb}
D3 = {c, d}
R3 a1 a2
e
ab
a1
a3
X
R1 a2
a3
ab
c
ab
d
X = Ch[{a1, a3 }] \ proj{a1, a3 }(R1 ∞ (Ch[{a1, a2 }] \ R3 ) ) aa
Ch[{a1, a2 }] \ R3 )
a1 a2
e
aa
e
ba
e
bb
R1 ∞ (Ch[{a1, a2 }] \ R3 )
a1
a2
a3
e
aa
d
d
Ch[{a1, a3 }]
a1 a3
X a1 a3
e
e
c
e
d
c
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
24
A special case:
Trace specifications


Attributes  Interfaces
Di = Ii *
that is, all finite sequences of elements of Ii , the
possible interactions at the interface ai (the “alphabet” at interface ai)

Machine behavior  Relation
Each row (DB object) represents a possible execution
history (“trace”) ; the value for each attribute
describes the interaction sequence occurring at the
corresponding interface during that trace
Synchrony constraint: The interaction sequences at the
different interfaces for a given trace are of equal
length
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
25
Two sub-cases:
- synchronous operation (as above)
- interleaving semantics (below)


Attributes  Interfaces
Di = (Ii U {null} ) *
(as synchronous case, except that there is a real
interaction at only one interface at a time;
“interleaving semantics” )

Machine behavior  Relation
As in synchronous case, except that the “interleaving
constraint” is satisfied for all mappings of a relation,
that is, for any j, the j-th element of T(ai) is non-null
for at most one attribute ai
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
26
Algorithms for equation solving
Solution: X = Ch[{a1, a3 }] \ proj{a1, a3 }(R1 ∞ (Ch[{a1, a2 }] \ R3 ) )

Algorithms for operations ∞ , \ , proj


In general not possible (infinite sets of
mappings)
For finite state models :



Polynomial complexity for
∞ , proj
proj introduces non-determinism
\ requires conversion to deterministic models,
which has exponential complexity
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
27
Example
Notation (x2,x3)
Notation (x2,x1)
a2
R3
{a, b, n}
R1
a3
{c, d, n}
a1
(a,n)
{n}
1
(a,n)
(n,n)
(a,n)
2
(n,c)
2
6
3
2
1
3
(b,n)
(n,d)
(b,n)
(b,n)
R3
X
R1
4
(n,d)
(n,n)
(a,n)
(a,n)
5
2
1
3
(b,n)
Notation (x1,x2,x3)
(a,n)
(b,n) (a,n)
(n,n)
(b,n)
(n,n)
(n,a,n)
fail
1,1
(n,b,n)
2,2 (n,n,c)
3,3
2
R3 completed
(n,n)
R1 join R3
(n,n)
2,2 (n,c)
(n,n)
4,3
5,3
Notation (x1,x3)
4,3
5,3
(n,n)
(n,a,n)
6,fail
(n,n)
(n,d)
proj (R1 join R3 )
determinized
(n,b,n)
6,1
3,3
1,1
6,1
(n,n,d)
(n,n,d)
Notation (x1,x3)
(n,a,n)
(n,n)
6,1
6,fail
2,2 (n,c)
(n,n)
6,1
3,3
1,1
Solution
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
28
Systems with input and output

Nature of input/output (non-rendezvous)



Output: time and parameters of an interaction are
determined by the system component producing the
output
Input: The component receiving the interaction
cannot influence the time nor parameter values
Specification of component behavior


Output: The specification gives guarantees about
timing and parameter values
Input: The specification may make assumptions about
timing of inputs and the received parameter values
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
29
Specification paradigms
with hypothesis and guarantees

Software

Pre- and postconditions of a procedure call


They define hypotheses on input parameters, and
guarantees on output parameters, respectively
Finite state machines (state-deterministic)

Unspecified input: hypothesis about the
behavior of the environment: this input will
not occur when the machine is in this state
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
30
Component specification and
interconnection


Each attribute of a relation is either input or
output
Constraint on component interconnection


No output conflicts: For each interface, there is only
one connected component for which the
corresponding attribute is output
For trace specifications: Unit delay constraint

Output(s) at time t depend only on previous
interactions of the same component (not on the input
received at time t) [e.g. Broy, Lamport]

In FSM context: corresponds to Moore machine
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
31
Conformance to specifications

Given a specification R and a trace T





Either T e R (we say T conforms to R) or …
T has wrong input: all prefixes of T up some time t conform to R,
but there is wrong input at time (t+1)
T has wrong output: similarly
T has wrong input and output at the same time instant
A component conforms to a specification R iff no
trace T in which the component participates has
wrong output in respect to R

Note: if a trace has wrong input, nothing can be assumed
about wrong output at a later time instance
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
32
Equation solving for trace
specifications with input/output
a2
R3
R1

a1
a3
X
Find most general specification X such that
any trace T of the composition of R1 and X
has the following properties:


proj{a1, a2} (T) conforms to R3
If proj{a1, a2} (T) has no wrong input in respect to R3
then proj{a2, a3} (T) has no wrong input in resp. to R1
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
33
Solution formula

Notation:




RWO(t) = set of traces that have wrong output
in respect to R at time instant t
RWI(t) : similarly for wrong input
Ut : union over all values of t
Solution:
X = Ch[{a1, a3 }] \ proj{a1, a3 } Ut (
R1 ∞ R3WO(t) U R1WI(t) ∞ R3 U R1WI(t) ∞ R3WO(t)
)
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
34
Solution algorithms for I/O

Synchronous FSMs



Can be easily derived from above formula
The special case of completely defined, deterministic
machines was already solved by Kim et al.
Interleaving semantics


IO-Automata


Simplification: Never wrong input and output at the same
time instant
Jawad Drissi (PhD thesis)
Communicating FSMs

Yevtushenko and Petrenko
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
35
Extensions
of the specification formalisms

More powerful specification languages


Petri nets, CSP, LOTOS, etc.
Different conformance relations

Safeness


Liveness - progress (some good interaction will occur)




Trace semantics (as discussed here)
Liveness [Thistle]
Absense of blockings [Tao, PhD thesis]
Optional and required progress [Drissi, PhD thesis]
Real-time aspects

Timed automata [Grenoble; work on DES; Drissi, PhD thesis]
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
36
Conclusions (i)

New results presented here:

Solution formula for equation solving in the
context of relational databases


Equation solving for component composition based
on trace semantics (synchronous and interleaving
case) as special cases
Solution formula for trace semantics with
input and output
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
37
Conclusions (ii)

Application areas:






Protocol design (Merlin-Bochmann, 1980)
Design of communication gateways
Controller design
Component reuse, e.g. in software engineering
Embedded testing
Future work

More powerful specification paradigms



e.g. interaction parameters
Tools
Practical design methodology based on formal
methods
Gregor v. Bochmann, University of Ottawa
Submodule construction for specifications with I/O, Nov. 2002
38
Descargar

Document