A hybrid SAT-based decision procedure for separation logic with uninterpreted functions
A Hybrid SAT-Based Decision Procedure for Separation
Logic with Uninterpreted Functions?
Sanjit A.Seshia sanjit.seshia@https://www.sodocs.net/doc/6d3290449.html,
Shuvendu https://www.sodocs.net/doc/6d3290449.html,hiri
shuvendu@https://www.sodocs.net/doc/6d3290449.html,
Randal E.Bryant
randy.bryant@https://www.sodocs.net/doc/6d3290449.html,
School of Computer Science&Department of Electrical and Computer Engineering Carnegie Mellon University,Pittsburgh,P A15213
ABSTRACT
SAT-based decision procedures for quanti?er-free fragments of?rst-order logic have proved to be useful in formal veri?cation.These decision procedures are either based on encoding atomic subfor-mulas with Boolean variables,or by encoding integer variables as bit-vectors.Based on evaluating these two encoding methods on a diverse set of hardware and software benchmarks,we conclude that neither method is robust to variations in formula characteris-tics.We therefore propose a new hybrid technique that combines the two methods.We give experimental results showing that the hy-brid method can signi?cantly outperform either approach as well as other decision procedures.
Categories and Subject Descriptors
I.1[Symbolic and Algebraic Manipulation]:Expressions and Their Representation,Algorithms;I.2.3[Deduction and Theorem Proving];F.4.1[Mathematical Logic]:Mechanical theorem prov-ing
General Terms
Algorithms,Experimentation,Measurement,Veri?cation
Keywords
Design veri?cation,Decision procedures,Boolean satis?ability,The-orem proving.
1.INTRODUCTION
Quanti?er-free fragments of?rst-order logic and decision proce-dures for them have become commonplace in many formal veri?-cation efforts.Decision procedures for the Logic of Equality with Uninterpreted Functions(EUF)have been successfully used in the automated veri?cation of pipelined processor designs[8,4].Pred-icate abstraction methods[9]based on decision procedures have ?This work was supported by ARO grant DAAD19-01-1-0485and SRC contract1029.001
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for pro?t or commercial advantage and that copies bear this notice and the full citation on the?rst page.To copy otherwise,to republish,to post on servers or to redistribute to lists,requires prior speci?c permission and/or a fee.
DAC2003,June2–6,2003,Anaheim,California,USA.
Copyright2003ACM1-58113-688-9/03/0001...$5.00.been used to verify parameterized cache coherence protocols.The logic of Counter Arithmetic with Lambda Expressions and Unin-terpreted Functions[6](CLU),which generalizes EUF,is the basis for the UCLID veri?er which has been used for bounded model checking and inductive invariant checking of out-of-order micro-processors with unbounded resources[11].Decision procedures are an integral part of software veri?cation systems including the Code Validation tool[13]and the Blast veri?er[10].Hence the importance of having ef?cient decision procedures can hardly be overstated.
Many decision procedures leverage off the recent advances in Boolean satis?ability(SAT)solvers.These decision procedures differ in the Boolean encoding and the degree of the coupling with the SAT solver.One can classify these procedures as being either eager or lazy.In the eager approaches[4,6,12,14],the quanti?er-free?rst-order formula is converted in a single step to an equiva-lent Boolean formula which is checked using the SAT solver.The lazy approaches(e.g.,[3,1])iteratively re?ne the Boolean encod-ing based on satisfying assignments from the SAT solver that are inconsistent with the?rst order theory.The process is repeated until a consistent assignment is found or all assignments are explored. We consider the problem of deciding formulas in the logic of Sep-aration Predicates and Uninterpreted Functions(SUF),which can express properties of systems modeled in CLU logic.For deci-sion procedures using the eager approach,two Boolean encoding methods have been proposed:small-domain encoding(also called ?nite instantiation)[6],and per-constraint encoding[14].In small-domain encoding,each integer variable is interpreted over a?nite set of values that is determined by analyzing the formula.On the other hand,in per-constraint encoding,each atomic subformula is encoded as a Boolean variable.Constraints are then added to prune off the inconsistent assignments of the Boolean variables.
In this paper,we con?rm results of our previous experimental eval-uation[5]of these two encoding methods,concluding that neither of the approaches are robust to variations in formula characteris-tics.Hence,we propose a new hybrid method that combines the two methods,and show that it can be more robust than either ap-proach.Finally,we report empirical results comparing our hybrid method with other decision procedures for SUF logic.
2.BACKGROUND
Figure1summarizes the expression syntax for SUF logic.Expres-sions can be of two types:integer or Boolean.Boolean expressions are formed by combining equalities,inequalities,or applications of uninterpreted predicates using Boolean connectives.Integer ex-pressions are formed by applying an uninterpreted function to a list of integer expressions,by applying the unary arithmetic functions
27.1
succ(“+1”)and pred(“?1”),or by applying the ITE(“if-then-else”)operator.We will omit parentheses for function and pred-bool-expr::=true|false|?bool-expr|(bool-expr∧bool-expr)
|(int-expr=int-expr)|(int-expr |predicate-symbol(int-expr,...,int-expr) int-expr::=ITE(bool-expr,int-expr,int-expr) |succ(int-expr)|pred(int-expr) |function-symbol(int-expr,...,int-expr) Figure1:SUF Syntax. icate symbols with zero arguments,writing a instead of a().We refer to function symbols of zero arity as symbolic constants,and to predicate symbols of zero arity as symbolic Boolean constants. Uninterpreted functions and predicates are used in hardware de- sign veri?cation to abstract word-level values of data and imple- mentation details of functional blocks.These functions and pred- icates satisfy no particular property other than functional consis- tency,viz.,that they evaluate to the same value on the same argu-ments.Adding equalities,inequalities,and interpreted functions succ and pred facilitates reasoning about ordering and equality of data values,and modeling ordered data structures such as queues. 2.1Decision Procedure Overview Assume we start with a well-formed formula F suf in SUF.The de- cision procedure must determine whether it is valid,i.e.,true un- der all possible interpretations of the function and predicate sym- bols.Through a sequence of validity-preserving transformations, we convert a SUF formula to a propositional formula F bool.Va- lidity of F suf is then checked by checking the(un)satis?ability of ?F bool. 2.1.1Eliminating Function Applications The?rst step is to eliminate applications of uninterpreted func- tion and predicate symbols of arity greater than one.In doing so, we keep track of a property of function applications called posi- tive equality.The general idea is to determine the polarity of each equality in the formula,i.e.,whether it appears under an even(pos- itive)or odd(negative)number of negations.Applications of un- interpreted functions can then be classi?ed as either p-function ap- plications,i.e.,used only under positive equalities,or g-function applications,i.e.,general function applications that appear under other equalities or under inequalities.The p-function applications can be encoded in propositional logic with fewer Boolean variables than the g-function applications,thus greatly simplifying the result- ing SAT problem. To be able to exploit positive equality,Bryant et al.eliminate function applications using“ITE”expressions.As an example,if function symbol f has two occurrences:f(a1)and f(a2),then we would generate2new symbolic constants vf1and vf2.We would then replace all instances of f(a1)by vf1and all instances of f(a2) by ITE(a2=a1,vf1,vf2).Note that this encoding ensures func-tional consistency.Predicate applications are eliminated using a similar process. 2.1.2Deciding Separation Logic Eliminating function and predicate applications leaves us with a formula F sep containing only symbolic constants,ITEs,successors, predecessors,equations,inequalities,and Boolean connectives.We will refer to this logic as separation logic.In addition,we will refer to equalities or inequalities involving only symbolic constants, successors,and predecessors,as separation predicates. The problem of deciding the satis?ability of a formula in separation logic is NP complete.It is NP-hard since Boolean satis?ability can be trivially reduced to it.In addition,it is in NP because the logic has a“small-model”property,viz.,if it is satis?able,there exists a satisfying assignment such that the values of the integer symbolic constants in the formula are polynomially bounded in the size of the formula. As mentioned in Section1,there are two approaches to encoding a formula in separation logic as a Boolean formula: 1.Small-Domain Encoding(SD):For each symbolic constant v i in F sep,we compute the bound b i on its value.The bounds b i are then used to derive an encoding of each v i as a“sym- bolic bit-vector”of Boolean variables.This results in a for- mula with only Boolean variables,along with ITEs,succes- sors,predecessors,equations,inequalities,and Boolean con- nectives.Binary arithmetic is then used to transform this for- mula into a Boolean formula F bool. 2.Per-Constraint Encoding(EIJ):In this method,we?rst eliminate the ITE construct from the formula,to get a for- mula that is a Boolean combination of separation predicates. Each separation predicate is then encoded with a fresh Boolean variable to get a Boolean formula F bvar.To rule out as- signments to these Boolean variables that do not correspond to any assignment to the integer-valued symbolic constants in F sep,we construct a Boolean formula F trans that imposes “transitivity constraints”on the values of the fresh Boolean variables.For example,if e=,0 x,y encodes x=y,and e =,0 y,z en- codes y=z,we would impose the constraint e=,0 x,y∧e =,0 y,z=? e=,0 x,z.This process might,in general,result in new Boolean variables,such as e=,0 x,z,being generated.Let F trans denote the conjunction of all the imposed constraints.We?nally construct F bool as F trans=?F bvar. For example,if F sep is x≥y∧y≥z∧z≥succ(x),then using SD, F bool is the Boolean formula [ 0x1x0 ≥ 0y1y0 ]∧[ 0y1y0 ≥ 0z1z0 ]∧[ 0z1z0 ≥ 0x1x0 +1] where2Boolean variables suf?ce to encode each symbolic con-stant,and the arithmetic and relational operators are re-interpreted over bit-vectors of https://www.sodocs.net/doc/6d3290449.html,ing EIJ,F bool is [(e≥,0x,y∧e≥,0y,z=?e≥,0x,z)∧(e≥,0x,z=??e≥,1z,x)]=?[e≥,0x,y∧e≥,0y,z∧e≥,1z,x] where the antecedent of the outermost implication is F trans and the consequent is F bvar. Each of SD and EIJ has its drawbacks when used in isolation.We describe these drawbacks in the next section. https://www.sodocs.net/doc/6d3290449.html,PARISON OF SD AND EIJ The method of encoding a SUF formula using SD usually results in a compact Boolean formula.As shown in[6],if there are N distinct nodes in the Directed Acyclic Graph(DAG)representation of a SUF formula F suf,then the size of the DAG for the resulting Boolean formula is roughly O(Nlg(N)).However,since numerical constants are encoded in unary(e.g.,x+k as succ k(x)),N can be very large if the formula has very large constants.However,in our experience,formulas rarely have very large constants.The EIJ method,on the other hand,can produce a Boolean formula whose size is exponential in N.This is because there is a potential of gen-erating an exponential number of transitivity constraints using this method[14].Note,however,that for the subclass of logic involving only equalities without arithmetic,the number of transitivity con-straints grows only polynomially in the number of equalities in the original formula[7]. The SD and EIJ methods also differ in their impact on search in SAT solvers.As the SD method uses a vector of Boolean vari-ables to encode each symbolic constant,suf?cient number of these Boolean variables have to be assigned values before the search space of solutions is pruned.On the other hand,in the EIJ method, each separation predicate(e.g.,x≥y+c)is encoded using a sin-gle Boolean variable(e.g.,e≥,c x,y).This encoding appears to assist the DPLL-based SAT solvers,as has been observed by Velev and Bryant[15]for deciding the restricted class of EUF logic.This is probably because,in many formulas,separation predicates con-trol the values sub-expressions of the formula evaluate to,and so assigning to the corresponding Boolean variables is more likely to lead to a con?ict or a satisfying assignment. In previous work[5],we performed an experimental study compar-ing SD and EIJ along with other variants of a decision procedure for SUF.The results indicated that neither SD nor EIJ performed consistently well over all benchmarks used in the study.However, it was noted that they appear to complement each other,suggesting that they might perform well in combination.In the same paper,we presented a hybrid technique that encodes equalities without arith-metic using EIJ and the remaining separation predicates using SD; however,this combination met with limited success as the decision of whether to choose SD or EIJ is?xed,i.e.,it does not depend on features of the formula being checked. In the rest of this section,we report on new experiments that con-?rm our previous?ndings comparing SD and EIJ and identify fea-tures of input formulas that affect the relative performance of SD and EIJ. Benchmarks.For use in all the experiments reported in this pa-per,we collected a set of49valid SUF formulas to use as bench-marks,many of which were used in our previous study[5],and are described in detail in that paper.We drew these formulas from real problems encountered in both hardware and software design veri?cation.The hardware designs include the load-store unit of an industrial microprocessor,an out-of-order microprocessor de-sign[11],a cache coherence protocol,and a5-stage DLX pipeline. The software benchmarks are generated in the veri?cation of safety properties of device driver code[10],and in translation valida-tion[13].The sizes of the formulas,when measured in terms of the number of nodes in a DAG representation,range from100nodes to 7500nodes. For the experiments described in this section,we selected a sam-ple of16formulas at random from the above benchmark set such that there was at least1formula from each problem domain.Ex-periments were run on a Pentium-IV2GHz machine with1GB of RAM. Impact on SAT solver.We?rst performed an experiment to study how the encoding method affects the performance of the SAT solver. Figure2shows results on5of the larger benchmarks from the sample of size16.The numbers in the table support our conjec-ture that the EIJ encoding is more effective with SAT solvers.Al-though the original number of clauses are far more in the case of EIJ method(due to transitivity constraints),the number of con?ict clauses needed to span the entire search space is far less for EIJ en-coding.The lower number of con?ict clauses added for EIJ method suggests better pruning of the search space through case splitting on the Boolean variables encoding separation constraints.This di-rectly translates to signi?cant improvement in the run time of the SAT solver(zChaff). Benchmark#of CNF#of Con?ict SAT Time Clauses Clauses(sec) SD EIJ SD EIJ SD EIJ 22s676991693871581115021.630.56 25s6752810494112304959.710.29 elf.r830556308891807770.890.06 ooo.t128544111648220364293731.83 5.49 dlx274693703311358745 5.060.43 Figure2:Effect of Encoding on zChaff performance.“Con?ict Clauses”denotes the con?ict clauses added by zChaff. Combining SD and EIJ based on Formula Features.From the preceding discussion and experimental results,it appears that EIJ would be a better encoding method except in cases where the num-ber of transitivity constraints grows too large,slowing down the translation procedure.Thus,a decision rule that chooses between the EIJ and SD methods of encoding would ideally be based on an estimate of the the number of transitivity constraints.Unfortu-nately,this number is hard to estimate in polynomial time,since it corresponds to the problem of estimating the number of cycles in a directed graph.We therefore performed a set of experiments to identify other formula features that are closely correlated with the run-time of the SD and EIJ methods.We started with a can-didate set of several features,including(1)the number of separa-tion predicates in the formula obtained after eliminating function applications,(2)the maximum over the sizes of the small-model required for each symbolic constant,(3)the fraction of function-applications that were p-function applications,and(4)the sum of the sizes of the small-models.The intuition was,for example,to use the number of separation predicates as an estimate of complex-ity of the EIJ method,and the small-model size as an estimate for the SD method. For each of the16benchmarks,we measured CPU run-time,nor-malized by the size of the original SUF formula.The normalization allows us to study how each formula feature affects the run-time by removing the effect of formula size,yielding similar normalized run-times for formulas with similar features.The CPU run-times have two components:the time taken to translate the formula to a Boolean formula,and the time taken by the SAT solver to solve that resulting Boolean formula. 0.25 1 4 16 64 256 1416642561024 N o r m a l i z e d T o t a l T i m e ( s e c / K n o d e s ) Number of Separation Predicates SD EIJ Figure3:Effect of number of separation predicates on EIJ. Notice that both axes are on a log scale. We found that the only feature that showed any correlation with run-time was the number of separation predicates.Speci?cally,the run-times of the EIJ method show good correlation with the number of separation predicates,as shown in Figure 3.When the number of separation predicates is low,the EIJ method outperforms the SD method,due to faster SAT times.But as the number increases,its performance gets worse,until beyond a certain threshold,the EIJ method fails to go beyond the formula translation stage (and was timed out after an hour).In Figure 3,this occurs for the three benchmarks with the largest number of separation predicates.On the contrary,the small-domain method completes within 6minutes on all these three benchmarks. The results shown in Figure 3indicate a natural heuristic for choos-ing between SD and EIJ,viz.,checking if the number of separation predicates is greater than a threshold value SEP THOLD .If the num-ber exceeds the threshold,we can use the SD encoding method,otherwise,we use EIJ.In the next section,we show how we can use this heuristic to develop a new hybrid method of encoding the separation logic formula as a Boolean formula. 4.HYBRID METHOD A naive scheme based on the results of the previous section might use the number of separation predicates to select either SD or EIJ for encoding the entire formula F sep .However,we can exploit the formula structure to encode different parts of the formula using dif-ferent methods.The main idea is to group symbolic constants into classes,and use a different encoding method for each class.To do this,we de?ne two symbolic constants to be in the same class if they are compared to each other using an equality or an inequality.Symbolic constants appearing in F sep are thus partitioned into equiv-alence classes,where those in one equivalence class can be encoded completely independent of symbolic constants in other equivalence classes.For each class,the choice of encoding is based on the num-ber of separation predicates which involve two symbolic constants from that class.In the rest of this section,we describe the steps in the hybrid encoding method,viz.,how to compute the equiva-lence classes,estimate the number of separation predicates for each class,and then ?nally use the estimate to encode the formula using a combination of both schemes. 1.Generate Classes.We ?rst collect the set of symbolic constants occurring in F sep into two sets V p and V g .V p consists of those sym-bolic constants occurring in F suf that were classi?ed as p-function applications,as well as those constants vf i that were introduced when eliminating an application of some p-function symbol f .The remaining symbolic constants are in V g . We start by assigning each symbolic constant in V g to its own class.We then compute the dependency set for each term in F sep ,denoting some subset of symbolic constants in V g to which this term could evaluate.While doing this,we merge some of the classes so that each dependency set is a subset of some class.For term T . =v , its dependency set is /0 if v ∈V p and is {v }if v ∈V g .For term T . =succ (T 1),its dependency set is the same as that of T 1.Similarly for T .=pred (T 1).For T . =ITE (F ,T 1,T 2),its dependency set is the union of those of T 1and T 2.If the dependency sets of T 1and T 2are subsets of two distinct classes,then we merge those classes.For each equation T 1=T 2and each inequality T 1 ground terms by repeatedly applying the following rewrite rules until a ?xed point is reached. succ (pred (T ))→T pred (succ (T ))→T succ (IT E (F ,T 1,T 2))→IT E (F ,succ (T 1),succ (T 2))pred (IT E (F ,T 1,T 2))→IT E (F ,pred (T 1),pred (T 2)) At this point,the terms at the leaves consist of only ground terms.For brevity,from now on we will simply write v +k (respectively v ?k )for succ k (v )(resp.pred k (v )). https://www.sodocs.net/doc/6d3290449.html,pute Domain Sizes.For each symbolic constant v ,we compute u (v ),the maximum amount it can be incremented and l (v ),the maximum amount it can be decremented.u (v )represents the maximum offset of v in any of the ground terms present in the formula.Similarly,l (v )represents the minimum offset.For ex-ample,if {v ?4,v ?2,v ,v +3,v +7}is the set of ground terms in which v appears,then u (v )=7,and l (v )=? 4.For each class V i we compute its range as: range (V i ) = ∑v ∈V i (u (v )?l (v )+1). This determines the size of the ?nite instantiation we need to con-sider for each symbolic constant in V i for SD encoding.Interpreting the symbolic constants over bit vectors of this size is suf?cient to determine the validity of the separation logic formula (due to the small-model property). https://www.sodocs.net/doc/6d3290449.html,pute an upper bound on the number of separation pred-icates for each class.For each of the classes V i ,estimate SepCnt (V i ),the maximum number of separation predicates which would in-volve two symbolic constants from the class V i .This is done as follows.Initially,SepCnt (V i )=0,for each class V i .Then,for each equation T 1=T 2and each inequality T 1 At the end of the process SepCnt (V i )gives an upper bound on the number of separation predicates that would involve two symbolic constants from the class V i .1 5.Perform hybrid encoding.At this point,we have all the in-formation we need to encode the separation logic formula into a Boolean formula.As discussed in Section 3,we use the threshold value SEP THOLD to avoid encoding classes that have a very large number of separation predicates with the EIJ method. The algorithm proceeds by recursing on the formula structure.A symbolic Boolean constant retains the same encoding.For a node f 1∧f 2,we recursively encode the subexpressions f 1,f 2and con-join the results.Similarly,?f 1is evaluated by encoding f 1and negating the result.The more interesting cases involve equation or inequalities. For each equation T 1=T 2or an inequality T 1 If SepCnt (V T 1)>SEP THOLD ,then we encode T 1,T 2using SD method.The encodings of T 1and T 2are symbolic bit-vectors.Bit-wise equality or comparison is used to translate these bit-vectors to a Boolean expression.Each symbolic constant is encoded with 1SepCnt (V i ) is an upper bound because we count predicates that disappear after eliminating ITEs,e.g.,counting (v 1,v 2)at the node ITE (F ,v 1,v 2)=ITE (?F ,v 2,v 1). a vector of symbolic Boolean constants.The size of the vector is determined by the domain size computed previously.Note that symbolic constants in V p are assigned distinct bit-string values.The arithmetic operations succ and pred are encoded using binary arith-metic,and IT E expressions are encoded as multiplexors. Otherwise,we use the EIJ method to encode T 1and T 2,using the technique proposed by Bryant et al.[4].Suppose T 1evaluates to a ground term g i under the condition c 1i ,and T 2evaluates to g j under c 2j .For example,the term ITE (F ,v 1,v 2)evaluates to v 2under ?F .The encoding of the predicate T 1 T 2,where ∈{=,<},is given by i ,j c 1i ∧c 2j ∧e g i ,g j ,where e g i ,g j is a symbolic Boolean constant to encode the constraint g i g j .Note that if either of g i or g j contains a symbolic constant from V p ,then e g i ,g j =false . 6.Generate F bool .Let F bvar denote the formula obtained by per-forming the hybrid encoding on F sep .We generate the conjunction F trans of all transitivity constraints for predicates in F sep encoded using the EIJ method.The ?nal Boolean formula F bool is then gen-erated as (F trans =?F bvar ). Hereafter we will denote our hybrid encoding method by H YBRID . 4.1Automatically Selecting a Threshold The value of the threshold parameter SEP THOLD determines the mix of SD and EIJ in H YBRID ,and hence determines its overall ef?ciency.For example,when SEP THOLD =0,H YBRID is the same as SD.While it might be acceptable to manually set the value of SEP THOLD for some formulas,it is highly desirable to ?nd a good default value. We select a default value of SEP THOLD by statistical analysis of the results of running EIJ on a sample of the benchmarks.As a sample,we selected the same 16benchmarks that we used in Sec-tion 3to ?nd the correlation of EIJ with the number of separation predicates.Given the sorted sequence T 1,...,T 16of the normal-ized run-times of EIJ on these benchmarks,we calculated the value of k ,1≤k ≤16,that minimized the sum of the variances of each the two subsets {T 1,...,T k }and {T k +1,...,T 16}.Dividing points into subsets in this manner is a well-known technique for cluster-ing points in one dimension,using squared distance as a measure of similarity.Having performed this clustering,we chose the de-fault SEP THOLD as the smallest multiple of 100greater than n k ,the number of separation predicates corresponding to the run-time T k .For our sample set,we calculated n k to be 676,so we set the default value of SEP THOLD to be 700for all experiments reported in Section 5. In general,a user can determine a default SEP THOLD by using a similar statistical technique on all formulas from a relevant domain that the tool has been run on in the past. 5.RESULTS &DISCUSSION We implemented a decision procedure for SUF based on H YBRID in Moscow ML,a dialect of the Standard ML programming lan-guage.In this section,we describe empirical results comparing H YBRID with the SD and EIJ encoding methods.We also report comparisons with other decision procedures. All experiments were run on a Pentium-IV 2GHz machine with 1GB of RAM running Linux.As a SAT engine,we used the zChaff SAT solver (version 2001.2.17)with the default options.A limit of 30minutes was imposed on each run of a decision procedure.We used the entire set of 49benchmarks described in Section 3,com-paring H YBRID to SD,EIJ,and other decision procedures on the total time taken to decide each formula.For H YBRID ,SD,and EIJ,this is the sum of the encoding time and the SAT time.Our results are depicted in Figures 4,5,and 6.In each plot,the x-coordinate of each point is the time taken by H YBRID ,and the y-coordinate is the time taken by the decision procedure we compare it against.We also plot the diagonal line y =x in each plot.Thus,points above the diagonal correspond to benchmarks on which H YBRID outperforms the other procedures,while points below it correspond to benchmarks on which H YBRID is outperformed. Comparing H YBRID to SD and EIJ.The results obtained from comparing H YBRID against SD and EIJ fall into two categories.The ?rst set of results are on 39benchmarks on which H YBRID with the default value of SEP THOLD outperformed both SD and EIJ,and are depicted in Figure 4.These 39benchmarks exclude formulas generated in proving correctness of hardware designs us-ing invariant checking.On the remaining 10benchmarks,SD out-performed both EIJ and H YBRID ,for various values of SEP THOLD greater than 100including the default value;the results obtained by setting SEP THOLD to 100are shown in Figure 5. Figure 4shows that H YBRID scales better than EIJ and SD.We notice that SD and EIJ timed out after 30minutes on some bench-marks,while H YBRID completed on all benchmarks.On several benchmarks that SD and EIJ completed on,H YBRID is a factor of 4to 8times faster.The only benchmarks on which SD and EIJ are marginally faster than H YBRID are small ones,all of which are decided within 16seconds.The improvement of H YBRID over EIJ is due to reduction in the number of transitivity constraints,while the improvement over SD is due to reduced SAT time.On one in-stance,zChaff fails to decide the SAT problem generated by SD within the timeout limit of 30minutes,while it ?nishes on the H Y -BRID encoding in about 90seconds. 0.25 1 4 16 64 256 1024 timeout 0.25 1 4 16 64 256 1024 T o t a l T i m e f o r E I J o r S D (s e c .) Total Time for Hybrid (sec.) EIJ SD Figure 4:Comparing H YBRID against EIJ and SD.Non-invariant checking benchmarks were used.Note the log scales on both axes. However,the results on the invariant checking formulas are very different.These formulas are characterized by many inequalities and a very large number of applications of uninterpreted functions,almost none of which are p-function applications.This results in a relatively small number of large-sized symbolic constant classes.Thus,even if the original number of separation predicates in each class is relatively low (e.g.,less than SEP THOLD ),the number of symbolic constants involved in those predicates is large,and this leads to a large number of transitivity constraints.Hence,using the EIJ encoding method results in poor performance,whether in pure form or in H YBRID .We found that SD performs the best on these benchmarks.EIJ and H YBRID using the default value of SEP THOLD fail to complete on any of them.Setting SEP THOLD to 100,we found that H YBRID manages to complete on some bench-marks,but it is still outperformed by SD,as shown in Figure 5. 16 64 256 1024 timeout 16 642561024timeout T o t a l T i m e f o r E I J o r S D (s e c .) Total Time for Hybrid (sec.) SD EIJ Figure 5:Comparing H YBRID against SD and EIJ on invariant checking benchmarks.SEP THOLD was set to 100. Comparison with Other Decision Procedures.We compared our decision procedure against existing decision procedures that can decide SUF formulas.One such procedure is the Stanford Valid-ity Checker (SVC)[2].SVC (version 1.1)can decide a superset of SUF,including,in addition,linear arithmetic and bit-vector arith-metic.We also compared against the more recent Cooperating Va-lidity Checker (CVC)[3],which is SAT-based.In all experiments,we used H YBRID with the default value of 700for SEP THOLD .Since both SVC and CVC interpret function applications over the rational numbers,we could not run them on the invariant check-ing benchmarks which involve inequalities,and whose validity de-pends on the property that the integers are not dense.We there-fore restricted our performance comparisons to the 39non-invariant checking benchmarks. Figure 6compares H YBRID against both CVC and SVC.Let us ?rst consider the comparison with SVC.We see that the formulas on which SVC outperforms H YBRID are relatively small,decided within 32seconds.This is mainly due to the overhead of translating to SAT in H YBRID .Also many of these formulas are conjunctions of atomic predicates on which SVC performs well,since deciding a conjunction of separation predicates can be reduced to a shortest-path problem.However,for larger formulas involving several dis-junctions,SVC’s run-time quickly blows up,and it fails to ?nish within 30minutes.H YBRID ,on the other hand,completes within 3minutes on all formulas. 0.25 1 4 16 64 256 1024 timeout 0.25 1 4 1664 256 1024 T o t a l T i m e f o r C V C o r S V C (s e c .) Total Time for Hybrid (sec.) SVC CVC Figure 6:Comparing H YBRID against SVC and CVC.Next,consider the comparison with CVC.Like EIJ,CVC works by replacing every equality or inequality with a fresh Boolean vari-able,and calling a SAT solver (a customized version of Chaff)on the Boolean encoding.However,unlike EIJ,transitivity constraints are enforced lazily,based on adding con?ict clauses to rule out spu-rious satisfying assignments from the SAT solver.Each iteration of adding con?ict clauses requires a call to a ?rst-order decision pro-cedure.Our experiments indicate that for many benchmarks,the overhead of lazy enforcement of transitivity constraints is too high,and H YBRID outperforms CVC by orders of magnitude.The ex-ceptional cases where CVC outperforms H YBRID are conjunctions that are decided by both methods within 16seconds.We believe this is because CVC tries to add con?ict clauses that involve the smallest possible subset of literals from the satisfying assignment,and for a conjunction,this clause enforces transitivity constraints without need for further iteration. Conclusions.The hybrid encoding method presented in this paper combines the complementary strengths of the small-domain and per-constraint encodings.Even with the default value of threshold,the method is robust to variations in formula characteristics,per-forming well on the majority of the benchmarks,and scaling better than other decision procedures. Acknowledgments We are grateful to Steven German,Ranjit Jhala,and Ofer Strichman for providing us with benchmarks. 6.REFERENCES [1]G.Audemard,P.Bertoli,A.Cimatti,A.Korniowicz,and R.Sebastiani.A SAT based approach for solving formulas over Boolean and linear mathematical propositions.In CADE’02,volume LNCS 2392,pages 195–210. [2] C.Barrett,D.Dill,and J.Levitt.Validity checking for combinations of theories with equality.In FMCAD’96,LNCS 1166,pages 187–201. [3] C.Barrett,D.Dill,and A.Stump.Checking satis?ability of ?rst-order formulas by incremental translation to SAT.In CAV’02,LNCS 2404,pages 236–249. [4]R.E.Bryant,S.German,and M.N.Velev.Processor veri?cation using ef?cient reductions of the logic of uninterpreted functions to propositional logic.ACM Transactions on Computational Logic ,2(1):1–41,January 2001. [5]R.E.Bryant,https://www.sodocs.net/doc/6d3290449.html,hiri,and S.A.Seshia.Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings.In Constraints in Formal Veri?cation CFV’02. [6]R.E.Bryant,https://www.sodocs.net/doc/6d3290449.html,hiri,and S.A.Seshia.Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions.In CAV’02,LNCS 2404,pages 78–92.[7]R.E.Bryant and M.N.Velev.Boolean satis?ability with transitivity constraints.In CAV ’00,LNCS 1855,pages 85–98. [8]J.R.Burch and D.L.Dill.Automated veri?cation of pipelined microprocessor control.In CAV ’94,LNCS 818,pages 68–80. [9]S.Das,D.Dill,and S.Park.Experience with predicate abstraction. In CAV’99,LNCS 1633,pages 160–171. [10]T.A.Henzinger,R.Jhala,R.Majumdar,G.C.Necula,G.Sutre,and W.Weimer.Temporal-safety proofs for systems code.In CAV’02,LNCS 2404,pages 526–538. [11]https://www.sodocs.net/doc/6d3290449.html,hiri,S.A.Seshia,and R.E.Bryant.Modeling and veri?cation of out-of-order microprocessors in UCLID.In FMCAD’02,LNCS 2517,pages 142–160. [12] A.Pnueli,Y .Rodeh,O.Shtrichman,and M.Siegel.Deciding equality formulas by small-domain instantiations.In CAV’99,LNCS 1633,pages 455–469. [13] A.Pnueli,M.Siegel,and O.Shtrichman.The code validation tool (CVT)-automatic veri?cation of a compilation process.Software Tools for Technology Transfer ,2,1998,pages 192–201. [14]O.Strichman,S.A.Seshia,and R.E.Bryant.Deciding separation formulas with SAT.In CAV’02,LNCS 2404,pages 209–222. [15]M.N.Velev and R.E.Bryant.Effective use of Boolean satis?ability procedures in the formal veri?cation of superscalar and VLIW microprocessors.In DAC ’01,pages 226–231. Web性能测试方案 1测试目的 此处阐述本次性能测试的目的，包括必要性分析与扩展性描述。 性能测试最主要的目的是检验当前系统所处的性能水平，验证其性能是否能满足未来应用的需求，并进一步找出系统设计上的瓶颈，以期改善系统性能，达到用户的要求。 2测试范围 此处主要描述本次性能测试的技术及业务背景，以及性能测试的特点。 编写此方案的目的是为云应用产品提供web性能测试的方法，因此方案内容主要包括测试环境、测试工具、测试策略、测试指标与测试执行等。 2.1测试背景 以云采业务为例，要满足用户在互联网集中采购的要求，实际业务中通过云采平台询报价、下单的频率较高，因此云采平台的性能直接决定了业务处理的效率，并能够支撑业务并发的压力。 例如：支撑100家企业用户的集中访问，以及业务处理要求。 2.2性能度量指标 响应时间（TTLB） 即“time to last byte”，指的是从客户端发起的一个请求开始，到客户端接收到从服务器端返回的响应结束，这个过程所耗费的时间，响应时间的单位一般为“秒”或者“毫秒”。响应时间＝网络响应时间+应用程序响应时间。 响应时间标准： 事务能力TPS（transaction per second） 服务器每秒处理的事务数； 一个事务是指一个客户机向服务器发送请求然后服务器做出反应的过程。 客户机在发送请求时开始计时，收到服务器响应后结束计时，一次来计算使用的时间和完成的事务个数。它是衡量系统处理能力的重要指标。 并发用户数 同一时刻与服务器进行交互的在线用户数量。 吞吐率（Throughput） 单位时间内网络上传输的数据量，也可指单位时间内处理的客户端请求数量，是衡量网络性能的重要指标。 吞吐率=吞吐量/传输时间 资源利用率 这里主要指CPU利用率（CPU utilization），内存占用率。 3测试内容 此处对性能测试整体计划进行描述，包括测试内容以及关注的性能指标。Web性能测试内容包含：压力测试、负载测试、前端连接测试。 3.1负载测试 负载测试是为了测量Web系统在某一负载级别上的性能，以保证Web系统在需求范围内能正常工作。负载级别可以是某个时刻同时访问Web系统的用户数量，也可以是在线数据处理的数量。例如：Web应用系统能允许多少个用户同时在线？如果超过了这个数量，会出现什么现象？Web应用系统能否处理大 上海交通大学医学院附属瑞金医院放射科简介 瑞金医院放射科目前为影像医学与核医学专业硕士、博士及博士后培养点，上海市住院医师规范化培训考核基地。科室现有高级职称人员18名，博士生导师2名，硕士生导师4名，在读博士研究生和硕士研究生20余名，每年招收进修医师25-30名。拥有多层螺旋CT 4台，磁共振检查仪3台，平板DSA设备3台及数字胃肠机、数字平板钼靶机、DR、CR等大型医疗设备。放射科已有完整的PACS和RIS系统，放射科的数字化建设已走在全国的前列。每年承办国家级继续教育学习班3-4项，主持国际多中心研究多项。近年来成功地主办、协办了多次大型国际性及区域性会议。科室与比利时、法国、美国等相关大学医院建立了多项合作交流项目，每年接待国外来访学者多批，并每年排除进修人员多名。2006年同比利时自由大学医院共同举办了中比神经影像研讨会，在上海、北京、杭州三地举行，受到了相当的好评。科室具有较强的师资队伍，在法文、英文教学方面具有特色，目前承担了上海市教委的影像学精品课程项目。 放射专业逐步形成了骨关节疾病、内分泌疾病、消化道和胰腺疾病、乳腺疾病、颅神经病变等方面的传统诊疗特色，开展了众多具有国际先进水平的特色项目：各类肿瘤或肿瘤样病变CT导引下的穿刺病理活检术；全身范围的多层CTA 检查；面肌痉挛和三叉神经痛的磁共振诊断；磁共振功能成像对脑认知的研究；乳腺癌影像学早期诊断；肾上腺病变的介入性治疗；肾动脉球囊扩张或内支架成形术治疗肾血管性高血压；CT引导下经皮治疗腰突症所致的坐骨神经根炎；半导体激光对原发及转移性肿瘤的姑息治疗；半导体激光治疗骨样骨瘤等。学科目前承担国家自然科学基金1项、上海市重大课题项目4项、市科委、市教委、市卫生局等基金及其它各类基金近20项；近年来获上海市科学技术进步“三等奖”2项、上海市医学科技奖“三等奖”2项。 联系导师简介 陈克敏，男，1951年1月出生，教授、主任医师 放射科主任，1976年毕业于上海第二医学院医学系，长期从事放射诊断和介入治疗的临床、教学和研究工作。目前担任中华医学会放射学分会委员、中国医学影像技术研究协会放射学分会副主任委员、上海放射学会副主任委员、国家 品质体系框架图 图中各缩写词含义如下： QC：Quality Control 品质控制 QA：Quality Assurance 品质保证 QE：Quality Engineering 品质工程 IQC：Incoming Quality Control 来料品质控制 LQC：Line Quality Control 生产线品质控制 IPQC：In Process Quality Control 制程品质控制 FQC：Final Quality Control 最终品质控制 SQA：Source (Supplier) Quality Assurance 供应商品质控制 DCC：Document Control Center 文控中心 PQA：Process Quality Assurance 制程品质保证 FQA：Final Quality Assurance 最终品质保证 DAS：Defects Analysis System 缺陷分析系统 FA：Failure Analysis 坏品分析 CPI：Continuous Process Improvement 连续工序改善 CS：Customer Service 客户服务 TRAINNING：培训 一供应商品质保证（SQA） 1.SQA概念 SQA即供应商品质保证，识通过在供应商处设立专人进行抽样检验，并定期对供应商进行审核、评价而从最源头实施品质保证的一种方法。是以预防为主思想的体现。 2.SQA组织结构 3.主要职责 1）对从来料品质控制（IQC）/生产及其他渠道所获取的信息进行分析、综合，把结果反馈给供应商，并要求改善。 2）耕具派驻检验远提供的品质情报对供应商品质进行跟踪。 3）定期对供应商进行审核，及时发现品质隐患。 4）根据实际不定期给供应商导入先进的品质管理手法及检验手段，推动其品质保证能力的提升。 5）根据公司的生产反馈情况、派驻人员检验结果、对投宿反应速度及态度对供应商进行排序，为公司对供应商的取舍提供依据。 4.供应商品质管理的主要办法 1）派驻检验员 把IQC移至供应商，使得及早发现问题，便于供应商及时返工，降低供应商的品质成本，便于本公司快速反应，对本公司的品质保证有利。同时可以根据本公司的实际使用情况及IQC的检验情况，专门严加检查问题项目，针对性强。 2）定期审核 通过组织各方面的专家对供应商进行审核，有利于全面把握供应商的综合能力，及时发现薄弱环节并要求改善，从而从体系上保证供货品质定期排序，此结果亦为供应商进行排序提供依据。 一般审核项目包含以下几个方面 A．品质。 B．生产支持。 C．技术能力及新产品导入。 D．一般事务. 具体内容请看“供应商调查确认表”. 3）定期排序 排序的主要目的是评估供应商的品质及综合能力，以及为是否保留、更换供应商提供决策依据.排序主要依据以下几个方面的内容： A.SQA批通过率：一般要求不低于95%。 B.IQC批合格率：一般要求不低于95%。 天线分集技术的原理 最初，许多设计者可能会担心区域规范的复杂性问题，因为在全世界范围内，不同区域规范也各异。然而，只要多加研究便能了解并符合不同区域的法规，因为在每一个地区，通常都会有一个政府单位负责颁布相关文件，以说明“符合特定目的的发射端相关的规则。 无线电通信中更难于理解的部分在于无线电通信链路质量与多种外部因素相关，多种可变因素交织在一起产生了复杂的传输环境，而这种传输环境通常很难解释清楚。然而，掌握基本概念往往有助于理解多变的无线电通信链接品质，一旦理解了这些基本概念，其中许多问题可以通过一种低成本、易实现的被称作天线分集(antenna diversity)的技术来实现。 环境因素的考虑 影响无线电通信链路持续稳定的首要环境因素是被称为多径/衰落和天线极化/分集的现象。这些现象对于链路质量的影响要么是建设性的要么是破坏性的，这取决于不同的特定环境。可能发生的情况太多了，于是，当我们试着要了解特定的环境条件在某个时间点对无线电通信链接的作用，以及会造成何种链接质量时，这无疑是非常困难的。 天线极化/分集 这种被称为天线极化的现象是由给定天线的方向属性引起的，虽然有时候把天线极化解释为在某些无线电通信链路质量上的衰减，但是一些无线电通信设计者经常利用这一特性来调整天线，通过限制收发信号在限定的方向范围之内达其所需。这是可行的，因为天线在各个方向上的辐射不均衡，并且利用这一特性能够屏蔽其他（方向）来源的射频噪声。 简单的说，天线分为全向和定向两种。全向天线收发信号时，在各个方向的强度相同，而定向天线的收发信号被限定在一个方向范围之内。若要打造高度稳固的链接，首先就要从了解此应用开始。例如：如果一个链路上的信号仅来自于特定的方向，那么选择定向天线获 目录 1前言 (2) 1.1 文档目的 (2) 1.2 适用对象 (2) 2性能测试目的 (2) 3性能测试所处的位置及相关人员 (3) 3.1 性能测试所处的位置及其基本流程 (3) 3.2 性能测试工作内容 (4) 3.3 性能测试涉及的人员角色 (5) 4性能测试实施规范 (5) 4.1 确定性能测试需求 (5) 4.1.1 分析应用系统，剥离出需测试的性能点 (5) 4.1.2 分析需求点制定单元测试用例 (6) 4.1.3 性能测试需求评审 (6) 4.1.4 性能测试需求归档 (6) 4.2 性能测试具体实施规范 (6) 4.2.1 性能测试起始时间 (6) 4.2.2 制定和编写性能测试计划、方案以及测试用例 (7) 4.2.3 测试环境搭建 (7) 4.2.4 验证测试环境 (8) 4.2.5 编写测试用例脚本 (8) 4.2.6 调试测试用例脚本 (8) 4.2.7 预测试 (9) 4.2.8 正式测试 (9) 4.2.9 测试数据分析 (9) 4.2.10 调整系统环境和修改程序 (10) 4.2.11 回归测试 (10) 4.2.12 测试评估报告 (10) 4.2.13 测试分析报告 (10) 5测试脚本和测试用例管理 (11) 6性能测试归档管理 (11) 7性能测试工作总结 (11) 8附录：............................................................................................. 错误！未定义书签。 1前言 1.1 文档目的 本文档的目的在于明确性能测试流程规范，以便于相关人员的使用，保证性能测试脚本的可用性和可维护性，提高测试工作的自动化程度，增加测试的可靠性、重用性和客观性。 1.2 适用对象 本文档适用于部门内测试组成员、项目相关人员、QA及高级经理阅读。 2性能测试目的 性能测试到底能做些什么，能解决哪些问题呢？系统开发人员，维护人员及测试人员在工作中都可能遇到如下的问题 1.硬件选型，我们的系统快上线了，我们应该购置什么样硬件配置的电脑作为 服务器呢？ 2.我们的系统刚上线，正处在试运行阶段，用户要求提供符合当初提出性能要 求的报告才能验收通过，我们该如何做？ 3.我们的系统已经运行了一段时间，为了保证系统在运行过程中一直能够提供 给用户良好的体验（良好的性能），我们该怎么办？ 4.明年这个系统的用户数将会大幅度增加，到时我们的系统是否还能支持这么 多的用户访问，是否通过调整软件可以实现，是增加硬件还是软件，哪种方式最有效？ 5.我们的系统存在问题，达不到预期的性能要求，这是什么原因引起的，我们 应该进行怎样的调整？ 6.在测试或者系统试点试运行阶段我们的系统一直表现得很好，但产品正式上 线后，在用户实际环境下，总是会出现这样那样莫名其妙的问题，例如系统运行一段时间后变慢，某些应用自动退出，出现应用挂死现象，导致用户对我们的产品不满意，这些问题是否能避免，提早发现？ 7.系统即将上线，应该如何部署效果会更好呢？ 并发性能测试的目的注要体现在三个方面：以真实的业务为依据，选择有代表性的、关键的业务操作设计测试案例，以评价系统的当前性能；当扩展应用程序的功能或者新的应用程序将要被部署时，负载测试会帮助确定系统是否还能够处理期望的用户负载，以预测系统的未来性能；通过模拟成百上千个用户，重复执行和运行测试，可以确认性能瓶颈并优化和调整应用，目的在于寻找到瓶颈问题。 作业参考答案——10-特殊图 1.(a)(c)(d)是欧拉图，(a)(b)(c)(d)(e)可以一笔画，(a)(b)(c)(d)(e)(f)(g)是 哈密顿图。 2.根据给定条件建立一个无向图G= 数至少为2，而V2中的每个结点度数至多为2，从而它满足t条件t=1，因此存在从V1到V2的匹配，故可分配。 5.此平面图具有五个面，如下图所示。 a b c d e f g r1r2 r3 r4 r5 ?r1，边界为abca，D(r1)=3; ?r2，边界为acga，D(r2)=3; ?r3，边界为cegc，D(r3)=3; ?r4，边界为cdec，D(r4)=3; ?r5，边界为abcdefega，D(r5)=8;无限面 6.设该连通简单平面图的面数为r，由欧拉公式可得，6?12+r=2，所以 r=8，其8个面分别设为r1,r2,r3,r4,r5,r6,r7,r8。因是简单图，故每个面至少由3条边围成。只要有一个面是由多于3条边所围成的，那就有所有面的次数之和 8∑ i=1 D(r i)>3×8=24。但是，已知所有面的次数之和等于边数的两倍，即2×12=24。因此每个面只能由3条边围成。 2 上海交通大学医学院附属瑞金医院北院 2018年度决算 目录 第一部分上海交通大学医学院附属瑞金医院北院概况 一、主要职能 二、机构设置 第二部分上海交通大学医学院附属瑞金医院北院2018年度决算表 一、收入支出决算总表 二、收入决算表 三、支出决算表 四、财政拨款收入支出决算总表 五、一般公共预算财政拨款支出决算表 六、一般公共预算财政拨款基本支出决算表 七、一般公共预算财政拨款“三公”经费及机关运行经费支出决算表 八、政府性基金预算财政拨款支出决算表 九、资产负债情况表 第三部分上海交通大学医学院附属瑞金医院北院2018年度决算情况说明 第四部分名词解释 第一部分上海交通大学医学院附属瑞金医院北院概况 一、主要职能 上海交通大学医学院附属瑞金医院北院是“郊区新建三级 综合医院项目”（“5+3+1”工程）的重要组成部分之一，位于嘉 定新城，于2009 年12月奠基，2012 年12月17日开始试运营。全院占地面积210亩，建筑面积72,000平方米，核定床位600张,核定编制800人，医院目前现有职工（含瑞金派驻及退 休回聘）903人，其中研究生学历272人，中高级职称320人，已开放临床医技科室41个，其中血液科、内分泌科、普外科等 多个瑞金母院固有的优势、重点学科在新院得到了有效的延伸 与发展。 瑞金医院北院的发展将本着“落户嘉定、服务周边”，改善 区域居民对优质医疗资源可及性的建设目标，继续朝着符合公 立医院综合改革总体思想和目标，紧密结合瑞金医院母院，有 所侧重，有所互补，捆绑错位发展；积极融合嘉定，与二级医 院和社区形成三级服务网络，更好地发挥在疑难复杂病例、危 急重症救治等方面的综合服务能力，切实为老百姓带来优质的 医疗服务。 二、机构设置 浅析发射分集与接收分集技术 1 概述 1.1 多天线信息论简介 近年来,多天线系统(也称为MIMO系统)引起了人们很大的研究兴趣,多天线系统原理如图1所示，它可以增加系统的容量,改进误比特率(BER).然而,获得这些增益的代价是硬件的复杂度提高,无线系统前端复杂度、体积和价格随着天线数目的增加而增加。使用天线选择技术，就可以在获得MIMO系统优势的同时降低成本。 图1 MIMO系统原理 有两种改进无线通信的方法：分集方法、复用方法。分集方法可以提高通信系统的鲁棒性，利用发送和接收天线之间的多条路径，改善系统的BER。在接收端，这种分集与RAKE接收提供的类似。分集也可以通过使用多根发射天线来得到，但是必须面对发送时带来的相互干扰。这一类主要是空时编码技术。 另外一类MIMO技术是空间复用，来自于这样一个事实：在一个具有丰富散射的环境中，接收机可以解析同时从多根天线发送的信号，因此，可以发送并行独立的数据流，使得总的系统容量随着min( , )线性增长，其中 和 是接收和发送天线的数目。 1.2 空时处理技术 空时处理始终是通信理论界的一个活跃领域。在早期研究中，学者们主要注重空间信号传播特性和信号处理，对空间处理的信息论本质探讨不多。上世纪九十年代中期，由于移动通信爆炸式发展，对于无线链路传输速率提出了越来越高的要求，传统的时频域信号设计很难满足这些需求。工业界的实际需求推动了理论界的深入探索。 在MIMO技术的发展，可以将空时编码的研究分为三大方向：空间复用、空间分集与空时预编码技术，如图2所示。 图2 MIMO技术的发展 1.3 空间分集研究 多天线分集接收是抗衰落的传统技术手段，但对于多天线发送分集，长久以来学术界并没有统一认识。1995年Telatarp[3]首先得到了高斯信道下多天线发送系统的信道容量和差错指数函数。他假定各个通道之间的衰落是相互独立的。几乎同时， Foschini和Gans在[4]得到了在准静态衰落信道条件下的截止信道容量(Outage Capacity)。此处的准静态是指信道衰落在一个长周期内保持不变，而周期之间的衰落相互独立，也称这种信道为块衰落信道(Block Fading)。 Foschini和Gans的工作，以及Telatar的工作是多天线信息论研究的开创 性文献。在这些著作中，他们指出，在一定条件下，采用多个天线发送、多个天线接收(MIMO)系统可以成倍提高系统容量，信道容量的增长与天线数目成线性关系 1.4 空时块编码 (STBC) 本文我们主要介绍一类高性能的空时编码方法——空时块编码( STBC: Space Time Block Code)。 STBC编码最先是由Alamouti[1]在1998年引入的，采用了简单的两天线发分集编码的方式。这种STBC编码最大的优势在于，采用简单的最大似然译码准则，可以获得完全的天线增益。 Tarokh[5]进一步将2天线STBC编码推广到多天线形式，提出了通用的正交设计准则。 2 MIMO原理及方案 ERP性能测试总结分享 1分享 (3) 1.1测试环境搭建 (3) 1.2并发量计算及场景设计 (3) 1.3测试框架搭建 (4) 1.4测试脚本开发/调试 (5) 1.5场景调试/执行 (5) 1.6性能监控分析 (6) 1.7结果报告 (7) 2展望 (8) 2.1业务调研及场景确定 (8) 2.2场景监控与分析 (8) 1分享 1.1 测试环境搭建 在我们进行性能测试之前，通常需要搭建一个供测试用的环境，使用这个环境来录制脚本，根据在这个环境下执行测试的结果，得出最终的测试结论。 有些时候，测试环境就是生产环境，例如：一个新的项目上线前进行的性能测试，通常就是在未来的生产环境下进行的。在这种情况下，可以排除测试环境与生产环境差异带来影响，测试结果相对比较准确。 反之，如果测试环境与生产环境不是同一环境，这个时候，为了保证测试结果的准确性，需要对生产环境进行调研。在搭建测试环境时，尽量保证搭建的测试环境和生成环境保持一致（环境主体框架相同，服务器硬件配置相近，数据库数据相近等）。 另外，最好输出一个测试环境搭建方案，召集各方参加评审确认。同时，在测试方案、测试报告中，对测试环境进行必要的阐述。 1.2 并发量计算及场景设计 首先，在确定场景及并发量之前，需要对业务进行调研，调研的对象最好是业务部门，也可以通过数据库中心查询数据，进行辅助。 场景选取一般包括：登陆场景、操作频繁的核心业务场景、涉及重要信息（如：资金等）业务场景、有提出明确测试需求的业务场景、组合场景等。 每个场景的并发量，需要根据业务调研的结果进行计算。可以采用并发量计算公式：C=nL / T 进行计算（其中C是平均的并发用户数，n是平均每天访问用户数，L是一天内用户从登录到退出的平均时间（操作平均时间），T是考察时间长度（一天内多长时间有用户使用系统））。 每个场景的思考时间，也可以通过业务调研获得。 另外，也可以采用模拟生产业务场景TPS（每秒通过事务数）的方式，来确定场景。相比上一种方式，模拟生产业务场景TPS，能更加准确模拟生产压力。本次ERP性能测试采用的就是这种方式：首先，通过调研确定业务高峰时段，各核心业务TPS量及产生业务单据量。然后，通过调整组合场景中，各单场景的Vusr（虚拟用户数）和Thinktime（思考时间），使每个场景的TPS接近业务调研所得到的TPS量,每个场景相同时间（即高峰时间段长度）通过事务数接近调研业务单据量，从而确定一个，可以模拟生成环境压力的基准场景。最后，通 综合排名： 综合排名比得主要是综合医院，专科医院就不参与了，这当中也包括三甲中医院，因为现在三甲中医院也是科室齐全，只不过多了个“中”字而已 1，复旦大学附属上海华山医院 上海人心中的永远的金字招牌，无论关于上海哪家医院排第一的理论到底有多多，最起码，华山医院这上海第一在上海人心中是肯定的！再看，《2007年全国医院排名》华山医院全国第三，上海第一；2009年全年门急诊量279万，全国第二，仅次于解放军总医院的300万；2009年出院人数4.7万，少于瑞金医院的5.5万，上海第二，综上，华山医院上海第一无可厚非。中国科学院院士一人，中国工程院院士两人，上海第一家接受JCI评审的综合医院，10个国家重点科室上海第一，全国仅次于协和医院......华山医院上海第一，想必应该如此2，上海交大附属瑞金医院 《2007年全国排名》全国第五，上海第二，2009年全员出院人次上海第一，中国科学院院士人，中国工程院院士2人，瑞金的实力无需多说，和华山不相上下。 3，复旦大学附属上海中山医院 虽然《2007年全国医院排名》把仁济医院排在全国第八，上海第三，但拥有中国科学院院士，工程院院士各1人，还有那么多重点专科的中山医院......够了，不多说。 争议就从第四名开始了 以下都是我个人意见： 4，上海交大附属仁济医院 5，第二军医大附属长海医院 6，上海交大附属新华医院 7，第二军医大附属长征医院 8，上海中医药大学附属曙光医院 9，上海中医药大学附属龙华医院 10，同济大学附属上海同济医院 分科排名（分科排名就不列举前10了，有名的我就写上，也算是指导大家去上海就医的选择吧） 内科： 神经内科：1，复旦大学附属上海华山医院；2，复旦大学附属上海中山医院；3，复旦大学附属儿科医院 心内科：1，复旦大学附属上海中山医院；2，复旦大学附属上海新华医院；3，复旦大学附属上海华山医院 消化内科：1，上海交大附属仁济医院；2，复旦大学附属上海中山医院；3，上海交大附属瑞金医院 呼吸内科：1，上海交大附属新华医院；2，第二军医大附属长海医院；3，同济大学附属上海同济医院 内分泌科：1，上海交大附属瑞金医院；2，上海交大附属仁济医院；3，同济大学附属上海同济医院 C/S测试 通常，客户/ 服务器软件测试发生在三个不同的层次： 1.个体的客户端应用以“ 分离的” 模式被测试——不考虑服务器和底层网络的运行； 2.客户端软件和关联的服务器端应用被一起测试，但网络运行不被明显的考虑； 3.完整的 C/S 体系结构，包括网络运行和性能，被测试。 下面的测试方法是 C/S 应用中经常用到的： 应用功能测试客户端应用被独立地执行，以揭示在其运行中的错误。 服务器测试——测试服务器的协调和数据管理功能，也考虑服务器性能（整体反映时间和数据吞吐量）。 数据库测试——测试服务器存储的数据的精确性和完整性，检查客户端应用提交的事务，以保证数据被正确地存储、更新和检索。 事务测试——创建一系列的测试以保证每类事务被按照需求处理。测试着重于处理的正确性，也关注性能问题。 网络通信测试——这些测试验证网络节点间的通信正常地发生，并且消息传递、事务和相关的网络交通无错的发生。 C/S结构与B/S结构的特点分析 为了区别于传统的C/S模式，才特意将其称为B/S模式。认识到这些结构的特征，对于系统的选型而言是很关键的。 1、系统的性能 在系统的性能方面，B/S占有优势的是其异地浏览和信息采集的灵活性。任何时间、任何地点、任何系统，只要可以使用浏览器上网，就可以使用B/S系统的终端。 不过，采用B/S结构，客户端只能完成浏览、查询、数据输入等简单功能，绝大部分工作由服务器承担，这使得服务器的负担很重。采用C/S结构时，客户端和服务器端都能够处理任务，这虽然对客户机的要求较高，但因此可以减轻服务器的压力。而且，由于客户端使用浏览器，使得网上发布的信息必须是以HTML 格式为主，其它格式文件多半是以附件的形式存放。而HTML格式文件（也就是Web页面）不便于编辑修改，给文件管理带来了许多不便。 1. 作用 家具性能测试是一种加速使用的疲劳和强度承受能力的测试方法，可以用来评估产品能否达到预期的设计要求。 2.GSA沙发性能测试 2.1 测试方法 GSA性能测试基于循环递增加载模式（图1）。测试开始时先给沙发加一个起始载荷，这个载荷以20次/分的频率循环加力25000/次。循环结束后，载荷增加一定量，然后再循环25000次。当载荷达到所需求的水平，或沙发框架或部件破环时测试才结束。 2.2测度设备 GSA沙发性能测试是在一套特别设计的汽缸-管道支架系统上进行的（如照片所示）。气缸在压缩空气机的推动下，以20次/分的循环频率对被测沙发加载。加载循环次数是由一个可编程逻辑控制器和可重置电子记数系统进行记录的。当沙发框架或部件破坏时，限制开关被激活并停止测试。 2.3主要的测试类型 图2所示是沙发的基本框架图，沙发框架可以分成3个部分：坐基框架系统、侧边扶手框架系统和后靠框架系统。根据沙发通常的受力状态，可以进行以下几种测试： 3 测试数据的讨论 3.1垂直坐力测试（seat foundation load test）（图3）， 在垂直坐力作用下，主要的座位支撑框架部位承受很大的应力，如果其中任何一个部件破坏，整个沙发也就很快破坏了。 前横档和后横档破坏的主要原因是其尺寸大小，不过实木横档上有太多交叉纹理和太大太多的节疤刀会引起横档破坏。横档底部的节疤破坏性最大，因为这里所受的拉应力最大，如果支撑框架部件主要是由木榫钉为主要连接件，横档破坏常常起于横档上用于连接座位撑档的榫钉孔处，然后扩大到整个横档截面上。另外在测试中，前横档和前支柱的接头也经常是破坏发生的地方，既有在垂直面的破坏，也有前后方向的破坏。这些破坏的接头大多是由于没有加用涂胶支撑木块来加强连接，而 品质体系框架图 1 品质体系框架图 图中各缩写词含义如下： QC：Quality Control 品质控制 QA：Quality Assurance 品质保证 QE：Quality Engineering 品质工程 IQC：Incoming Quality Control 来料品质控制 LQC：Line Quality Control 生产线品质控制IPQC：In Process Quality Control 制程品质控制FQC：Final Quality Control 最终品质控制 SQA：Source (Supplier) Quality Assurance 供应商品质控制DCC：Document Control Center 文控中心 PQA：Process Quality Assurance 制程品质保证FQA：Final Quality Assurance 最终品质保证 DAS：Defects Analysis System 缺陷分析系统 FA：Failure Analysis 坏品分析 CPI：Continuous Process Improvement 连续工序改进 CS： Customer Service 客户服务 TRAINNING：培训 一供应商品质保证（SQA） 1.SQA概念 SQA即供应商品质保证，识经过在供应商处设立专人进行抽样检验，并定期对供应商进行审核、评价而从最源头实施品质保证的一种方法。是以预防为主思想的体现。 2.SQA组织结构 3.主要职责 1）对从来料品质控制（IQC）/生产及其它渠道所获取的信息进行分析、综合，把结果反馈给供应商，并要求改进。 2）耕具派驻检验远提供的品质情报对供应商品质进行跟踪。 3）定期对供应商进行审核，及时发现品质隐患。 品质体系的一般架构 图中各缩写词含义如下： QC：Quality Control 品质控制 QA：Quality Assurance 品质保证 QE：Quality Engineering 品质工程IQC：Incoming Quality Control 来料品质控制LQC：Line Quality Control 生产线品质控制IPQC：In Process Quality Control 制程品质控制FQC：Final Quality Control 最终品质控制SQA：Source (Supplier) Quality Assurance 供应商品质控制DCC：Document Control Center 文控中心PQA：Process Quality Assurance 制程品质保证FQA：Final Quality Assurance 最终品质保证DAS：Defects Analysis System 缺陷分析系统FA：Failure Analysis 坏品分析CPI：Continuous Process Improvement 连续工序改善CS：Customer Service 客户服务TRAINNING：培训 一供应商品质保证（SQA） 1.SQA概念 SQA即供应商品质保证，识通过在供应商处设立专人进行抽样检验，并定期对供应商进行审核、评价而从最源头实施品质保证的一种方法。是以预防为主思想的体现。 2.SQA组织结构 3.主要职责 1）对从来料品质控制（IQC）/生产及其他渠道所获取的信息进行分析、综合，把结果反馈给供应商，并要求改善。 2）耕具派驻检验远提供的品质情报对供应商品质进行跟踪。 3）定期对供应商进行审核，及时发现品质隐患。 4）根据实际不定期给供应商导入先进的品质管理手法及检验手段，推动其品质保证能力的提升。 5）根据公司的生产反馈情况、派驻人员检验结果、对投宿反应速度及态度对供应商进行排序，为公司对供应商的取舍提供依据。 4.供应商品质管理的主要办法 1）派驻检验员 把IQC移至供应商，使得及早发现问题，便于供应商及时返工，降低供应商的品质成本，便于本公司快速反应，对本公司的品质保证有利。同时可以根据本公司的实际使用情况及IQC的检验情况，专门严加检查问题项目，针对性强。 2）定期审核 通过组织各方面的专家对供应商进行审核，有利于全面把握供应商的综合能力，及时发现薄弱环节并要求改善，从而从体系上保证供货品质定期排序，此结果亦为供应商进行排序提供依据。 一般审核项目包含以下几个方面 A．品质。 B．生产支持。 C．技术能力及新产品导入。 上海交通大学医学院附属瑞金医院医（技）师“三基”培训和考核管理办法 （讨论稿） 为加强临床一线医（技）师的“三基”能力，切实提高医疗内涵质量，确保医疗安全，按照《医师定期考核管理办法》相关规定，结合我院的实际情况，特制定如下“三基”培训和考核管理办法。 一、培训和考核目的： 1.规范临床医（技）师的基本操作流程 2.强化临床医（技）师的基本操作技能 3.提高临床医师的基本理论和基础知识 二、培训和考核对象： 注册在瑞金医院的执业医师和执业助理医师（包括住院医师、主治医师、副主任医师和晋升主任医师职称三年内的主任医师）、辅助科室的医技人员 三、培训形式： 1、以网络自学和医院集中辅导相结合的方式，每人每年必须修满规定学分（标 准详见考核内容），学分获取情况记入个人医疗档案，作为“三基”考核的内容之一，直接与医师年度绩效考核挂钩。 2、网络自学采用考核得分制，每门课程自学后通过测试方可获得0.5学分； 3、集中辅导采用学分制，每次参加培训即可获得0.5学分（迟到或早退30分钟 以上者不计分）。 4、医技人员的培训以科室自行组织培训为主，医院集中培训为辅，每次参加科 室培训即可获得0.25学分，学习情况由科主任审核盖章确认。 四、培训内容： 1、临床基本技能：全身体格检查、胸穿、腹穿、深静脉穿刺、心电图阅读、影 像片阅读、呼吸机使用、徒手心肺复苏 2、临床基本理论和基础知识：各专业的临床诊疗常规、抗生素合理使用规范、 合理用血指征 3、卫生相关法律法规：《医疗事故处理条例》、《病史书写规范》、《中华人 民共和国传染病防治法》、《医师外出会诊管理暂行规定》、《医师定期考核管理办法》、《处方管理办法》、《麻醉药品和精神药品管理条例》、《医院感染管理办法》、《医疗废物管理条例》 4、医院规章制度：39条医疗管理制度 5、医技人员的专业知识和技能培训以本专业为主。 五、培训和考核周期： 临床医师的集中理论培训每年举办40次，技能培训不定期举办，以医务处的实际安排为准。 考核一年为一个周期，具体时间安排如下： 3——4月份卫生法律、法规、规章制度、临床诊疗常规和专业知识考核5月份 卫生法律、法规、规章制度、临床诊疗常规和专业知识考 核补考 7——8月份临床技能考核 9月份临床技能考核补考 11月份学分考核 六、考核方式： 1、临床各级医师采取有关法律、法规、规章制度、专业知识的书面考核、技术 操作考核、学分考核相结合的形式。 2、辅助科室医（技）师采取本专业专业知识的书面考核和技能操作、心肺复苏 考核相结合的形式。 3、由各科室协助医务处共同组建考核题库，书面及技能操作考核全部由医务处 统一组织。 七、考核内容： 临床住院医师： 1. C S/C SS系统架构的基本概念 1.1系统架构定义 虽然B/S结构、J2EE架构愈来愈成为流行模式，但基于传统的C/S结构的应用程序还广泛地应用于各种行业。尤其是金融行业中的商业银行柜面－核心帐务系统等。一方面由于传统商业银行一般都有大量的字符终端等需要复用的设备，一方面也是因为他们存在大量密集的对实时性要求很高的高柜业务，使用传统的基于C/S结构或者C/S/S结构的应用效率更有保证。 C/S结构即CLIENT/SERVER结构。传统的C/S结构一般分为两层：客户端和服务器端。该结构的基本工作原理是，客户程序向数据服务器发送SQL请求，服务器返回数据和结果。客户端负责实现用户接口功能，同时封装了部分应用逻辑。服务器端的数据库服务器主要提供数据存储功能，也通过触发器和存储过程提供部分应用逻辑。 C/S/S结构即客户/应用服务器/数据库服务器三层结构，中间增加了应用服务器，通常实现应用逻辑，是连接客户与数据库服务器的桥梁。它响应用户发来的请求执行某种业务任务，并与数据库服务器打交道，技术实现上通常选用中间件产品，如BEA公司的TUXEDO （事实上J2EE架构的应用也属于这种三层或多层结构，这里不包括。）和IBM公司的CICS等。 三层或多层C/S结构与两层C/S结构相比，它的优势主要表现在：安全性加强、效率提高、易于维护、可伸缩性、可共享性、开放性好等。 1.2系统架构示意图 1.3CS/CSS系统架构中性能测试的特点 1.3.1CS/CSS系统架构的性能影响因素 由于CS/CSS系统的以下特性，测试工程师对一个CS/CSS系统实施性能测试具有很大的难度： *整个系统的各个部分使用多种操作系统，性能上有差别； *整个系统架构的各个环节上使用多种数据库，同样在性能上有差别； *应用是多个，分属多个种类，分布在不同设备上，包括自行开发的应用、第三方的应用； *系统中的设备、组件通过不同协议进行连接、通讯； *系统的内部接口多，性能瓶颈多；而系统的整体性能往往取决于最差的部分；需要分别测试和联合测试 *系统的性能指标不光同应用系统架构有关，还和具体行业应用的业务模式有关； *采用此架构的行业应用往往是一个7×24小时系统； *采用此架构的行业应用可能高柜业务多，这样会影响对性能度量项的选取和转换； *各个环节基本上以交换数据报文的方式通信，其格式经常会比较复杂。 因此这样的系统对于对测试工程师的知识的深度和广度都是一个考验。对于这样的系统，到底如何使用什么样的测试策略、如何分析测试需求、如何选取性能度量项的转换计算模型、如何确定测试内容和轮次、如何设计性能测试案例等等以及规划和实施性能测试中的其它诸多问题，都需要遵循一个系统的方法来解决。 1.3.2CS/CSS系统架构中性能测试的基本策略 1. 确定好测试工作范围 首先可以分析压力测试中最容易出现瓶颈的地方，从而有目的地调整测试策略或测试环境，使压力测试结果真实地反映出软件的性能。例如，服务器的硬件限制、数据库的访问性能设置等常常会成为制约软件性能的重要因素，但这些因素显然不是用户最关心的，我们在测试之前就要通过一些设置把这些因素的影响调至最低。 另外，用户更关心整个系统中哪个环节的性能情况也会影响工作范围。如有的环节是全 电子科技大学二零零 六 至二零零 七 学年第 二 学期期 末 考试 离散数学 课程考试题 B 卷 （ 120 分钟） 考试形式： 闭卷 考试日期 200 年 月 日 一、单选题（四选一）（10×1＝10分） 1. 如果命题公式G=P ∧Q ，则下列之一哪一个成立（2 ）。 1).G=?(P →Q) 2).G=?(P →?Q) 3).G=?(?P →Q) 4).G=?(?P →?Q) 2. 设Φ是一个空集，则下列之一哪一个不成立（1 ）。 1).Φ∈Φ 2).Φ?Φ 3).Φ∈{Φ} 4).Φ?{Φ} 3. 谓词逻辑的推理中，)()()(x G x x G ??使用的是规则（ 3 ）。 1). ES 2).US 3).UG 4).EG 4. 在集合｛0，1｝上可定义（ 2 ）个不同的二元运算。 1).2 2).4 3).8 4).16 5. 设集合A ＝{a,b,c}，A 上的二元关系R ＝{ 品质体系的一般架构 图中各缩写词含义如下: QC : Quality Con trol 品质控制QA : Quality Assura nee 品质保证QE : Quality Engin eeri ng 品质工程 IQC : Incoming Quality Con trol 来料品质控制 LQC :Line Quality Control 生产线品质控制IPQC :In Process Quality Control 制程品质控制FQC Fi nal Quality Co ntrol 最终品质控制SQA :Source (Supplier) Quality Assura nee 供应商品质控制DCC :Docume nt Con trol Cen ter 文控中心 PQA :Process Quality Assura nee 制程品质保证FQA :Final Quality Assura nee 最终品质保证DAS :Defects An alysis System 缺陷分析系统FA : Failure An alysis 坏品分析 CPI : Con ti nu ous Process Improveme nt 连续工序改善 CS : Customer Service 客户服务TRAINNING : 培训 一供应商品质保证(SQA) 1. SQA概念 SQA即供应商品质保证，识通过在供应商处设立专人进行抽样检验，并定期对供应商进行审核、评价而从最源头实施品质保证的一种方法。是以预防为主思想的体现。 2. SQA组织结构 3. 主要职责 1) 对从来料品质控制(IQC) /生产及其他渠道所获取的信息进行分析、综合，把结果反馈给 供应商，并要求改善。 2) 耕具派驻检验远提供的品质情报对供应商品质进行跟踪。 3) 定期对供应商进行审核，及时发现品质隐患。 4) 根据实际不定期给供应商导入先进的品质管理手法及检验手段，推动其品质保证能力的 提升。 5) 根据公司的生产反馈情况、派驻人员检验结果、对投宿反应速度及态度对供应商进行排 序，为公司对供应商的取舍提供依据。 4. 供应商品质管理的主要办法 1) 派驻检验员 把IQC移至供应商，使得及早发现问题，便于供应商及时返工，降低供应商的品质成本，便于本公司快速反应，对本公司的品质保证有利。同时可以根据本公司的实际使用情况及IQC的检验情况，专门严加检查问题项目，针对性强。 2) 定期审核 通过组织各方面的专家对供应商进行审核，有利于全面把握供应商的综合能力，及时发现薄弱环节并要求改善，从而从体系上保证供货品质定期排序，此结果亦为供应商进行排序提供依据。 一般审核项目包含以下几个方面 A. 品质。 B. 生产支持。 C. 技术能力及新产品导入。 般事务? 具体内容请看“供应商调查确认表”Web性能测试方案
上海交通大学医学院附属瑞金医院放射科简介
品质体系框架图.
天线分集技术的原理
性能测试流程规范
慕课 离散数学 电子科技大学 课后习题十 答案
上海交通大学医学院附属瑞金医院北院
浅析发射分集与接收分集技术
金蝶ERP性能测试经验分享
上海各大医院排名及专治各科
CS架构性能测试
沙发性能测试
品质体系框架图
品质体系的一般架构
上海交通大学医学院附属瑞金医院医(技)师
CS和CSS架构的软件性能测试分析
电子科技大学2006-2007年《离散数学》期末考试B卷
品质体系的一般架构