A Verification Concept for SDL Systems and its Application to the Abracadabra
Protocol
Markus Rinderspacher
Institut für Logik, Komplexit?t und Deduktionssysteme
Interner Bericht 14/94
Abstract
SDL is a specification language to specify distributed systems. Especially it is suitable for communication protocols. In some cases however it is not enough to describe just the behaviour of a protocol, but there are formulated some additional properties as requirements of the SDL system. A formalism convenient to describe them is for example first order logic. Our approach is to prove such properties with methods of automated reasoning after transforming the SDL specification into a first order logic specification. The proofs are done with the program verification system Tatzelwurm, especially with its prover.
Practical experience shows that it is convenient to do a proof in two steps. In the first step the behaviour of the system is calculated out of the behaviour of the agents. The proofs of this step is independent of the property to prove. In this report we give a proof methods containing instructions how the arguments are applied during these proofs. It is shown how reachability analysis is done during a formal proof and how fairness arguments are applied.
The report contains two papers, where the first one describes the formal basis of the method and shows the proof obligations occurring verifying a communication protocol. The second paper shows how some tedious tasks can be done more elegant using rewrite rules and recursive equations.
In the appendix we give two examples out of the verification of the Abracadabra Protocol.
Contents
1. Proof Structuring with Fixed Point Theory4 1.1. Introduction4 1.
2. Fixed points of Functions over Lists5 1.
3. Development of a Correctness Proof6 1.
4. Practical experience13
1.5. Conclusion13
2. Systematic Verification of in SDL specified Protocols14 2.1. Introduction14 2.2. The Description of the behaviour of a SDL system15 2.
3. Explicit behaviour21 2.3.1. Solving System Equations21 2.3.1.1.An example21 2.3.2. Liveness27
2.4. Evaluation28
3. References30 Appendix:
I. The specification of the Abracadabra Protocol31 II.The complete presented example33 III. Another example48
1. Proof Structuring with Fixed Point Theory
Abstract
Starting from a purely functional description of a communication protocol, we present a method how correctness proofs including safety- and progress properties can be developed systematically with an automatic theorem prover. We show how a complex proof can be divided into smaller ones due to proof arguments typically occurring in the area of protocol verification. Experience with this method shows that proofs can be developed with an acceptable amount of work.
1.1. Introduction
The objective we pursue with our work is to verify properties of communication protocols. We start with an automata based description of the protocol and a property p given in terms of first-order logic. Due to Broy [Bro87,91] we model the behaviour of the protocol agents with functions over streams and the system behaviour with its least fixed point c. If we use this formalism, we can reduce the verification problem to a proof of the theorem
lf(c) → p(c).
lf is a logical formula formalizing that c is the least fixed point of the system regarded. To find the proof of this theorem we use the program verification system Tatzelwurm [K?U891] with its integrated tableau prover. This prover is designed to prove formulae occurring in program verification. It is enlarged by decision procedures [K?U892] for theories typically occurring in the verification of programs and protocols, like arithmetic, records and lists. Furthermore Tatzelwurm supports interactive theorem proving with a powerful user-interface. Interactive proving is necessary, since automatic proofs of such complex problems seem to be impossible because of the enormous search space, which must be managed.
Nevertheless interactive theorem proving is not the solution of all problems. If we try to find a proof for the above theorem, we will get completely lost, if we have no method how to find this proof.
The presented method is part of our experience with the verification of the Abracadabra protocol [Isc89]. There we took a paper [Bro87], which suggested, how the behaviour of the Abracadabra-protocol can be modelled and how its correctness proof can be found. We did this proof with Tatzelwurm and were successful after we had made some essential changes to the suggestions of Broy.
Respect to our experience we suggest for future verification projects two steps:
(1) calculate the fixed point of the system explicitly and
(2) prove the property.
Calculation of the fixed point is a subgoal occurring in every protocol verification project. It causes a lot of work, so that here a method reduces proof expense.
We organize this paper by giving in Section 2 some results of fixed point theory and especially
the fixed point theorem, the basis of our reasoning.
In Section 3 we will give a formalization of a protocol and show that a correctness proof can be systematically developed applying well-known arguments like reachability and fairness. Section 4 collects some experience obtained proving with Tatzelwurm and finally Section 5 concludes the results and gives hints, how to continue in future.
1.2. Fixed points of Functions over Lists
In this section we want to give some results of fixed point theory, which is the basis for our later argumentation. We regard fixed points in complete partial orders. The following definitions and theorems can be found in [Loe87].
Let (S, ≤) be a partial order, then an element m ∈ S is called the least(greatest) element of a set S, if m ≤ s (s ≤ m) for all s ∈ S
Definition 1.2.1.: (Least Upper Bounds)
Let (D, ≤) be a partial order and S a (possibly empty) subset of D. An element u ∈ D is said to be an upper bound of S (in D), if d ≤ u for all d ∈ S; u is said to be the least upper bound (lub) of S (in D), if u is the least element of the set of all upper bounds of S in D.
Note that the least upper bound is uniquely determined, if it exists. In the following a totally ordered subset S of D is called a chain.
Definition 1.2.2.: (Complete Partial Orders)
A partial order (D, ≤) is a complete partial order (cpo), if the following two conditions hold:
1.The set D has a least element.
2.For every chain S in D the least upper bound S exists.
Definition 1.2.3.: (Continuity)
Let (D, ≤) and (E, ≤) be cpo's. A function f: D → E is said to be continuous, if for every chain S in D, f(S) = f(S).
Theorem 1.2.4.: (The Fixed Point Theorem)
Let (D, ≤) be a cpo and f: D → D be a continuous function. Then f has a (uniquely determined) least fixed point mf = {f i(⊥) | i ∈ Nat}, where ⊥ is the least element of the cpo (D, ≤).
Now we want to apply the fixed point theorem to lists and functions over lists. The following theorems are easy to prove. Let G be a set of objects and let L(G) be the possibly infinite lists with elements of G. The application of the fixed point theorem demands cpos and continuous functions. We have to add a least element ω to G and obtain a flat partial order (Gω, ≤). We define a prefix ordering ? on the lists and add an element ε, which is called the empty list. We
consider these lists L(Gω) as a subset of the function set ((Nat → Gω), ≤), which is known to be a cpo. The following theorem establishes that (L(Gω), ?) is a cpo. We simplify our notation in writing L instead of L(Gω), assuming the element sort of the list is a flat partial order.
Theorem 1.2.5.: (L(Gω), ?) is a sub-cpo of ((Nat → Gω), ≤)
Now we study the continuity of functions in more detail. We need some criteria, which allow to check, whether the functions are continuous.
At first we examine the standard list functions cons, car, cdr and an additional function app, which appends a list to a finite list.
Theorem 1.2.6.: The functions cons, car, cdr are continuous in their list argument. The function app is continuous in its second argument.
We write in the following & instead of cons and app. Examining the arguments allows us to determine, which of the constructors is meant. As shortcut we write m k for the list having exactly k elements m. Later we will describe processes by functions over lists. The following theorem allows us to construct continuous functions using continuous functions and some conditions. It will be used to establish the continuity of the functions defined 3.3 and 3.4. Theorem 1.2.7.:
Let I be a finite index set and i, j ∈ I. Let {f i | i ∈ I} ? [L → L] be a finite set of continuous functions and {h i | i ∈ I} ? [G → G]. Let B i ? L, where B i ∩B j = ? and i = L, with:
if l ? l’ and l ∈ B i then l’ ∈ B i.
By the following a continuous function f is defined:
(1)f(ε) = ε
(2)f(cons(g, l)) = cons(h
i (g), f
i
(l)) if cons(g, l) ∈ B i for all i ∈ I 1.3. Development of a Correctness Proof
In this section we want to show, how fixed point theory can be used to develop correctness proofs systematically. The example used here is taken out of the verification of the Abracadabra-protocol [Isc21], which operates over a full-duplex communication medium between two agents. The medium may occasionally lose messages, but will not disorder, corrupt, invent or duplicate messages.
The two stations communicate transferring Protocol Data Units (PDUs). The service, provided by the protocol must be reliable, in the sense that the protocol guarantees the transmission of the data, coming from the user of the service. We assume, that we know in advance which of agents is the sender and the receiver respectively. Also we split up the bidirectional medium into
two unidirectional media mu, having the same behaviour.
Fig 1.3.1. shows the system regarded in this paper, where the names in brackets are the functions describing the behaviour of the agents. The protocol has to transmit a sequence s of data. We have to proof that this sequence is eventually transmitted.
Fig. 3.1. The system regarded
The first problem, to be solved is the calculation of the system behaviour using the behaviour of the cooperating agents. To transmit the data the agents send and receive messages.Lists of messages are called streams. We describe the behaviour of the agents with continuous functions over streams, called stream processing functions. Then we define the behaviour of the system by a recursion equation, which has a solution due to the fixed point theorem.
The sender transmits s to the receiver by sending a stream c(s), which depends beside s on the implementation of the sender and on the input it gets from the medium. Due to [Bro87] c(s) is the solution of the equation c(s) = con(f1(lic(f2(c(s))))). Due to the fixed point theorem the solution is uniquely determined, provided the functions are continuous.
To define the behaviour of the agents we assume that a message is one of the in pairs different objects {em, cr, cc, dt, ak, dr, dc}. It is dt a two place, ak a one place function symbol and the rest are constant symbols. dt takes as argument a data and a control-bit and ak a control-bit. em is used to model, that the medium does not deliver one of the other messages. The control-bit is assumed to be one of the boolean objects {tt, ff}. We have a function symbol non, to define a function mapping tt to ff and vice versa. In the following are m, m’arbitrary messages, c, c’ streams, d, d’ data, s, s’ list of data and a, b boolean.
Definition 1.3.1.: (Medium Function)
A medium function f: L → L is a function having the following properties:
1f(ε) = ε
2.car(f(m & c)) = m or car(f(m & c)) = em
3.f(m & c) = f(m & ε) & f(c)
Lemma 1.3.2: A medium function is continuous
Proof: (a sketch) It is a well-known fact, that it is enough to prove that f is monotone and
f(S) ? f(S) for every chain S with an infinite number of elements
1.Monotony: Let c ? c’. If c is infinite, c’ is also infinite and c = c’. Then f(c) = f(c’),
which is sufficient for f(c) ? f(c’).
If c is a finite stream, we can write c’ = c & c’’. Since f(c) ? f(c) & f(c’’), f(c) ? f(c’) holds
2.f(S) ? f(S): Let S = {c i | i ∈ Nat} be a chain. Then f(S) := {f(c i ) | i ∈ Nat} is also a chain. Since S and f(S) have an infinite number of elements, so S and f(S) are infinite streams. Since f(S) is an infinite stream and f(S) ? f(S), f(S) = f(S) holds.
We show a sketch of the behaviour of the system in Fig. 1.3.1. It is shown by the following state transition diagrams and the parallel operator . The state labeled with x means termination and the transitions are labeled with pairs (i; o) of I/O-signals, where - means no input (output).We denote the indeterminism of the medium by τ-transitions. The other indeterminisms are occurring, because the diagram does not describe all the details. It is omitted that the agents‘sender and receiver have an additional boolean control variable, which makes them deterministic.
Fig. 1.3.2. The components of the system
Sender:Receiver:Medium:
em; em
dt; ak
em; cr
ak; dt em; dr The full behaviour of these agents is given by the following functions. For each state we define a function typically having three arguments, the input stream, the data to be transmitted, and the state of the control variable. If arguments are not necessary, we omit them.
Definition 1.3.3: (Sender)
A sender-function con is a function, having the following properties:
(Con)con(c, s) = cr & itc(c, s)
(Itc 1)itc(cc & c, d & s) = dt(d, tt) & itt(c, d & s, tt)
(Itc 2)itc(em & c, s) = cr & itc(c, s)
(Itt 1)itt(ak(a) & c, d & d’ & s, a) = dt(d’, non(a)) & itt(c, d’ & s, non(a))
(Itt 2)itt(ak(a) & c, d & ε, a) = dr & itd(c)
(Itt 3)(em = m ∨ cc = m ∨ m = ak(non(a)))
→ itt(m & c, d & s, a) = dt(d, a) & itt(c, d & s, a)
(Itd1)itd(dc & c) = ε
(Itd2)? dc = m → itd(m & c) = dr & itd(c)
(Id)For the rest of the streams the functions are the identity on their stream.
Definition 1.3.4: (Receiver)
A receiver-function lic is a function, having the following properties:
(Lic1)lic(cr & c) = cc & lib(c)
(Lic2)? cr = m → lic(m & c) = em & lic(c)
(Lib1)lib(dt(d, a) & c) = lit(dt(d, a) & c, tt)
(Lib2)(cr = m ∨ em = m) → lib(m & c) = cc & lib(c)
(Lit1)lit(dt(d, a) & c, a) = ak(a) & lit(c, non(a))
(Lit2)lit(dr & c, a) = lid(dr & c)
(Lit3)m = dt(d, non(a)) ∨ em = m → lit(m & c, a) = ak(non(a)) & lit(c, a)
(Lid1)lid(dr & c) = dc & lid(c)
(Lid2)? dr = m → lid(m & c) = dc & lid(c)
(Id)For the rest of the streams the functions are the identity on their stream.
Note that these functions are continuous respect to 1.2.7. We have described the system behaviour with stream-processing functions of its components and the equation c(s) = con(f1(lic(f2(c(s))))). To prove properties however we have to solve this equation, which is the same as to calculate the fixed point explicitly.
We do this by manipulating the fixed point equation in a systematic way. In our example we define 6 more equations and fixed points and 16 theorems describing the relations between these fixed points.
At first we give these equations and theorems and then we show using an example how we get the fixed point equations and the theorems successively.
We define fixed points by following equations:
)c(s) = con(f1(lic(f2(c(s)))))
(F
)r1(s) = itc(f1(cc & lib(f2(r1(s)))), s)
(F
1
(F
)s ≠ε→ r2(s) = itt(f1(lib(f2(dt(car(s), tt) & r2(s)))), s, tt)
2
)s ≠ε→ r3(s, a, non(a)) = itt(f1(ak(non(a)) & lit(f2(r3(s, a, non(a))), a)), s, non(a))
(F
3
)s ≠ε→ r4(s, a, a) = itt(f1(lit(f2(dt(car(s), a) & r4(s, a, a)), a)), s, a)
(F
4
(F
)r5(a) = itd(f1(lit(f2(dr & r5(a)), a)))
5
)r6 = itd(f1(dc & lid(f2(r6))))
(F
6
The relations between the fixed points are given by the following theorems:
)c(s) = cr & r0(s)
(S
1
)car(f2(cr & r0(s))) ≠ em → r0(s) = r1(s)
(S
2
(S
)car(f2(cr & r0(s))) = em → r0(s) = cr & r0(s)
3
(S
)s ≠ε∧ car(f1(cc & lib(f2(r1(s))))) ≠ em → r1(s) = dt(car(s), tt) & r2(s)
4
(S 5)
car(f 1(cc & lib(f 2(r 1(s))))) = em → r 1(s) = cr & r 1(s)(S 6)
car(f 2(dt(car(s), tt) & r 2(s))) ≠ em → r 2(s, i, k) = r 3(s, ff, tt)(S 7)
s ≠ ε ∧ car(f 2(dt(car(s), tt) & r 2(s))) = em → r 2(s) = dt(car(s), tt) & r 2(s)(S 8)
s ≠ ε ∧ cdr(s) ≠ ε ∧ car(f 1(ak(non(a)) & lit(f 2(r 3(s, a, non(a))), a))) ≠ em → r 3(s, a, non(a)) = dt(car(cdr(s)), a) & r 4(cdr(s), a, a)(S 9)s ≠ ε ∧ car(f 1(ak(non(a)) & lit(f 2(r 3(s, a, non(a))), a))) = em
→ r 3(s, a, non(a)) = dt(car(s), non(a)) & r 3(s, a, non(a))
(S 10)s ≠ ε ∧ car(f 2(dt(car(s), a) & r 4(s, a, a))) ≠ em → r 4(s, a, a) = r 3(s, non(a), a)
(S 11)s ≠ ε ∧ car(f 2(dt(car(s), a) & r 4(s, a, a))) = em
→ r 4(s, a, a) = dt(car(s), a) & r 4(s, a, a)
(S 12)s ≠ ε ∧ cdr(s) = ε ∧ car(f 1(ak(non(a)) & lit(f 2(r 3(s, a, non(a))), a))) ≠ em
→ r 3(s, a, non(a)) = dr & r 5(a)
(S 13)car(f 2(dr & r 5(a))) ≠ em → r 5(a) = r 6
(S 14)car(f 2(dr & r 5(a))) = em → r 5(a) = dr & r 5(a)
(S 15)car(f 1(dc & lid(f 2(r 6)))) ≠ em → r 6 = ε
(S 16)car(f 1(dc & lid(f 2(r 6)))) = em → r 6 = dr & r 6
As an example we show how we can deduce the fixed point equation F 2 and the theorems S 4 and S 5 from F 1.
(F 1) r 1(s) = itc(f 1(cc & lib(f 2(r 1(s)))), s)
Due to the indeterminism of the medium we have to treat two cases.
1. Suppose f 1(cc & lib(f 2(r 1(s)))) = cc & f 1(lib(f 2(r 1(s)))).
If we assume, that s ≠ ε, we get with the definition (Itc 1 ) of 1.3.3.
r 1(s) = dt(car(s), tt) & itt(f 1(lib(f 2(r 1(s)))), s, tt), which leads to
cdr(r 1(s)) = itt(f 1(lib(f 2(dt(car(s), tt) & cdr(r 1(s))))), s, tt),
which is a fixed point equation, which has a least fixed point, we name it r 2(s). We get:
(F 2) s ≠ ε → r 2(s) = itt(f 1(lib(f 2(dt(car(s), tt) & r 2(s))), s, tt).
Since the least fixed point is uniquely determined, it is r 1(s) = dt(car(s), tt) & r 2(s).
We get (S 4) by collecting the assumptions we made.
2. We assume f 1(cc & lib(f 2(r 1(s)))) = em & f 1(lib(f 2(r 1(s)))).
With the definition (Itc 2 ) of 1.3.3. we get
r 1(s) = cr & itc(f 1(lib(f 2(r 1(s)))), s), which leads to
cdr(r 1(s)) = itc(f 1(lib(f 2(cr & cdr(r 1(s))))), s)
Applying the definition of the medium and (Lib 2) of 1.3.4. we get
cdr(r 1(s)) = itc(cc & f 1(lib(f 2(cdr(r 1(s))))), s)
Since the least fixed point is uniquely determined, it′s r 1(s) = cr & r 1(s).
We get (S 5) by collecting the assumptions we made.
We received the theorems S 1, ..., S 16 by manipulating of the fixed point equations. We illustrate them in the following diagram graphically. We got the insight that manipulation of fixed point equations in the described way is a reachability analysis during a proof. The fixed points can be regarded as states and the relations between the fixed points can be viewed as reachability graph. In this case the graph describes the behaviour on the senders point of view. The sender is not able to recognize, whether the medium described by f 2 transmits the signal or not. This is reflected by the τ-transition in the diagram.
Fig. 1.3.3. Relations between the fixed points
em; dt We have examined the system behaviour without fairness until now. Fairness should guarantee that the system eventually leaves a state after entering it. We systematically derive a formulation of the system behaviour including fairness. To speak in terms of Fig. 1.3.3. we show that the small loops eventually terminate, provided that the medium is fair .
Definition 1.3.5: (Fair Medium Function)
A fair medium function f is a medium function with the following additional property
? k. f(m k+1 & c) = f(em k & m & c)
With this property we are able to prove following theorems, which enlarges the first formalization of the system to a formalization containing liveness.
(S a ) ? k. c(s) = cr k+1 & r 1(s)
(S b ) s ≠ ε → ? k. r 1(s) = cr k & dt(car(s), tt) & r 2(s)
(S c ) s ≠ ε → ? k. dt(car(s), tt) & r 2(s) = dt(car(s), tt)k+1 & r 3(s, ff, tt)
(S d ) s ≠ ε ∧ cdr(s) ≠ ε
→ ? k. r 3(s, a, non(a)) = dt(car(s), non(a))k & dt(car(cdr(s)), a) & r 4(cdr(s), a, a)
(S e ) s ≠ ε → ? k. dt(car(s), a) & r 4(s, a, a) = dt(car(s), a)k+1 & r 3(s, non(a), a)
(S
f
) s ≠ε∧ cdr(s) = ε→? k. r3(s, a, non(a)) = dt(car(s), non(a))k & dr & r5(a)
(S
g
) ? k. dr & r5(a) = dr k+1 & r6
(S
h
) ? k. r6 = dr k
It is now possible to prove properties of the formalized system. We prove properties, which are formalized by requirements on fixed points with induction over the list s. Induction over lists
demands that the lists are finite. Note that the loop consisting of state r
3 and r
4
is terminating, if
the list s is finite.
We proof now by induction the property, that the sender transmits all the data of s. Let k be a list of integers. To express a property at first we define functions messc and messt, which extract the transmitted data out of a list of messages. messc and messt have the following properties:
(1) messc(ε) = messt(ε, a) = ε
(2) messt(dt(d, a) & c, a) = d & messt(d, non(a))
(3) messt(dt(d, non(a)) & c, a) = messt(dr & c, a) = messt(c, a)
(4) messc(cr & cr & c) = messc(cr & c)
(5) messc(cr & dt(d, a) & c) = messt(dt(d, a) & c, tt)
(6) messc(cr & dr & c) = messt(dr & c, tt)
(7) exp(ε, k, a) = ε
(8) exp(d & s, i & k, a) = d i & exp(s, k, non(a))
Corollary 1.3.6.: It is messt(exp(s, k, a), a) = messt(exp(s, k, non(a)), non(a)).
Theorem 1.3.7.: If s ≠ε then messc(c(s)) = s for all finite lists of data s.
Proof: (Induction over the length of s)
Assume for an arbitrary s messc(c(s)) = s holds.
There are k, k’, k, k’’ such that c(cons(d, s)) = cr k& dt(d, tt)k’ & exp(s, k, ff) & dr k’’
Since c(s) has the form c(s) = cr k& exp(s, k, tt) & dr k’’,
it’s messc(c(s)) = messt(exp(s, k, tt) & dr k’’, tt) = s and
messc(c(d & s)) = messt(dt(d, tt)k’ & exp(s, k, tt) & dr k’’, tt)
= d & messt(exp(s, k, ff) & dr k’’, ff) = d & s.
1.4. Practical experience
We proved the theorem lf(c) → p(c) given in section 1 with Tatzelwurm in three steps:
(1a)lf(c) → S
1∧ ... ∧ S
16
, using the fact that c is the least fixed point
(1b)S
1∧ ... ∧ S
16
→ S
a
∧ ... ∧ S
h
, using the fairness property of the medium
(2)S
a ∧ ... ∧ S
h
→ p(c)
To do these proofs with Tatzelwurm we needed about 25 h to prove S
1, ..., S
16
, 37 h to prove
S a , ..., S
h
and 12 h to prove p. The proof of the five lemmata took 4 h.
What is not included in these times, is the time we spent on planning the proof. It took a very long time (5 months) until we found a way applying the proof arguments of the proofs (1a, b) systematically. The manner of applying these arguments is general so that we hope, that we can reduce the time spending on protocol verification closely to the above times.
1.5. Conclusion
It has been shown that fixed point theory is not only convenient to describe the behaviour of protocols, but it is also possible to find correctness proofs systematically. We saw how well-known arguments as reachability and fairness are applied during the correctness proof.
The systematic application of proof arguments promises soon to reduce verification effort drastically, so that we hope to tackle real world protocols successfully.
Our next subgoal is to implement the described method with our proof programming language.
2. Systematic Verification of in SDL specified Protocols
Abstract
SDL is a language convenient to describe communication protocols. We have to verify them formally, if they are safety critical systems. Formal verification however is a very complex task, which needs to be supported by methods and tools. We present a method how correctness proofs including safety- and liveness properties can be developed systematically. We start from a purely functional description of a communication protocol, which is mechanically derived out of the SDL description. We separate its proof into several parts and show which proof methods are convenient to tackle them. Experience with this method shows that proofs can be developed with an acceptable amount of work.
2.1. Introduction
A SDL system description contains a number of process descriptions, which are in the following called agents. An agent is an extended finite automata, which is built up from states and transitions. A state of an agent consists of one of a finite number of agentstates and of a datastate, a function σ, mapping the agents variables to their values.
There are two possibilities to prove properties of SDL systems. The first possibility is to extend modelcheckers with datastates. A contribution to this task can be found in [Di92]. As alternative we use a theorem prover, which has the advantage that we don’t have to extend it in order to prove system properties expressible in first order logic. The praxis however shows that it is necessary to use a special purpose prover to do verification successfully. A prover which is designed for proofs occurring in program verification is the prover of the Tatzelwurm system [K?u89a,b]. It is a tableau prover [Fit90] extended by reduction procedures treating arithmetic, records and lists, datastructures typically occurring in programs. These extensions are also very helpful for protocol verification problems. However case studies showed that we can make use of the automata structures of the agents in order to define a concept which optimizes the verification process. The introduction of this concept is the objective of this paper.
We suggest to do correctness proofs in two steps. In the first step we calculate the behaviour of the system out of the behaviour of the agents. In the second step we prove the property.
In this paper we show how the first step of the proof can be done systematically. There are reflected typical tasks like reachability analysis and fairness while verifying with the presented method.
The concept bases on the formalism suggested by M. Broy [Bro87, 91], who describes systems of communicating processes with stream processing functions. However the work of Broy lacks an approach to its automatization, which is the contribution of this paper.
Now we want to summarize some characteristic properties and illustrations of the concept.
At first we have to transform the SDL system into a formal system, including a proof theory.
*We transform a SDL process description into a system of conditional rewrite rules.
*We transform the SDL system description into a equation system eq.
*The system behaviour is the solution of eq.
*We formalize the desired property as requirement on the solution of eq.
To calculate the behaviour of the SDL system we have to solve the equation system eq.
*We apply rewrite rules as long as there are some applicable.
*If there are no more rewrite rules applicable, we transform the equation system eq with its solution c to a equation system eq’ with its solution c’ and establish a relation between c and c’. Then we proceed solving eq’.
*The process terminates, if all the derived systems of equations are solved.
The following correspondences illustrate the verification process.
*A transition is simulated in the formal system by the application of a rewrite rule.
* A system state corresponds to a equation system and its solution.
*A relation between the solutions of the equation system corresponds to a system transition.
*All solutions of all systems of equations together with its relations can be seen as reachability graph.
*Additional assumptions about the behaviour of the system, like Fairness lead to a drop of solutions.
The following paper stresses the calculation of solutions of the system of system equations.
The solution is a n-tupel {c
1, ..., c
n
}.
We formulate the system properties by defining predicates which characterize correct solutions.
For example define P to be the predicate, formalizing that c
i and c
j
contain the same sequence
of data. The proof of the validity of P(c
i , c
j
) is a pure predicate logic proof, which can be
done with Tatzelwurm.
2.2. The Description of the behaviour of a SDL system
The following section describes, how a SDL system description is mapped into a formal system. The agents of a SDL system are communicating with each other by sending and receiving messages. The signals, received and sent by the agent are carrying parameters.
We call a (possibly infinite) sequence of messages a stream. We define some operations on streams. The function car takes a stream and returns its first element. The function cdr takes a stream and returns it without its first element. The function & takes either two streams and returns their concatenation or it takes a message and a stream and returns a stream, where the message is added to the input stream. We assume that ε is the empty stream.
We describe the behaviour of the agents by stream processing functions, mapping input streams to output streams.
Fig 2.2.1. shows a typical architecture of a communication protocol. We have two protocol
agents, two medium agents and two user agents. The streams are called c 1, ... , c 8. In 2.2.1.the behaviour of the protocol agents is described by the functions g , h , a user agent is described by a function u , and the medium agents are described by the medium function med .
Fig. 2.2.1. A typical protocol architecture
We define the behaviour of the system to be the solution of the following equation system:c 1 = u (c 2); c 2 = g (c 1, c 4); c 3 = h (c 1, c 4); c 4 = med (c 6);
c 5 = me
d (c 3); c 6 = h (c 7, c 5); c 7 = u (c 8); c 8 = g (c 7, c 5);
If we want to express properties, we do this by defining a predicate which is assumed to evaluate to true , if the property is fulfilled and false if not. For example, we define a predicate P with val (P (c , c ’)) = true iff “c and c ’ contain the same data”, where val is assumed to be an evaluation function of first order formulae.
To prove for example that val (P (c 1, c 8)) = true , we proceed in three steps:
1.We transform the SDL specification into a formal system, including a system of equations and rewrite rules, which are implicit definitions of the functions u , g , h , med .
2.We solve the equation system, using the derived rewrite rules.
3.We prove the required property, using the calculated solution.
In the remaining we describe how we derive a set of rewrite rules out of a SDL process description. If we analyze SDL, we realize that we have four elementary actions.
(1) Agent reads a signal.
(2)Agent evaluates a condition
(3)Agent writes a signal
(4)Agent assigns a value to a variable
In a diploma thesis [Mü93] has been shown that the SDL language constructs can be transformed into a sequence of elementary actions. Assume that the descriptions of the agents only consist of elementary actions. We regard the names of the SDL states as program labels and introduce additional labels g i between elementary actions. The labels are mapped into 2-ary functionsymbols in the formal system. The functions (stream processing functions) take a datastate σ and an input stream i as their arguments and return an output stream. We define that σ[s ] means that σ is evaluated at the place s and that σ[s ← t][s ] = t. The relation
“::=” describes a relation between the functions. A evaluation of a condition is mapped to a conditional rewrite rule, where ? separates the condition from the rewrite rule. The following example shows a SDL state definition and its mapping to a system of rewrite rules.
[b ← tt], i)5
s =
ε
g (σ, i) ::= dt(car(s), tt) & g (σ, i)
5
cr g (σ, i) ::= cr & itc(σ, i) 1
itc(σ, cc & i) ::= g (σ, i)2
σ[s] = ε ? g (σ, i) ::= g (σ, i)23σ[s] ≠ ε ? g (σ, i) ::= g (σ, i)24
dt(car(s), tt)
yes no itc(σ1
dr g (σ, i) ::= dr & itd(σ, i)3Fig. 2.2.2. Transformation of Agent Behaviour
In the next step we simplify the representation omitting the intermediate states, because it is inconvenient to derive such a lot of rewrite rules from the SDL text. We get for every transition path one rewrite rule, if we combine all rules situated on it. The following Fig. 2.2.3. shows the result of the transformation of the SDL fragment to rewrite rules in our formal system.Proceeding in this way we can transform SDL agent descriptions into a system of rewrite rules.The functions describing the behaviour of the system are defined implicitly by the rules, i.e.they are the models of this formal system.
← tt], i)
itc(
Fig. 2.2.3. An agent description and its mapping
to a system of rewrite rules
For further presentation we study a simplified version of the Abracadabra Protocol [Isc21].Fig. 2.2.4. shows the architecture of this version. The protocol description is simplified in two aspects. First we use a simplified user interface. We assume that the user hands over a sequence s of data to the protocol. Second we assume, that we know which of the processes wants to transmit s. We describe the behaviour of the sender with the function con and the behaviour of the receiver with the function lic .
Fig. 2.2.4. A simplified version of the Abracadabra Protocol
We give now an informal description of the behaviour of the Abracadabra Protocol. The two stations communicate transferring Protocol Data Units (PDUs). Communication proceeds in the three sequential phases: Connection , Data Transfer and Disconnection . We assume that the medium is unreliable. An attempt to transmit a message m by a medium may succeed or fail.We model the failure of a transmission attempt by receiving a special message em.
a. Connection Phase
The sender sends a cr , a Connection Request PDU. If it receives cc, a Connection Confirmation PDU, it proceeds to the data transfer phase, if there are some data to transmit. If there are no data to transmit it sends dr, a Disconnect Request PDU and enters the disconnection phase. If it receives em , a cr is sent .
b. Data Phase
The sender sends dt , a Data Transfer PDU. If it receives ak , an acknowledgement PDU it may send a further dt . Each dt and ak bears a control bit, which is assumed to be tt or ff ..Successive dt’s carry alternating values in sequence starting at tt after connection. The correct acknowledgement to a dt contains the control bit of the next dt expected. The reception of an em or the wrong control bit causes a further attempt to transmit dt .
c. Disconnection Phase
The sender sends dr , a Disconnection Request PDU. If it receives a dc , a disconnection confirmation PDU, it considers the disconnection to be complete. If it receives em , it tries another time to transmit dr .
Fig. 2.2.5. shows the behaviour of the agents of the protocol using a finite state machine. Note that this is only an approximation of the behaviour of the protocol, because the datastates are omitted.
Fig. 2.2.5. The components of the Abracadabra Protocol
Sender:Receiver:Medium:
em; em
em; cr cc, ak, em; dr em, dr; dc The rewrite rule representation, given in For. 2.2.1. describes the full behaviour of the protocol, including the datastates. The rewrite rules are constructed in the following way. They are conditioned, where C is assumed to be a quantor free formula, which is evaluated to true or false with respect to the actual datastate σ. f , g are function symbols, m , m ’ are messages and i is a stream.
C (σ) ? f (σ, m & i ) ::= m ’ & g (σ, i )
In some cases the right hand side is just ε. These rules correspond to actions, terminating a process.
pqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq+qüw Definition 2.2.1.: (The behaviour of the sender)w w Connection Phase w w(1)con(i) ::= cr & itc(σ, i)w w(2)itc(σ, em & i) ::= cr & itc(σ, i)w w(3)σ[s] ≠ε ? itc(σ, cc & i) ::= dt(car(σ[s], tt)) & itt(σ[b← tt], i)w w(4)σ[s] = ε ? itc(σ, cc & i) ::= dr & itd(i)w w Data Phase w w(5)cdr(σ[s]) ≠ε ∧ σ[b] = v w w? itt(σ, ak(v) & i) ::= dt(car(cdr(σ[s])), non(v)) w w& itt(σ[(s, b) ← (cdr(σ[s]), non(v))], i)w w(6)cdr(σ[s]) = ε ∧ σ[b] = v? itt(σ, ak(v) & i) ::= dr & itd(i)w w(7)itt(σ, em & i) ::= dt(car(σ[s], σ[b]) & itt(σ, i) w w(8)itt(σ, cc & i) ::= dt(car(σ[s], σ[b]) & itt(σ, i)w w(9)σ[b] = v? itt(σ, ak(non(v)) & i) ::= dt(car(σ[s], σ[b]) & itt(σ, i)w w Disconnection Phase w w(10)itd(dc & i) ::= εw w(11)itd(cc & i) ::= dr & itd(i)w w(12)itd(em & i) ::= dr & itd(i)w w(13)itd(ak(v) & i) ::= dr & itd(i)w w w w Definition 2.2.2.: (The behaviour of the receiver)w w Waiting for a connect request w w(1)lic(cr & i) ::= cc & lib(σ, i)w w(2)lic(em & i) ::= em & lic(i)w w Waiting until the connection is established w w(3)lib(σ, dt(v, tt) & i) ::= ak(tt) & lit(σ[b← ff], i)w w(4)lib(σ, dt(v, ff) & i) ::= cc & lib(σ, i)w w(5)lib(σ, cr & i) ::= cc & lib(σ, i)w w(6)lib(σ, em & i) ::= cc & lib(σ, i)w w(7)lib(σ, dr & i) ::= dc & lid(i)w w Data Transfer Phase w w(8)σ[b] = v’ ? lit(σ, dt(v, v’) & i) ::= ak(v′) & lit(σ[b← non(v’)], i)w w(9)σ[b] ≠v’ ? lit(σ, dt(v, v’) & i) ::= ak(v′) & lit(σ, i)w w(10)lit(σ, em & i) ::= ak(non(σ[b])) & lit(σ, i)w w(11)lit(σ, dr & i) ::= dc & lid(i)w w Waiting for a disconnect confirmation w w(12)lid(em & i) ::= dc & lid(i)w w(13)lid(dr & i) ::= dc & lid(i)w w w w Definition 2.2.3.: (The behaviour of the medium)w w The behaviour of the medium does not depend on a internal datastate, therefore w w we omit this argument. Let m be an arbitrary signal: w w(1)med(m & i) ::= m & med(i)w w(2)med(m & i) ::= em & med(i)w oqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq+q i For. 2.2.1. The Rewrite Rule Representation of the Abracadabra Protocol
第一章：1、软件体系结构的定义 国内普遍看法： 体系结构=构件+连接件+约束 2、软件体系结构涉及哪几种结构： 1、模块结构（Module） 系统如何被构造为一组代码或数据单元的决策 2、构件和连接件结构（Component-And-Connector，C&C） 系统如何被设计为一组具有运行时行为（构件）和交互（连接件）的元素 3、分配结构（Allocation） 展示如何将来自于模块结构或C&C结构的单元映射到非软件结构（硬件、开发组和文件系统） 3、视图视点模型 视点（View point） ISO/IEC 42010:2007 (IEEE-Std-1471-2000)中规定：视点是一个有关单个视图的规格说明。 视图是基于某一视点对整个系统的一种表达。一个视图可由一个或多个架构模型组成 架构模型 架构意义上的图及其文字描述（如软件架构结构图） 视图模型 一个视图是关于整个系统某一方面的表达，一个视图模型则是指一组用来构建 4、软件体系结构核心原模型 1、构件是具有某种功能的可复用的软件结构单元，表示了系统中主要的计算元素和数据存储。 2.连接件(Connector)：表示构件之间的交互并实现构件
之间的连接 特性：1)方向性2)角色3)激发性4)响应特征 第二章 1、软件功能需求、质量属性需求、约束分别对软件架构产生的影响 功能性需求：系统必须实现的功能，以及系统在运行时接收外部激励时所做出的行为或响应。 质量属性需求：这些需求对功能或整个产品的质量描述。 约束：一种零度自由的设计决策，如使用特定的编程语言。 质量原意是指好的程度，与目标吻合的程度，在软件工程领域，目标自然就是需求。 对任何系统而言，能按照功能需求正确执行应是对其最基本的要求。 正确性是指软件按照需求正确执行任务的能力，这无疑是第一重要的软件质量属性。质量属性的优劣程度反映了设计是否成功以及软件系统的整体质量。 系统或软件架构的相关视图的集合，这样一组从不同视角表达系统的视图组合在一起构成对系统比较完整的表达
民航飞机专业术语中英文对照 1、the airframe 机身,结构 2、The front (fore) part 前部 3、The rear (aft) part 后部 4、port 左旋(舵) 5、starboard 右旋(舵) 6、the inboard engine or inboards 内侧发动机 7、the outboard engine or outboards 外侧发动机 8、the nose 机头 9、the belly 腹部 10、the skin 蒙皮 11、the windscreen or windshield 风挡 12、the wing 机翼 13、the trailing edge 机翼后缘 14、the leading edge 机翼前缘 15、the wing tip 翼尖 16、the control surface 操纵面 17、ailerons 副翼 18、flaps (inboard flap,outboard flap,leading edge flaps) 襟翼（内侧襟翼，外侧襟翼，前缘缝翼）
19、spoilers (inboard\outboard spoiler)(spoiler down\up) 阻力板，扰流板（内、外侧扰流板）（扰流板放下、打开） 20、slats 缝翼 21、elevators (elevator control tab) 升降舵（升降舵操纵片） 22、rudder (rudder control tab) 方向舵（方向舵操纵片） 23、flap angle 襟翼角 24、flap setting 襟翼调整 25、the full flap position 全襟翼位置 26、a flapless landing 无襟翼着陆 27、the landing gear 起落架 28、stabilizer 安定面 29、the nose wheel 前轮 30、gear locked 起落架锁定 31、the wheel well 起落架舱 32、the wheel door 起落架舱门 33、a tyre 轮胎 34、to burst 爆破 35、a deflated tyre 放了气的轮胎 36、a flat tyre 走了气的轮胎 37、a puncture 轮胎被扎破 38、to extend the flaps (to retract the flaps) 放下襟翼
XX电器有限公司 编号：产品技术规格书 品名： 产品型号： 产品编码： 编制：审核：批准： 日期：日期：日期： 名称： 地址：
1.基本信息 本承认书规定了进水阀的关键参数，性能要求，检验标准，测试标准，抽样判定规则及生产工艺、包装运输等 1.1产品概述： 本实用新型产品是属于水阀类，是一进一出单阀控制的进水阀，是一种用来控制流体的自动化基础元件，属于执行器；生活中用于控制水的流动或停止，一般会用到这种电磁阀。其工作原理是，电磁阀里有密闭的腔,当线圈通电时，电磁铁芯吸合，卸压孔打开，在进水咀介质的压力推动，打开主阀口，介质流通。当线圈断电时，弹簧复位并推动阀芯和伸缩套封住卸压孔，主阀口关闭，介质截止。这样通过控制电磁阀的电流就控制了机械运动。 1.2产品结构： 结构特点说明，各部件良好配合为关键。
2. 关键参数 1. 零件表面光洁,无缺陷,装配牢固可靠,无松动现象,其 性能应符合GB/T1291-91的要求； 2.额定电压为220V-240V 50/60Hz,额定电流为30±5mA(不通水状态); 3.绝缘等级为F级； 4.适用水压: 0.02-1.0MPa； 5.最大耐水压: 1.6MPa以下,历时10Min无渗漏； 6. 绝缘电阻: 导电部分和外露金属部分,非金属部分之间均大于100MΩ； 7. 匝间绝缘: 对线圈施加1500V,50Hz的脉冲电压,在示 波仪上观察到的是完整的正弦波； 8. 电气强度:绝缘电阻通过后，导电部分和外露 不通电金属和非金属之间施加3125V 50Hz高 压1Min的时间,不应击穿； 9. 流量要求:（根据客户要求）； 10. 绕组温升: <75K； 11. 线圈电阻为4.1±0.3KΩ； 12. 寿命不小于30000次,常温,额定电压下通5S,断5S为一周期，厂家要每周做一次寿命试验： 1)0.02MPa时,5000次； 2)0.3MPa时,20000次； 3) 0.8MPa时,5000次； 13. 噪声,声压级小于55dB(A)； 14.注公差的塑料件按MT5,金属件按IT14级验收； 15. 电磁部分的工作按连续工作考核。 3. 检验标准 3-1 检验依据： 00234015—《零部件图纸》 Q/HR 0501014 《材料通用要求》（现行） Q/HR 0501028 《塑料成型件通用要求》（现行） GB/T 2828.1-2003 《计数抽样检验程序第1部分：按接收质量限（AQL）检索的逐批检验抽样计划》 4.测试标准 依据R-CS-1203002家用电动洗碗机用电磁阀测试。
软件体系结构-期末大题
————————————————————————————————作者：————————————————————————————————日期: ?
1．基于构件的软件开发的优势是什么? 基于构件的软件将软件开发的重点从程序编写转移到了基于已有构件的组装,更快地构造系统，减轻用来支持和升级大型系统所需要的维护负担，从而降低了软件开发的费用2.尝试用自己的语言介绍Ｋruｃhteｎ的“4+１”模型。 Ｋrｕcｈten 提出了一个"4+1"视图模型，从５个不同的视角包括包括逻辑试图、进程视图、物理视图、开发视图、场景视图来描述软件体系结构。每一个视图只关心系统的一个侧面,5个试图结合在一起才能反映系统的软件体系结构的全部内容。
3.在希赛公司的一个财务管理系统,财务部要客户提供………… 4.不同的体系结构风格具有各自的特点、优劣和用途。试对管道－过滤器风格、事件驱动风格、分层系统、C2风格和基于消息总线的风格进行分析比较。P52-56 （1)管道和过滤器 特点: @使得软构件具有良好的隐蔽性和高内聚、低耦合的特点； @允许设计者将整个系统的输入输出行为看成是多个过滤器的行为的简单合成；
@支持软件重用。只要提供适合在两个过滤器之间传送的数据，任何两个过滤器都可被连接起来； ＠系统维护和增强系统性能简单。新的过滤器可以添加到现有系统中来；旧的可以被改进的过滤器替换掉; @允许对一些如吞吐量、死锁等属性的分析; @支持并行执行。每个过滤器是作为一个单独的任务完成，因此可与其它任务并行执行?缺点:①通常导致进程成为批处理的结构。 ②不适合处理交互的应用。 ③因为在数据传输上没有通用的标准,每个过滤器都增加了解析和合成数据的工作，这样就导致了系统性能下降,并增加了编写过滤器的复杂性。 (2)
above-the-line advertising 线上广告 广告代理商能从媒介获得佣金（代理费）的广告，如报刊广告、广播广告、电视广告、影院广告、户外广告等。 account executive (AE) 客户经理 广告公司的业务人员职称。客户经理往往须负责下列工作：1，与客户及内部其他部门共同计划广告（planning）,向各部门传达客户的诉求；2，内部协调（coordination）；3，将广告设计稿提供给客户；4，监督执行政府的有关广告规章和法规（regulatory matters）；5，利润管理（agency profit management）。客户经理通过计划和协调公司的服务部门，为客户提供更好的服务。 account service 客户服务 客户服务是广告代理商的中心工作，肩负着使客户满意从而建立起长期的合作关系，及推动广告代理商内部工作有效运转的任务。它是广告代理商直接同客户进行沟通、交流的一种功能。 advertising agency 广告代理商 习惯上称为“广告公司”，即《中华人民共和国广告法》中所称的广告经营者，一般设 有许多职能和业务部门。 advertising campaign 广告活动 有时称为“运动”或“战役”。广告活动包括以下四个重点：制作适当的销售信息、及 时传达给受众、选择适当的时机，用合理的成本。广告主制定一项能测定的目标后，为 达到这一目标制定广告战略，然后在市场上执行，包括：广告计划、广告制作、销售及 营销等。 advertising department 广告部 分为企业的广告部和媒介的广告部。企业的广告经理负责拟定、审核及实施企业的广告 计划。一般也是负责有关广告的具体工作。媒介的广告部经理负责出售报刊等的版面， 广播、电视的时间等。 airport advertising 机场广告 利用机场的候机室及在机场内其他各种场地和设备上制作刊出的广告，也包括在指示牌 上制作的广告。 Appeal 诉求 广告通过媒介向目标受众诉说，以求达到所期望的反应。诉求是制定某种道德、动机、 认同，或是说服受众应该去做某件事的理由。诉求分三类：理性的、感性的和道义的。 诉求所用语句应具有强烈的感染力。 area sampling 区域抽样 群体抽样的一种形式。样本空间按区域进行划分，选定某抽样区域，如一个县、一个行 政区、一个街区，从中确定调查对象。 Audience 受众 接受广告的公众，也就是广告的对象。通过任何广告媒介接触的观众或听众，都有数量 、特征方面的不同需要考虑到。这些不同可使广告做到有的放矢。
A air superiority 制空权 ambush 伏击 assistance 援助、协助 attitude 飞行姿态（高度） AW ACS(Airborne Warning and Control System) link 空中预警引导 aye-aye, sir 遵命，长官（同affirmative）AB 加力 ACM 空战机动 ACT 空战战术 AI 空中拦截 Angles 用千英尺表示高度的快捷方式，例如，“Angles 20”表示高度20,000英尺。Angle-off 敌机航向和你的航向之间的角度差，也称为航向交叉角或HCA Armour star hands 肥厚,笨拙的手，驾驶飞机时容易出错 Aspect angle 你的飞机相对于敌机尾部的角度 Attack geometry 进攻战机的追击路径 B bail out （爬出座舱）跳伞 bearing 航向 航向的划分方法是：以飞行员自己的飞机为圆心的一个与地平面平行的虚拟圆，分为360度，正北方为零度，正东方为90度，正南方为180度，正西方为270度，依此类推。black out 由于指向头部方向的加速度过大而导致的大脑缺血，引起的暂时性失明和意识丧失。 bogie 原指妖怪或可怕的人，空战中指敌机。bandit 原指强盗，空战中指敌机（同bad guy） bombing run 炸弹攻击 brake 阻力板（降落时塔台呼叫call the ball 就是指放下阻力板） bug out 撤出战区 bull's eye 原指圆形箭靶的中心，空战中的意思是“正中！”，类似的短语还有：direct hit, great balls of fun, splash one, one down等。bingo 原指一种赌博游戏或烈酒，空战中指出乎意料地打中了敌机。 只够返回基地的燃料，其它已耗尽的状态。Bar 雷达波的一次扫描 Basic Fighter Maneuvers（BFM）在一对一空战环境中的基本空战机动 Belly check 执行180度的翻滚，检查机身下方空间 Boresight mode 雷达束固定指向机首前方，第一个进入雷达束区域的目标将被自动锁定 Butterfly setup 一个战斗训练进入计划，两架战机开始以一字并列编队飞行，然后互相转离45度。在距离4英里之后，两架战机互相返回进入迎面相遇。 BVR 超视距 C chaff 原指谷壳和糠，空战中指金属箔条，用以干扰敌方防空雷达或雷达制导导弹。也指仅燃料够返回基地，其它已耗尽的状态。 chopper 直升机 cockpit 飞机座舱 collide 碰撞 Cold 雷达停止工作，“冷机鼻”commence 着手开始做 contact 原意为接触，空战中指发现敌人，一般分为radar contact（雷达发现）和visual contact（目视发现）两种。 control tower （机场）指挥塔 convoy 原指护送、护航，用于军事方面时多指运输车队或运输舰队。 copy 收到，确认 Corner velocity 飞机具有最快的转弯速率和最小转弯半径时的速度 Crawl back up in the cockpit 有时，飞行员会遇到一种称为“任务饱和”的现象，即瞬间发生了太多的事情，而飞行员的能力无法处理应付如此之多的事情，导致他发生智力上的退化。 CMD自动驾驶的command方式 Clean 战机未被雷达探测到
CMMI标准名词术语 1 AT Assessment Team 评审小组 2 ATM Assessment Team Member 评审小组成员 3 BA Baseline Assessment 基线评审 4 CAR Causal Analysis and Resolution 原因分析与决策 5 CBA CMM-Based Appraisal 基于CMM的评价 6 CBA-IPI CMM-Based Appraisal for Internal Process Improvement 为内部过程改进而进行的基于CMM的评价（通常 称为CMM评审） 7 CC Configuration Controller 配置管理员 8 CF Common Feature 公共特性 9 CFPS Certified Function Point Specialist 注册功能点专家 10 CI Configuration Item 配置项 11 CM Configuration Management 配置管理 12 CMM Capability Maturity Model 能力成熟度模型 13 CMMI Capability Maturity Model Integration 能力成熟度集成模型 14 COTS Commerce off the shelf 商业现货供应 15 DAR Decision Analysis and Resolution 决策分析与制定 16 DBD Database Design 数据库设计 17 DD Detailed Design 详细设计 18 DP Data Provider 数据提供者 19 DR Derived Requirement 派生需求 20 EPG Engineering Process Group 工程过程小组 21 FP Function Point 功能点 22 FPA Function Point Analysis 功能点分析 23 FR Functional Requirement 功能性需求 24 GA Gap Analysis 差距分析 25 ID Interface Design 接口设计 26 IFPUG International Function Point Users Group 国际功能点用户组织 27 IPM Integrated Project Management 集成项目管理 28 IR Interface Requirement 接口需求 29 KPA Key Process Area 关键过程域 30 KR Key Requirements 关键需求 31 LA Lead Assessor 主任评审员 32 MA Measurement and Analysis 测量与分析 33 MAT Metrics Advisory Team 度量咨询组 34 MCA Metrics Coordinator and Analyst 度量专员 35 ML matreraty library 度量数据库 36 NFR Non-functional Requirement 非功能性需求 37 OC Operational Concept 操作概念 38 OID Organizational Innovation and Deployment 组织革新与部署
钢模板技术规格书 一、钢模板组成基本规定 1、钢模板由面板系统、支撑系统、操作平台系统及连接件等组成。 2、组成模板各系统之间的连接必须安全可靠。 3、钢模板的支撑系统应能保持钢模板竖向放置的安全可靠和风荷载作用下的自身稳定性。 4、钢模板应能满足现浇混凝土体成型和表面质量效果的要求。 5、钢模板结构构造应简单、重量轻、坚固耐用、便于加工制作。 6、钢模板应具有足够的承载力、刚度和稳定性，应能整装整拆，组装便利，在正常维护下应能重复周转使用。 二、钢模板的设计要求 1、钢模板应根据工程结构形式、荷载大小、质量要求及施工设备和材料等结合施工工艺进行设计。 2、钢模板中的钢结构设计应符合现行国家标准GB50017?钢结构设计规范?。大模板、滑升模板等设计还应符合现行国家标准GB50113?滑动模板工程技术规范?的相应规定。 3、钢模板设计时板块规格尺寸宜标准化。 4、钢模板各组成部分应根据功能要求采用极限状态设计方法进行设计计算。 5、钢模板设计时应考虑运输、堆放和装拆过程中对模板变形的影响。
6、钢模板设计时应考虑组装方便便捷，连接处采用定位销孔。 7、钢模板设计最终应考达到的要求有：签字齐全的设计图纸、工装图、排料图、工艺图、技术标准、作业指导书等技术文件，必要时。应有刚度、强度、稳定性的核算。 8、在材料选用上，为保证模板结构的承载能力，防止在一定条件下出现脆性破坏，应根据模板体系的重要性、荷载特征、连接方法等不同情况，选用合适的钢材型号和材性，且宜采用Q235钢和Q345钢。 9、模板的钢材质量应符合相应的国家标准规定： 10、具体要求： ①钢模板的面板应选用厚度不小于5mm的钢板制作，材质不低于Q235A的性能要求。 ②钢模板的法兰采用钢板或角钢，横筋、竖筋采用型钢或钢板制作，材质宜与钢面板材质同一牌号，以保证焊接性能和结构性能。 ③钢模板的背杠及桁架采用型钢制作，材质不低于Q235A的性能要求。 ④钢模板的吊环应采用Q235A材料制作并应具有足够的安全储备，严禁使用冷加工钢筋。 ⑤钢模板对拉螺栓材质硬不低于Q235A的钢材制作，应有足够的强度承受施工载荷。
考试题型 一、填空（每题1分，共10分） 二、名词解释（每题2分，共20分） 1、B/S 2、C/S 3、HMB 4、DSSA 5、ADL 6、XML 7、ATAM 8、Web Service 9、MTTF10、SOAP 11、WSDL 12、UDDI 13、SAAM 14、MVC 15、Artifact-Driven 16、Use-Case-Driven 17、Domain-Driven 18、Pattern-Driven 19、构件20、连接件21.、MTBF 22、敏感点23、权衡点24、直接场景25、间接场景26、质量属性效用树27、XML Schema 三、问答题（40分） 1、构件描述模型有哪几种？ 2、理解并比较构件分类的三种方法：关键字分类法、刻面分类法和超文本组织方法， 它们是如何组织的？如何在其中检索构件？每种方法各有什么优缺点？ 3、了解软件体系结构的四个发展阶段。 4、根据软件体系结构的定义，你认为软件体系结构的模型应该由哪些部分组成？ 5、至少掌握三种经典软件体系结构风格。 6、试分析和比较B/S，二层C/S和三层C/S，指出各自的优点和缺点。 7、请对MVC风格体系结构进行介绍，并说明该风格的优缺点。 8、在正交软件体系结构中，什么是完全正交结构？在实际使用时是不是必须严格遵 守结构正交？使用正交软件体系结构有什么优点？ 9、层次系统结构和基于消息的层次系统结构有什么区别？ 10、体系结构描述语言与程序设计语言有什么区别？ 11、ACME中定义了哪七种体系结构实体？ACME中的表述和表述映射，类型和风格是什么含义？
12、了解基于XML的软件体系结构描述语言。 13、简要介绍Krutchten的“4+1”视图模型。 14、设计模式的基本成分有哪几个？请简单介绍其各个基本成分。 15、为什么要评估软件体系结构？从哪些方面评估软件体系结构？ 16、软件体系结构评估的主要方法有哪三种？请简单解释每种方法。 17、SAAM和ATAM评估方法的基本步骤分别是什么？ 18、Web服务有哪些核心技术，这些技术是如何在Web服务中发挥作用的。 四、看图答题（30分） 1、请根据P38图3-5介绍黑板系统的组成。 2、请根据P59图3-26解释HMB风格的构件模型。 3、请根据P60图3-27解释消息总线的属性和服务。 4、请根据P147图5-2介绍体系结构设计方法的元模型。 5、请根据P167图6-1简要介绍基于体系结构的软件开发过程的各个步骤。并说明各个步骤的必要性何在？或者说，它们在软件生命周期中都起到了什么作用？ 6、请根据P207图8-1分析服务提供者、服务请求者和服务注册中心三者的作用，以及它们之间的工作流程。 7、请根据P229图8-11介绍UDDI的具体工作步骤。
以下属于涉及面很广, 有广告领域的, 有数字设计领域的, 更有IT领域的, 因为本身数字互动营销就是个很多元很不清不楚的东东~ 我承认这很无聊, 不过事实的确是这样的, 很多概念我们圈内人士自己都搞不清楚! 那该如何沟通, 如何清楚的向客户去表述呢? 比如数字营销, 互动营销, 网络营销, 这三个概念, 能一下说明白的大概也该去中科院了. 又比如线上, 线下这个“线”能定义清楚的…废话不多(不断更新中…)——————————————————————— Advertorial (软文) 广告的一种, 即付费文章, 故意设计成像一篇普通的文章。 Appeals (述求) Emotional Appeals/感性诉求, Rational Appeals/理性诉求 Art Base(美术/设计出身) 刚入行不久的同学也许会经常被人问到:“你是Art Base 还是Copy Base?” 一开始都是被问的一头雾水! 在广告圈中创意人分出身有两个派系——Copy Base和Art Base. Copy Base指出身于文案, 文字达人(Copywriter); Art Base就是指出身于美术, 设计, 视觉达人! 比如你是某公司CD, 你在向别人介绍时可以这么用:“我是xxx公司CD, 我是Art Base!”ATL (线上) 还有BTL呢! 这个讲起来真是有的讲, 相信平时大家都会被线上线下的概念混淆的团团转…有时间要写一篇关于这两个概念的日记. 互相探讨下! 其实在无数传统广告的书籍上都有讲这两个概念的. 但是这条线究竟是啥呢? ATL即Above The Line; BTL即Below The Line. ATL可以泛指为广告; BTL则是其他销货
中医名词术语标准参考 舌诊 舌诊：tongue diagnosis 望舌：inspection of tongue 舌象：tongue manifestation 舌尖：tip of the tongue 舌边：margins of the tongue 舌中；舌心：center of the tongue 舌根；舌本：root of the tongue 舌体；舌质：tongue body 舌色：tongue color 荣枯老嫩：luxuriant/ flourishing, withered, tough and tender 淡白舌：whitish tongue 淡红舌：reddish tongue 红舌：red tongue 青舌：blue tongue 紫舌：purple tongue 青紫色：bluish purple tongue 绛舌：crimson tongue 胖大舌：enlarged tongue 肿胀舌：wollen tongue 瘦薄舌：thin tongue 点刺舌：spotted tongue 芒刺舌：prickly tongue 齿痕舌：teeth-marked tongue 裂纹舌：fissured tongue 光剥舌：peeled tongue 镜面舌：mirror tongue 地图舌：geographical tongue 舌衄：spontaneous bleeding of the tongue 强硬舌：stiff tongue 萎软舌：limp wilting tongue 颤动舌：trembling tongue 歪斜舌：deviated tongue 短缩舌：contracted tongue 吐弄舌：protruded agitated tongue 舌卷：curled tongue 苔色：coating color 苔质：texture of coating 白苔：white coating 白砂苔：white sandy coating
XX事业部XX项目 XX设备采购 技术规格书 编制： 审核： 审批： 编制时间：
目录 1、总则 2、设计条件 3、产品标准 4、供货范围 5、技术要求 6、质量性能保证 7、包装运输 8、检验验收 9、技术服务 10、技术资料 11、其他
1、总则 1.1 本技术规格书针对公司XX事业部XX项目XX装置（设备）的采购，提出了相关产品的功能设计制造、供货范围、质量保证、检验验收、包装运输、技术资料及服务等方面的基本要求。 1.2 本技术规格书提出的为最低限度的技术要求，并未对一切技术细节做出规定，也未充分引述有关标准和规范的条文，卖方应提供符合本技术规格书和现行工业标准的成熟、可靠、全新的产品及服务。 1.3卖方对所提供的设备、附件和附属设备的制造质量、供货、技术规格、文件图纸资料、技术服务、工程服务、包装运输、开箱检验、安装指导、现场测试、设备运行等各个环节负有完全责任。卖方对其技术文件的所有内容负完全责任，买方在技术文件上的签字并不意味对卖方责任的解脱。 1.4卖方提供的产品及配套产品必须在中国境内有技术服务和维护能力的服务网点。 1.5本技术规格书未明确事宜，卖方应在设计过程中充分尊重买方意见，在现有国内技术水平能够达到情况下，不得以任何理由拒绝。 1.6本技术规格书中标注“*”和“△”的为重要技术条款，其中标注“*”的为否决条款，标注“△”的视偏离程度进行评分或否决。卖方对重要技术条款必须逐条响应，并给出相关技术指标；如有与
本技术规格书描述的要求不一致但能满足要求的，应论述其理由。未明确响应的一律视为偏离。 2、设计条件 2.1 工程概况 2.2 气候水文资料 2.3 公用工程及现场条件 2.4 关键指标 3、产品标准 4、供货范围 4.1 主要设备清单 4.2 备件清单 4.3 工作范围及界面划分 5、技术要求 5.1 通用要求 5.1.1 使用寿命。设备设计寿命10（20、30）年，正产使用条件下连续运行不少于25000小时。 5.1.2 5.2 设备要求 5.3 电气仪表要求 5.4 防腐及其他要求
壹 . 名词解释(参考斯佳分享的名词解释文档) 1.ADL(Architecture Description Language) 体系结构描述语言 2. SOA(Service-Oriented Architecture) 面向服务架构 3. DSSA (Domain Specific Software Architecture) 特定领域软件体系结构 4.CORBA(Common Object Request Broker Architecture) 公共对象请求代理体系结构 5. UML(Unified Modeling Language) 统一建模语言 6.XML(Extensible Markup Language ) 可扩展标记语言 7.B/S(Browser/Server) 浏览器/服务器C/S(Client/Server) 客户端/服务器 8.HMB(Hierarchical [?ha??'rɑ:k?kl] message bus) 层次消息总线 9.SA (Software Architecture) 软件体系结构 10.OMG(Object Management Group) 对象管理组织 11.SOAP(Simple Object Access Protocol) 简单对象访问协议 12.WSDL(Web Services Description Language) web服务描述语言 13.SOAD(Service Oriented Analysis And Design) 面向服务的分析与设计 14.DCOM(Distributed Component Object Model) 分布式对象组件模型 https://www.doczj.com/doc/e72477749.html, (Module Interconnection Language) 模块内连接语言 贰 . 判断题 1、软件重用是指重复使用已有的软件产品用于开发新的软件系统，以达到提高软件系统的开发质量与效率，降低开发成本的目的。答案：√ 依据页码：P4 2、软件体系结构充当一个理解系统构件和它们之间关系的框架，特别是那些始终跨越时间和实现的属性。 答案：√ 依据页码：P28 5、构件可以由其他复合构建和原子构件通过连接而成。（） 答案：√ 依据页码：P37 6、体系的核心模型由5种元素组成：构件、连接体、配置、端口和角色（） 答案：√ 依据页码：P37 7、软件体系结构的核心由5种元素组成：构件、连接件、配置端口和角色。其中，构件、连接件和配置是最基本的元素（） 答案：√ 依据页码：P37 8、开发视图主要支持系统的功能需求，即系统提供给最终用户的服务（） 答案：X 依据页码：P32、33 9、构件、连接件以及配置是体系结构的核心模型最基本的元素（） 答案：√ 根据页码：P37
广告专业英语 英翻中 A AAAA America Association of Advertising advocacy advertising 倡导型广告Account Executive 客户主管 Account planning 客户策划 Account Services 客户部 Advertising Department 企业广告部agency 广告代理商 Art Director 美术指导 Assistant Partner 董事助理 A priori 先验估汁(演绎法) A posteriori 实测值(归纳法) analysis 分析archetype 标准受众，原型availability 空余时段 audience duplication 重复受众 AA（Account Assistant）客户助理Action Plan 行动方案 AD（Account Director）客户总监 Add Value 附加价值 Advertorial付费软文 AM（Account Manager）客户经理Analysis Tools分析工具Announcement 公告 Annual Report年报 AP (Asia-Pacific) 亚太区 AR List 任务清单 ATL (Above the Line) 线上活动Attachment附件 Audience Awareness公众认知度Awareness 认知 ad planning 广告策划 appeal 诉求B bid [bid] 广告竞标 business-to-business（B2B）advertising brand image 品牌印象 Brainstorming 头脑风暴法 Billboard 广告路牌 Blow in card 报刊广告插页 Bulldog edition 报纸的早发版 best face forward 展现最佳面貌 brand manager 品牌经理 buried position 被淹没的广告位Background material 背景材料Benchmark测试基准 BI (Behavior Identity)企业行为识别系统Bidding 竞标 Bio个人简历（Viva Resume）Boilerplate公司简介（附在新闻稿后面的关于该公司的简短介绍） Brand Loyalty品牌忠诚度 Brand Management品牌管理 Brand Planning/Designing品牌策划/设计Brand Positioning Survey品牌定位调查Brand Promotion品牌推广 Branding Strategy品牌战略 Briefing Kit资料包 Briefing情况介绍 BTL (Below the Line) 线下活动 Bundle 附赠品 Business Model商业计划 Business Philosophy 经营哲学 Business Strategy 经营战略 brand development index 品牌成长指数back- to-back 广告连播 C capitalism 资本本主义，资本运营commercial advertising 商业广告communication process 传播过程comparative advertising 比较广告consumer advertising 消费品广告consumerism 消费主义 Chief Executive Officer(CEO) 首席执行长官
工程专业术语中英文对照
CDB工程专业术语中英文对照(二） 添加时间：2013-4-24 节流截止放空阀 2011-08-10 16:50:46| 分类：English | 标签：|字号大中小订阅 六、仪表及自动控制 通用描述 COMMON DESCRIPTION 设备名称Equipment Name 缩写 ABB. 分散控制系统Distributed Control System DCS 安全仪表系统Safety Instrumentation System SIS 紧急切断系统Emergency Shutdown system ESD 火气系统Fire and Gas system F&G 监视控制和数据采集系统 Supervisory Control and Data Acquisition SCADA 可编程逻辑控制器Programmed Logic Controller PLC 远程终端单元Remote Terminal Unit RTU 站控系统Station Control System SCS 中央控制室Central Control Room CCR 操作间Operation room 机柜间Equipment room/ Cabinet room 大屏显示系统Large Screen Display system LSD 流量类仪表 FLOW INSTRUMENT 设备名称Equipment Name 孔板Orifice Plate 文丘里流量计Venturi Flowmeter 均速管流量计Averaging Pitot Tube 阀式孔板节流装置 Orifice Plate in quick change fitting 涡轮流量计Turbine Flowmeter
新疆天龙矿业股份有限公司综合利用工业废渣4000t/d新型干法水泥生产线项目 回转窑规范书 招标单位：新疆天龙矿业股份有限公司设计单位：南京水泥工业设计研究院
2011年3月 第一部分技术规范 1.1 总则 1.1.1 本技术规范书适用于新疆天龙矿业股份有限公司综合利用工 业废4000t/d新型干法水泥生产线项目的回转窑。本规范书包 括回转窑本体及附属设备的功能、结构、性能、安装和实验设 计等方面的技术要求。 1.1.2 本技术部分并未对一切技术细节做出规定，投标方应提供符合 本技术部分的技术条件和满足招标方使用要求的优质产品。1.1.3 本技术部分所用的标准如与投标方所执行的标准不一致时， 按较高标准执行。 1.2 工程概况 1.2.1 项目名称 新疆天龙矿业股份有限公司水泥技改扩建项目综合利用工业废渣4000t/d熟料新型干法水泥生产线。 1.2.2 建设地点 新疆阜康市甘河子镇新疆天龙矿业股份有限公司水泥公司东侧空地。 1.2.3 建设规模、范围及产品方案 采用新型干法预分解生产工艺，建设一条带9000kW纯低温余 热发电的4000t/d熟料水泥生产线，年产熟料124.00万t；年 产水泥170万t，其中PO42.5普通硅酸盐水泥119.00万t、
PC32.5复合硅酸盐水泥51.00万t；年发电量为5112×104kWh，年供电量为4703×104kWh。 建设范围自原料进厂至水泥成品出厂(包括煤粉制备及输送)以及与之相配套的生产辅助设施；9000kW纯低温余热发电系统。 1.3 自然条件 厂区所在地属中温带大陆性干旱半干旱气候。 年平均气温：6.3℃； 年平均降水量：176mm； 蒸发量：2141mm； 无霜期平均：156天； 年日照时数：2280～3230小时。 据阜康市气象站有关气象资料查明，该场区主要气象特征参数(1963年-2009年)如下： 多年平均最高气温在7～8月 最热月平均气温：25.8 oC； 极端最高气温达：41.5 oC(1973年)； 多年平均最低气温在12～1月 最冷月平均气温：-19.4oC； 极端最低气温达：-37oC(1976年)； 多年平均气温：7.0oC左右； 每年10月中下旬开始降雪，10月下旬至翌年3月下旬为冻结期，历年最大积雪厚度：33cm(2000年2月)； 最大冻土深度：202cm(1969年3月)； 多年年平均降水量：220.3mm； 年最大降水量：388.6mm； 年最小降水量：106.1mm；
广告业常用术语名词解释 创意总监 (简称CD) 主要任务是创意管理,即控制公司的创意品质. 艺术指导 (简称AD) 通常与文案人员结成创意小组,共同发想创意概念,并具体负责创意视觉化工作. 文案人员 (简称CW) 与艺术指导共同发想创意概念,并具体负责文案写作工作. 业务员 (简称AE) 汇集客户市场,产品的基本资料,得出对市场,产品,消费者的分析. AAD〔Associated Account Director〕——副客户总监 AAD〔Associated Art Director〕——副美术指导 ACD〔Associated Creative Director〕——副创作总监 AD 〔Account Director〕—客户服务总监、业务指导 AD〔Art Director〕——美术指导（在创作部可以独挡一面执行美术指导工作的美术监督） AE〔Account Executive〕——客户执行、客户服务、客户主任；预算执行者，负责广告代理商和广告主之间的一切有关业务，观念，预算，广告表现之联系 AM 〔Account Manager〕——客户经理 AP〔Account Planner〕——客户企划（分策略企划和业务企划）两种〔Artist〕——正稿员 ASM〔Area Sale Manager〕——大区销售经理 CD〔Creative Director〕——创作总监、创意总监、创意指导（CD的前身，不是撰稿人便是美术设计，因为积累了丰富的经验，并有优异的创作成绩而成为督导） 〔Copy Director〕——文案指导 CGH〔Creative Group Head 〕——创意组长 〔Computer Visualizer〕——计算机绘图员 CW〔Copywriter〕——撰稿人 DCS〔Director of Client Service〕——客户主管 ECD〔Executive Creative Director〕——执行创意总监 FA〔Finish Artist〕——完稿、画师 〔Finish Artist Group Head〕——完稿组长 GAD〔Group Account Director〕——客户群总监 GCD〔Group Creative Director〕——创意群总监
技术规格书编制规定 1总则 1.1本规范书适用于＿＿＿＿＿设备，提出了设备的功能设计、结构、性能、安装和试验等方面的技术要求。 1.2买方在本规格书中提出了最低限度的技术要求，并未规定所有的技术要求和适用的标准，卖方应提供一套满足本规范书和所列标准要求的高质量产品及其相应服务。对国家有关安全、环保等强制性标准，必须满足其要求（如锅炉与压力容器、高电压设备等）。 1.3如未对本规范书提出偏差，将认为卖方提供的设备符合规范书和标准的要求。偏差（无论多少）都必须清楚地表示在投标文件中的附件“差异表”中。 1.4卖方须执行本规格书所列标准。有矛盾时，按较高标准执行。 1.5合同签订后个月，按本规范书要求，卖方提供合同设备的设计、制适、检验／试验、装配、安装、调试、试运、验收、试验、运行和维护等标准清单给买方，买方确认。 2 范围 1.1 拟采购的设备清单 序号 位 号 设备名称 数 量 开/ 备 备 注
1.2卖方应仔细阅读本说明书和数据表中的技术要求和工艺参数，并将其作为准备和完成报价的依据。 3工程概况 3.1概述 （本节说明地理位置、工程规模、分期建设情况、工程现状等） 3.2本期工程简介 （视设备情况对下列内容进行取舍） 3.2.1燃料供应及其运输 3.2.2水源 3.2.3储灰场 3.2.4厂／场区总布置及交通运输 4设计和运行条件 4.1系统概况和相关设备 （填写本设备所在的系统以及与之相应系统的简况，和相关设备的情况）4.2工程主要原始资料 4.2.1气象特征与环境条件 4.2.2厂／场区地质 4.2.3厂/场区地震 4.2.4燃煤
4.2.5灰渣特性 4.1.6燃油 4.1.7水质 4.3安装运行条件 5技术条件 （根据具体设备的填写） 5.1参数、容量/能力 5.2性能要求 启停、运行、寿命、变负荷等内容 5.3结构要求／系统配置要求 5.4配供的辅助设备要求 5.5仪表和控制要求（l＆C） 5.6标准 5.7性能保证值 5.8安装调试要求 5.9 设备数据表 6监造（检验）和性能验收试验 见监造（检验）和性能验收试验 7设计与供货界限及接口规则 8清洁、油漆、包装、装卸、运输与储存