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