Process algebra needs proof methodology, The Concurrency Column

Process algebra needs proof methodology

Wan Fokkink2,3,Jan Friso Groote1,2,Michel Reniers2 1Dep.of Mathematics and Computer Science,Eindhoven University of Technology,

P.O.Box513,5600MB Eindhoven,The Netherlands

2CWI,Cluster of Software Engineering,

P.O.Box94079,1090GB Amsterdam,The Netherlands

3Vrije Universiteit Amsterdam,Department of Theoretical Computer Science,

De Boelelaan1081a,1081HV Amsterdam,The Netherlands

Email:Wan.Fokkink@cwi.nl,{J.F.Groote,M.A.Reniers}@tue.nl

Abstract

This note contains the contribution to the Concurrency Column of the EATCS

Bulletin of February,2004.It indicates on the one hand what the strengths of

process algebras are,and on the other hand mentions a major https://www.docsj.com/doc/0710358657.html,ing

elementary process algebra it is hard to prove correctness of complex distributed

algorithms,protocols and systems.We encountered this when providing a process

algebraic proof that the sliding window protocol of bu?er size n is behaviourally

equivalent to a bounded queue of size2n.We used and developed notions such

as invariants,cones and foci and coordinate transformations together providing

the means to give a precise and insightful proof of the correctness of the sliding

window protocol.These and other techniques are all shortly addressed in this

note.The main message however is that in order to make process algebra the

universal tool for the study of correct system behaviour(for which we believe it

is one of the best candidates)much more of e?ective proof techniques need to be

developed.

Why is process algebra exciting?

An early paper by Milner in1973[41]gave a clear motivation for process algebra.He gave three reasons to design a process algebra.

?All(computer)systems interact with their environment.For most of these,this is their primary‘raison d’?e tre’.So,within computer science,we need a formalism in which interaction is a primary citizen.

?Nondeterminism is important.The actual behaviour of a computer system is in?uenced by factors that we do not understand or are too complex to include in

a comprehensive description.For instance the exact moments at which interrupts

1

2 occur in a computer can have substantial in?uence on its overall behaviour.Yet, incorporating these moments would quickly make the study of any non-trivial behaviour in the system untenable.Nondeterminism provides a way to manage this complexity.We simply describe nondeterministically that interrupts can occur at any https://www.docsj.com/doc/0710358657.html,ner uses the‘weather’that can in?uence the behaviour of computers and that we cannot completely describe and understand.

?Parallelism is an omnipresent notion in computers.

Especially,the?rst two aspects are missing in many foundational formalisms,in par-ticular in those from the70’ies of the last century.

Based upon these motivations,Milner developed CCS[42],a simple and very elegant theory for communicating systems.Very similar theories were developed by other researchers among which CSP[34]and ACP[5].As we grew up in the realm of ACP, we use it in the rest of this note,but all that is being said applies to all process theories in general.

Another new key notion in process algebra is the internal actionτ(which we also attribute to Milner[42],although we do not know whether this is its true origin). The idea is that the exact nature of most actions that occur in a computer system is irrelevant.Hence,these actions can be made invisible by declaring them hidden.In other words,these actions are renamed toτ’https://www.docsj.com/doc/0710358657.html,ing appropriate reduction relations, e.g.weak-[42,45]or branching bisimulation[21],the residual visible behaviour can be made small and insightful.

Note that besides process algebras,there are more formalisms that allow interaction, nondeterminism and abstraction,such as Petri-nets[46]and I/O-automata[38].But to our taste,none of these formalisms integrate all these aspects so nicely as process algebra.

The limits of classical process algebra

The axiomatic theories of CCS,ACP and CSP led to typical and elegant correctness proofs of intricate communicating systems.Examples are for instance Milner’s sched-uler and the alternating bit protocol(see e.g.[3,42]).

Unfortunately,these examples turned out to be the limit of what could be proven correct using manipulation by means of the axioms directly.Around1990,it became obvious that the applicability of process algebra in its original form for practical pur-poses was limited.

Obviously,if process algebra could not be e?ectively applied to much more complex systems,there should be only one reasonable destiny for all the work done on it:the shelves of our national libraries.But,given the elegance and simplicity of its elementary theory,we could not accept this fate.

So,in1990the challenge was(and for the larger part still is):

3 Can we develop process algebra such that it can be used e?ectively to design

the correct behaviour of realistic interacting programs and systems?

The?rst derived question,namely whether we can describe realistic,interacting sys-tems,had already been answered a?rmatively by in particular LOTOS[36]and sub-sequently by other formalisms such as PSF[40].In these languages the expressiveness of process algebra is enhanced with data types and some syntactic sugaring.

One of the striking conclusions was that specifying interacting systems using these formalisms really improved quality and clarity,compared to the standard verbose and verbal speci?cations,that unfortunately are still very commonly in use.But after initial enthusiasm,it turned out that especially the larger speci?cations did contain mistakes similar to the typical mistakes in programs.A speci?cation formalism by itself does not guarantee correctness.

This made it obvious that ways were needed to ascertain the correctness of such speci?cations.

Why are state based techniques not the only answer A major movement to provide the means to establish the correctness of speci?cations originates in state space exploration.The basic idea is that a system speci?cation is transformed into an automaton or state space.By explicit exploration of this state space,properties,such as deadlock freedom,can be https://www.docsj.com/doc/0710358657.html,ing property lan-guages such as the modal mu-calculus[10],much more advanced properties can be formulated.

Using spectacular techniques,such as Binary Decision Diagrams[12],partial order reduction[23],bit-hashing[35],supported by the even more spectacular increase of the speed of computers and the use of networks of computers it is now possible to e?ectively and automatically prove many properties about the behavioural speci?ca-tions of destitute interacting systems.This is actually leading to modeling as a new paradigm in computer science,which is common in most other engineering disciplines. This means that the essential behaviours of programmed systems are being modeled and that insight is primarily obtained by studying the behaviour of the model. Unfortunately,many realistic systems and their models exhibit behaviours that lead to state spaces too large and too complex to deal with using any of the methods above. And although we often wanted to believe di?erently,most of the real world examples to which we want to apply our techniques,are way out of reach.A typical example is a new railway safety control philosophy developed in the Netherlands[4]allowing a more e?cient and reliable railway transport.One of the reasons that it will not be taken into service is that nobody can convincingly certify its correct operation.Until this is possible,it seems that the Dutch railway companies will stick to the proven, simple control systems to which they are accustomed,denying customers the bene?ts of the new technology.

4 In those cases where automatic methods are insu?ciently helpful,manual manipu-lation can save the day.Typically,protocols and algorithms deal with unspeci?ed or unbounded data,are about an unbounded number of communicating partners and are often quite complex.In order to prove the correctness of such systems human ingenu-ity and intuition are indispensable.The ability to include the human intellect into the veri?cation e?ort will be a distinguishing success factor for many decades to come. This situation is similar to mathematics,where numerical techniques and automatic formula manipulation play increasingly important roles.But even in engineering math-ematics,manual veri?cation techniques,intuition,insight,experience and hard labour remain essential to solve problems.It however needs to be said that the combination of manual and automated techniques have advanced this?eld as a whole.

Within computer science the situation is similar.So,besides automated techniques, it is essential to further the?eld of manual veri?cation,far beyond the level of Milner’s Scheduler or the alternating bit protocol.

The sliding window protocol

In1990we were ready to undertake this challenge.But?rst we needed a tractable speci?cation language without any form of syntactic sugar but still su?ciently strong to model complex interacting systems.So,we needed a formalism more advanced than bare process algebra,but not as syntactically rich as LOTOS and PSF.We designed the languageμCRL(micro Common Representation Language)[26]consisting of ACP, abstract equational data types and two new operators(the if-then-else and the sum over(in?nite)data types)to glue data and processes together.

Figure1:Sliding window protocol

After this,we embarked upon the question whether we could prove the correctness of the most complex sliding window protocol in Tanenbaum’s Computer Networks [50,Second edition]solely on the basis of the axioms and rules of process algebra. The structure of the sliding window protocol is drawn in?gure1.The basic idea

5 behind the protocol is that data must be sent from A to D.We only consider the unidirectional variant here.In the bidirectional variant data is sent from D to A also. The data is stored in a bu?er in S and is subsequently sent via the channel K to the receiver R.The receiver R sends acknowledgements back to S via channel L.While in transit,data and acknowledgements can get lost.Therefore,sender S regularly resends its data,as long has it has not been acknowledged and receiver R retransmits acknowledgements periodically.Only if data has been acknowledged,the sender S removes it from its bu?er.A typical feature of the sliding window protocol is that the messages are numbered.By looking at these numbers and by bu?ering the messages, receiver R can deliver the data in the same order as they were read by S.It turns out that the protocol works correctly by numbering the messages modulo2n if both bu?ers have size n.

Algebraically proving the correctness of the sliding window protocol appeared to be much harder than expected,and has only recently been?nished[19].There have been a number of failed attempts to prove the sliding window protocol correct within the process algebraic community.There are some attempts where the nature of the protocol has been substantially adapted[25,44,47].Furthermore,there are a number of proofs of simpli?ed sliding window protocols,with only a single bu?er place[7,52,53]or where modulo calculation does not essentially play a role[15].We consider the fact that we managed to give a process algebraic proof of the full sliding window protocol with arbitrary bu?er size n and packet numbering modulo2n(and had the proof checked using PVS[43])a substantial step forward.More importantly,we identi?ed several essential techniques that make the proof rather straightforward.

Using assertional techniques a number of successful proofs of the sliding window pro-tocol have been given[13,48,49].Especially,the proof of Anneke Schoone gave us the essential inspiration for a technique which we call‘coordinate transformations’.Typical for the assertional proofs are the limited correctness properties that can be shown.For the sliding window protocol correctness is formulated as:the list of delivered data of the sliding window protocol matches the list of input data.Within process algebra the more insightful theorem is proven that the behaviour of the sliding window protocol with window size n is branching bisimilar to that of a queue with bu?er size2n. Very early on we made two observations about the third sliding window protocol of Tanenbaum.The?rst was that the external behaviour of the protocol as stated in Tanenbaum is extremely complex.So,we had to make slight adaptations to guarantee that the protocol nicely behaved like a bounded queue.The second observation was that the protocol contained a deadlock,which we had to repair.

In the remainder of this note we?rst shortly introduce the languageμCRL and sub-sequently address the techniques that we have identi?ed as important to algebraically prove the correctness of interacting systems.

6 A short primer inμCRL

We want to avoid formulas,and we mainly provide main ideas.Readers that want more are referred to for instance[19,27]or even the draft of a planned book on these techniques[28].Yet,it might be useful,to brie?y sketch the languageμCRL,which has provided the context for our work.

Processes have the following syntax:

p::=a(d1,...,d n)|τ|δ|p+p|p·p|p p|τI(p)|?H(p)|

p|p c p.

d:D

The process a(d1,...,d n)is an action,parameterized with data elements.The process τis the internal action,i.e.an action that cannot be directly observed.The process δis inaction or deadlock,i.e.the process that cannot perform any behaviour.The operator+denotes the choice between two processes,and the operator·is sequential composition.The sequential composition operator is often omitted.Parallel composi-tion is denoted by .Actions can be hidden using the hiding operatorτI where I is a set of action labels of the actions that are to be renamed toτ.The encapsulation operator?H blocks all actions whose labels are in the set H.All these operators are standard operators of ACP[3].

The operators that integrate data and processes are the sum operator d:D p that represents the possibly in?nite choice of process p over all data elements in D.The process p c p denotes the then-if-else construct.If the condition c is true,the process at the left is executed,otherwise the process at the right-hand side is performed.The languageμCRL also contains the operators

7 The advantage of abstract data types is their simplicity and genericity.By employing these a fast and memory e?cient toolset forμCRL has been built[9].A disadvantage of abstract data types is the need to rede?ne the basic types for every speci?cation, and the inability to use domain speci?c technologies,such as for instance integer linear programming.

The languageμCRL has been kept simple.All operators and keywords of the lan-guage are given above,except for the keyword init used to indicate the initial state of a process.

Linear processes

Both for manual veri?cation and for tools it turned out to be extremely fruitful to transform all processes to linear form,which in essence is an equation of the form

X( d: D)=

i∈I

e i: E i

a i(f i( d, e i))X(g i( d, e i)) c i( d, e i) δ

It says that process X with parameters d can for each i∈I(I is a?nite index set) choose to perform action a i with parameters f i( d, e i)ending up in process X with parameters determined by the function g i,provided condition c i holds.In case a process cannot perform an in?nite number ofτ-actions,it is calledτ-convergent,or convergent for short.

It is possible to automatically transform any guarded process description to linear form[51].This includes parallel processes.One of the largest advantages of linear processes is that they do not su?er from the state space explosion problem.Process descriptions of hundreds of pages have been transformed to linear form.Note that linear processes are a common normal form for processes,cf.for instance I/O-automata and the Unity language[14].

Axioms and rules

Milner[42]provided a concise set of axioms to deal with processes.Nice rules to deal with in?nite behaviour were provided by Bergstra and Klop,namely,the recursive speci?cation principle and Koomen’s fair abstraction rule(see e.g.[3]).These axioms and rules give a complete underpinning of process algebra.

The recursive speci?cation principle formulated for convergent linear processes equa-tion(CL-RSP)says that every convergent linear process has one solution within the context of branching bisimulation.So,each such linear process exactly de?nes a pro-cess,and moreover,if we can show another process to be a solution of a linear process equation,it must be branching bisimilar to the standard solution of the linear equation.

8 Koomen’s fair abstraction rule says that everyτ-loop can be removed from a process. It expresses fairness by saying that if in aτ-loop certain actions are iteratively enabled, then one of them must eventually be executed.

As stated before,these elementary rules are too cumbersome to prove complex dis-tributed systems correct.In the next?ve sections we provide techniques to overcome this.

Invariants

Remarkably,classic process algebra does not include the notion of an invariant,whereas it is one of the most important concepts in assertional correctness proving.In[6]the notion of an invariant for linear process equations has been introduced.It is a simple predicate that remains true when actions are performed.Formulated in terms of a linear process we say that I is an invariant if for all d,i∈I and e i it holds that

I( d)∧c i( d, e i)→I(g i( d, e i)).

This is generally easy to check.A process starting in a state where the invariant holds can be simpli?ed using the invariant.

It turned out that invariants are essential when proving realistic systems correct.But much more is needed.

Cones and foci

A method that has been totally inspired by the correctness proof of the sliding window protocol is the cones and foci technique[30].The core di?culty of showing that the sliding window protocol simulates a bidirectional queue lies in the fact that if the queue would perform an action,then the sliding window could only mimic this by?rst doing a large number of internal steps.

After studying this situation,a rather general pattern emerged in the behaviour of implementations.This can be seen in?gure2.The implementation is generally performing many internal actions to achieve some goal,for instance the delivery of data.This behaviour can be drawn as a cone shaped as a set of states with a single state at the focus of the cone.This focus point is where the implementation strives after.All the states in such a cone are bisimilar to a single state in the speci?cation describing the external behaviour of the implementation.An implementation consists of a large number of such cones.

At the focus point,the implementation and the speci?cation can exhibit exactly the same behaviour.But the implementation can already perform external actions,when not at the focus point.E.g.the implementation can already deliver a datum when it still needs to acknowledge it.

9

External actions

F

Progressing internal actions

c

d c d

d

d

a b a

b b

b c a Figure 2:A focus point and its cone

Given the fact that implementations contain cones,there is an easy way to prove the implementation and speci?cation weak-or branching bisimilar by providing a state mapping h from the states of an implementation to the states of a speci?cation and by checking the following six properties that can simply be formulated on linear processes:

1.There is no in?nite sequence of τ-steps.This property can be relaxed by requiring splitting the τ-transitions in progressing and non progressing τ-transitions,and by requiring that there is no in?nite sequence of progressing τ’s.

2.The states s and s before and after a τ-step,are mapped to the same state in the speci?cation by the state mapping,i.e.h (s )=h (s ).

3.Each external action that can be done in a state s in the implementation can also be performed in the related state h (s )in the speci?cation.

4.For each state s that is a focus point,each action that can be performed in h (s )can also be done in s .

5.Data in related actions in s and h (s )must match.

6.The states reached when performing related actions in s and h (s )must be related by h again.

The strength of this technique comes particularly from 4.It is not necessary to check that each action in the speci?cation can be performed in any state in the implementa-tion.It is only necessary to see that such actions can be mimicked in the focus point.The ?rst condition seems particularly restrictive,but it has been relaxed in [20,30].

10

There are several generalizations of the cones and foci theorem[20,22].The e?ec-tiveness of the cones and foci theorem is such that there is now a long list of correctness proofs where this theorem plays a pivotal role.

Coordinate transformations

Unfortunately,the cones and foci theorem turned out to be insu?cient to prove the correctness of the sliding window protocol.Inspired by the work of Anneke Schoone [48],we split the proof in two parts.First we showed that the sliding window protocol with unbounded sequence numbers behaved correctly using the cones and foci method. Then,we showed that this unbounded sliding window protocol behaved the same as the ‘modulo’sliding window protocol by a simple application of the recursive speci?cation principle.In a sense we went from a non modulo to a modulo coordinate system. There is a strong resemblance with mathematics,where solving a problem in one coordinate system is much harder than in another coordinate system.Similarly,we believe this is also an essential technique in this?eld.

Using invariants,cones and foci and coordinate transformations,we were able to give a proof of the sliding window protocol.

Con?uence

Techniques that are totally unrelated to the sliding window protocol,but particularly e?ective,areτ-con?uence andτ-prioritisation[29].These techniques are related to partial order reduction but much less involved.In[42]a slightly di?erent notion of

a =τ

=τ

=a j

(g i(

d, e

i

), e j )=f j( d, e j)

equations

11 The notion ofτ-con?uence(although it comes in many?avours)is best illustrated in a picture(see?gure3).It says that if a process can perform an a and aτaction,it must be able to perform respectively aτand an a action to a joint state.If this holds for all states and transitions we call the transition systemτ-con?uent.

If a system isτ-con?uent and it is not possible to perform an in?nite sequence ofτ’s, theτ-prioritisation operation preserves branching bisimulation.Theτ-prioritisation operation simply does the following.In any state priority can be given to aτ-transition. This means that all other transitions(including otherτ-transitions)in this state are removed such that only the prioritizedτremains.

The use ofτ-con?uence on a given state space is generally less fruitful,as the state space has already been generated.Butτ-con?uence andτ-convergence can be estab-lished on a linear process.Subsequently,τ-prioritisation can be applied to reduce the state space,before it is generated.

In manual correctness proofs,τ-con?uence can be used to straighten the behaviour of a protocol,for instance by showing that the protocol can be considered as if it oper-ated in several rounds.Without proper foundation such assumptions have been made in the proofs of correctness of several distributed algorithms[16].When generating state spaces,applyingτ-con?uence andτ-prioritisation often reduces its size substan-tially.There are instances,where the size of the state space after reduction is only the logarithm of the original state space.

Unbounded parallel processes

Many distributed algorithms deal with an unbounded number of processes.If an individual process i can be described as P(i),the parallel composition of n+1such processes is straightforwardly described by the following equation:

X(n:Nat)=(P(n) X(n?1)) n>0 P(0).

It turns out to be non trivial to derive a linear process equation for X.A way to do this is by inductively adding a single process at the time.The problem is that the behaviour of a restricted number of such processes can be hard to comprehend.

We overcome this problem by a general meta theorem that gives the linear form of X and that moreover shows that if P is well de?ned,X also uniquely de?nes a process [31].

Modal logic

Where process algebra traditionally looks at equating speci?cation and implementa-tion,it is without doubt that establishing the validity of certain properties,neatly formulated using modal formulas,has become an essential means to formulate and establish correctness of systems.

12 On the one hand the veri?cation of modal formulas has up to now mainly been dominated by providing smart and fast algorithms to establish the validity of such formulas on state spaces.On the other hand a lot of energy went into the fundamental underpinning of the theory.However,relatively little attention has been paid to the development of a mathematical theory to e?ectively prove the validity of formulas manually.This means that no mathematical experience and subsequent methodology is building up.

Modal formulas must contain data to allow to formulate properties beyond the level that the system contains no deadlock.In[24]it has been pointed out how such enhanced formulas in combination with a linear process can be transformed to parameterized boolean equation systems.Following the line of the excellent thesis by Angelika Mader [39],where the theory for?xed point boolean equation systems is summarized and developed,we are working on extending this theory to solve such equations with data [32,33].

A typical phenomenon is that some of the equations that we obtain have no easy so-lutions,and require the investigation of patterns comparable to the patterns occurring in solving di?erential equations or integrals.We feel that much work needs to be done in this?eld.

Toolset

When interested in the speci?cation of correct realistic systems there is one unfortunate observation that one cannot escape.Speci?cations of realistic systems are large,easily extending dozens of pages.Obviously,only the most extraordinary people can muster the energy to prove properties about objects of this size.In order to also allow ordinary people to design correct systems,computer tools are required.

ForμCRL we have designed a tool primarily centered around the notion of a linear process.In this way we avoid the essential use of automata,which quickly become too large to be handled.As already remarked above,we have transformed large systems of literally hundreds of pages to linear form.

The linear process equation can be transformed and minimised.A simple optimi-sation is for instance the detection and elimination of parameters that always remain constant and that do not in?uence external behaviour.Besidesτ-prioritisation,the elimination of irrelevant parameters is the foremost tool to reduce the size of state spaces.More involved operations are checking and generation of invariants,establish-ingτ-con?uence and application ofτ-priorisation.Even modal formulas with data can be established on linear process equations where it is of no relevance whether the state space is?nite or in?nite.The only determining factor is the complexity of the property, the process and in particular the data types.

Currently,after optimising the linear process,we generally resort to the generation of a state transition system and use automata based algorithms for our?nal analysis.

13 For the generation of the state space several dedicated rewrite technologies have been introduced that allow to calculate with abstract data types almost as fast as with concrete data types.Memory consumption is extremely low by employing sharing o?ered by the ATerm library[11],leading to a memory consumption of a few bits per parameter in a state for large state spaces.And by employing networks of computers and dedicated algorithms,we can now generate state spaces of more than109states[8] and we expect that around the time this note appears in print it is regularly possible to generate state spaces of1010states.

The toolset is freely available via www.cwi.nl/~mcrl.

Open questions

Below we mention a few of the questions that we believe are important to be solved for the further development of this?eld and into which we already looked to a smaller or larger extent.Of course,the?eld is broad and therefore much more needs to be done than can possibly be mentioned here.

?Time,probabilities,stochastics and continuous behaviour are all encountered when studying systems.All of these notions have been addressed in many pa-pers,but none of them have a su?ciently simple and mathematically developed form that we know how to incorporate these in our setting.For instance the combination of continuous time,data and branching bisimulation still does not have a satisfying axiomatisation(despite[18,37,2]).

?Techniques such as the cones and foci method have been developed to prove branching bisimulation.Sometimes,one encounters speci?cations and implemen-tations for which equivalences weaker than branching bisimulation are needed.

One could think of trace equivalence,failure equivalence or simulation.Within the context of process algebra,no e?ective means have been developed.An inter-esting notion could be simulation as used in the context of I/O-automata.But the use of prophecy variables[1]appears to be even more interesting.

?Within distributed systems there are many impossibility results.It is impos-sible to reach consensus or common knowledge over asynchronous communica-tion channels.Within process algebra,or more generally within the world of behavioural automata there are no nice and general theories to systematically derive and understand these impossibility results.

?Besides process algebra and similar formalisms(such as I/O automata)there are a few rather di?erent formalisms around dealing with the same questions of behaviour and correctness.These are the world of assertional techniques(in-variant,weakest preconditions)and Petri-nets.Similar to process algebra,these formalisms have their unique strengths.It is however odd to see that all these

REFERENCES14 domains seem to operate in a rather isolated way,rather than to incorporate each

other’s techniques and to converge to a uni?ed theory of system behaviour.

For instance,within assertional theorem proving there is a strong but virtually forgotten?eld of the derivation of algorithms(see e.g.[17]).Based on concise descriptions of the desired e?ects extremely elegant algorithms have been derived in a very insightful way.Within process algebra such techniques do not exist.

In Petri-nets it is possible to describe distributed data processing e?ectively.

Moreover,it is possible to derive many behavioural properties from the static structure of a Petri-net.Within the context of process algebra similar structural reasoning is largely absent.

References

[1]M.Abadi and https://www.docsj.com/doc/0710358657.html,mport.The existence of re?nement mappings.Theoretical

Computer Science,82:253–284,1991.

[2]J.C.M.Baeten and C.A.Middelburg.Process Algebra with Timing.Monographs

in Theoretical Computer Science.Springer Verlag,2002.

[3]J.C.M.Baeten and W.P.Weijland.Process Algebra.Cambridge tracts in theoret-

ical computer science18,Cambridge University Press,1990.

[4]J.Berger,P.Middelraad and A.J.Smith.EURIS,European Railway Interlocking

Speci?cation.UIC,Commission7A/16,1992.

[5]J.A.Bergstra and J.W.Klop.Fixed point semantics in process algebras.Report

IW206,Mathematisch Centrum,Amsterdam,1982.

[6]M.A.Bezem and J.F.Groote.Invariants in process algebra with data.In B.Jon-

sson and J.Parrow,editors,Proceedings Concur’94,Uppsala,Sweden,Lecture Notes in Computer Science no.836,pages401-416,Springer Verlag,1994.

[7]M.A.Bezem and J.F.Groote.A correctness proof of a one bit sliding window

protocol inμCRL.The Computer Journal,37(4):289–307,1994.

[8]S.C.C.Blom.Personal communication,2003.

[9]S.C.C.Blom,W.J.Fokkink,J.F.Groote,I.van Langevelde,B.Lisser and J.C.van

de Pol.μCRL:A Toolset for Analysing Algebraic Speci?cations.In proceedings CAV’01.LNCS2102,pages250-254,2001.

[10]J.Brad?eld and C.Stirling.Modal logics and mu-calculi.In J.A.Bergstra,

A.Ponse and S.A.Smolka,Handbook of Process Algebra,pages293-332,Elsevier,

North-Holland,2001.

REFERENCES15 [11]M.G.J.van den Brand,H.A.de Jong,P.Klint and P.A.Olivier.E?cient Anno-

tated Terms.Software-Practice and Experience30:259-291,2000.

[12]R.E.Bryant.Graph-based algorithms for boolean function manipulation.IEEE

https://www.docsj.com/doc/0710358657.html,put.C-358:677-691,1986.

[13]https://www.docsj.com/doc/0710358657.html,ing higher order logic for modelling real-time protocols.In

Proc.TAPSOFT’91,LNCS494,pp.259–282.Springer,1991.

[14]K.M.Chandy and J.Misra.Parallel Program Design.A Foundation.Addison

Wesley,Reading MA1988.

[15]D.Chkliaev,J.Hooman,and E.de Vink.Veri?cation and improvement of the

sliding window protocol.In TACAS’03,LNCS2619,pp.113–127.Springer,2003.

[16]D.Dolev,M.Klawe and M.Rodeh.An O(n log n)unidirectional distributed algo-

rithm for extrema?nding in a circle.Journal of Algorithms,4:245-260,1982. [17]W.H.J.Feijen and A.J.M.van Gasteren.On a method of multiprogramming.

Springer Verlag.1999.

[18]W.J.Fokkink.Clocks,Trees and Stars in Process Theory.PhD.Thesis.Univer-

siteit van Amsterdam,1994.

[19]W.J.Fokkink,J.F.Groote,J.Pang,B.Badban,J.C.van de Pol.Verifying a Slid-

ing Window Protocol inμCRL.Technical report SEN-R0308,CWI,Amsterdam, 2003.

[20]W.J.Fokkink and J.Pang.Cones and Foci for Protocol Veri?cation Revisited.In

Proceedings of6th Conference on Foundations of Software Science and Computa-tion Structures(FoSSaCS),Lecture Notes in Computer Science2620,pp.267-281, Springer-Verlag,2003

[21]R.J.van Glabbeek and W.P.Weijland.Branching time and abstraction in bisim-

ulation semantics.Journal of the ACM43(3):555-600,1996.

[22]W.O.D.Gri?oen and F.W.Vaandrager.Normed simulations.In A.J.Z.Hu and

M.Y.Vardi,editors,Proceedings CAV’98,Vancouver,BC,Canada,LNCS1427, pages332-344,Springer-Verlag,1998.

[23]P.Godefroid and P.Wolper.A partial approach to model https://www.docsj.com/doc/0710358657.html,rmation

and Computation,110(2):305-326,1994.

[24]J.F.Groote and R.Mateescu.Veri?cation of Temporal Properties of Processes

in a Setting with Data.In Armando Martin Haeberer,editor,Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology

REFERENCES16 AMAST’99(Amazonia,Brazil),volume1548of Lecture Notes in Computer Sci-ence,pages74-90.Springer Verlag,January1999.

[25]J.F.Groote and H.P.Korver.Correctness proof of the bakery protocol inμCRL.

In Proc.ACP’94,Workshops in Computing,pp.63–86.Springer,1995.

[26]J.F.Groote and A.Ponse.The syntax and semantics of mCRL.In A.Ponse,

C.Verhoef and S.F.M.van Vlijmen,eds,Algebra of Communicating Processes,

Workshops in Computing,pp.26-62,1994.

[27]J.F.Groote and M.A.Reniers.Algebraic process veri?cation.In J.A.Bergstra,

A.Ponse and S.A.Smolka,Handbook of Process Algebra,pages1151-1208,Else-

vier,Amsterdam,2001.

[28]W.J.Fokkink,J.F.Groote and M.A.Reniers.Modelling distributed systems.To

appear,2004.

[29]J.F.Groote and M.P.A.Sellink.Con?uence for Process Veri?cation.In Theoretical

Computer Science B(Logic,semantics and theory of programming),170(1-2):47-81,1996.

[30]J.F.Groote and J.Springintveld.Focus points and convergent process operators:

a proof strategy for protocol veri?cation.The Journal of Logic and Algebraic

Programming49,pages31-60,2001.

[31]J.F.Groote and J.van Wamel.The parallel composition of uniform processes with

data.Theoretical Computer Science,266:631-6,2001.

[32]J.F.Groote and T.A.C.Willemse.A Checker for Modal Formulas for Processes

with Data,Eindhoven University of Technology,Department of Computer Science, CSR02-16,2002.

[33]J.F.Groote and T.A.C.Willemse.Parameterized boolean equation systems.Eind-

hoven University of Technology,Department of Computer Science,In preparation, 2004.

[34]https://www.docsj.com/doc/0710358657.html,municating Sequential Processes.Prentice Hall International,

1985.

[35]G.J.Holzmann.An Analysis of Bitstate Hashing.Formal Methods in System De-

sign13(3):289-307,1998.

[36]https://www.docsj.com/doc/0710358657.html,rmation processing systems–open systems interconnection–LOTOS

–a formal description technique based on the temporal ordering of observational behaviour ISO/TC97/SC21/N DIS8807,1987.

REFERENCES17 [37]A.S.Klusener.Models and axioms for a fragment of real time process algebra.

PhD.Thesis.Eindhoven University of Technology,1993.

[38]N.Lynch and M.Tuttle.An Introduction to Input/Output automata.CWI-

Quarterly,2(3):219–246,Centrum voor Wiskunde en Informatica,Amsterdam, The Netherlands,1989.

[39]A.Mader.Veri?cation of Modal Properties using Boolean Equation Systems.PhD.

Thesis.Fakult¨a t f¨u r Informatik.Technische Universit¨a t M¨u nchen,Dieter Bertz Verlag,1997.

[40]S.Mauw and G.J.Veltink.A process speci?cation formalism.Fundamentae Infor-

maticae.XIII:85–139,1990.

[41]https://www.docsj.com/doc/0710358657.html,ner.Processes:A mathematical model of computing agents.In H.E.Rose

and J.C.Shepherdson,editors,Proceedings Logic Colloquium1973,pages158-173.

North-Holland,1973.

[42]https://www.docsj.com/doc/0710358657.html,ner.A Calculus of Communicating Systems.volume92of Lecture Notes in

Computer Science.Springer-Verlag,1980.

[43]S.Owre,N.Shankar,J.M.Rushby,D.W.J.Stringer-Calvert.PVS Version2.4,Sys-

tem Guide,Prover Guide,PVS Language Reference.https://www.docsj.com/doc/0710358657.html,, 2001.

[44]K.Paliwoda and J.W.Sanders.An incremental speci?cation of the sliding-window

protocol.Distributed Computing,5:83–94,1991.

[45]D.M.R.Park.Concurrency and automata on in?nite sequences.In Proceedings of

5th GI Conference,LNCS104,pages167-183.Springer-Verlag,1981.

[46]W.Reisig.Petri Nets.Springer-Verlag,1985.

[47]C.R¨o ckl and J.Esparza.Proof-checking protocols using bisimulations.In Proc.

CONCUR’99,LNCS1664,pp.525–540.Springer,1999.

[48]A.A.Schoone.Protocols by Invariants.Cambridge International Series on Parallel

Computation7,Cambridge University Press,1996.

[49]J.L.A.van de Snepscheut.The sliding window protocol revisited.Formal Aspects

of Computing,7(1):3–170,1995.

[50]https://www.docsj.com/doc/0710358657.html,puter Networks(second edition).Prentice-Hall Interna-

tional,1988.

[51]https://www.docsj.com/doc/0710358657.html,enko.Linearization inμCRL.PhD.Thesis.Eindhoven University of Tech-

nology,Eindhoven,2002.

REFERENCES18 [52]F.W.Vaandrager.Veri?cation of two communication protocols by means of process

algebra.Report CS-R8608,CWI,Amsterdam,1986.

[53]J.J.van Wamel.A study of a one bit sliding window protocol in ACP.Report

P9212,University of Amsterdam,1992.

三爱三节演讲稿

践行“三爱三节”争做文明学生敬爱的老师、亲爱的同学们： 大家好！ 我是二年级的刘茹意。今天我演讲的题目是践行“三爱三节”争做文明学生。 勤以修身，俭以养德，节约为美。勤俭节约是中华民族的传统美德。立志向、有梦想，爱学习、爱劳动、爱祖国，德智体美全面发展，是当代小学生的终极目标。 学习，是我们学生最大的责任和义务。漫漫求学路，在书中学到的知识，提素质，明心智，辨是非。在学习中我们从慒慒无知的小孩到进入学校学习，这让我们受益匪浅。 劳动，它是我们创造一切的源泉。劳动绝非不雅，绝非低俗，相反的，劳动更是一种境界，一种升华，明白了它，就更让我们明白了辛劳，明白了艰辛。 爱国，更是一种光荣。由始至终，我们都在为我们是一个中国人而自豪。中国，她是我们心中最大的骄傲，我们爱我们的国家，我们爱她泱泱大地，我们爱她精彩文化，我们爱她不停步伐。 同学们，在我们的周围，勤俭节约无处不在。每个人都有义务把节约当作责任、当作习惯。节约可以从小事做起，从身边做起，时时刻刻严格要求自己节约不浪费：离开教室时，请伸伸你的小手，关掉电灯；洗手和抹布时，提醒一下身边的同学，把水龙头开得小一些，临走时检查一下，水龙头是否拧紧了。节约粮食，不挑食，不剩饭菜，与父母外出吃饭时，饭菜点的适量，如有剩余，打包带回家。节约的意识大家都有，其实节约做起来并不难。举手之劳，我们能做的还有很多。 亲爱的老师、同学们，空谈误国，实干兴邦。浪费不以量小而为之，节约不以微小而不为，勤俭节约，细水长流。让“节约光荣，浪费可耻”成为师生的常态习惯，成为一种校园的新风尚。希望大家能够勤奋学习，热爱劳动，体验生活，陶冶情操，让“三节三爱”飘扬在校园的每个角落，飘荡在祖国的每个角落。 同学们，让我们行动起来吧，践行“三爱三节”，争做文明学生！ 我得演讲结束了，谢谢大家！

DVS-6000视频服务器用户使用手册V11

客户端管理软件 用 户 使 用 手 册

本手册旨在帮助用户管理和使用本公司的视频服务器系列产品，使用本手册前您需要了解一些网络的基础知识，以便于更好的发挥产品的各种性能。您也可以通过网上联机帮助来获取更多的帮助。 本手册中使用的安全注意标记 警告! -- 表示一个可能存在损伤服务器的潜在危险。 危险! -- 表示一个会严重削弱服务器性能的操作。 遇到以上的操作时，尽量不要这样操作，除非您对该操作十分的了解。 知识产权 本手册所覆盖到的所有产品，都具有完全自主的知识产权，任何个人或者公司不得以任何理由盗用本公司的产品或者转载与本公司产品相关的资料文档。 技术支持与服务 在使用过程中，如果您遇到任何技术问题，您可以联系您本地的经销商。如果您的问题不能立即得到解决，他会将问题反映到公司技术部以确保能最快速的解决您的问题。如果您能够连接到internet您可以通过以下方式来解决： 1、通过公司网站下载相关软件的最新版本进行升级。 2、在公司常见问题解答页中找到您想知道的答案。 3、通过即时通讯软件如QQ或者MSN等联系公司技术支持人员。

目录 目录 (3) 1.1.网络产品主要功能参数： (5) 2.1. 客户端软件安装 (7) 1. 视频服务器参数配置 (10) 1.1. 视频及图像设置 (11) 1.1.1. 视频属性的设置 (12) 1.1.2. 图像设置 (12) 1.1.3. 图像高级设置技巧 (13) 1.2. OSD/MASK设置 (14) 1.3. 音频设置 (16) 1.4. 系统网络配置 (17) 1.5. 云台、串口设置 (19) 1.5.1. PTZ设备管理 (19) 1.5.2. PTZ协议设置 (19) 1.5.3. 232串口参数设置 (20) 1.5.4. 云台管理常见问题 (20) 1.6. 告警及事件管理 (20) 1.6.1. 视频移动告警管理 (20) 1.6.2. 视频丢失告警管理 (22) 1.6.3. 探头输入管理 (22) 1.6.4. 探头输出设置 (23) 1.7. PPPOE&DDNS设置 (24) 1.8. 中心平台接入配置 (25) 1.9. 系统设置 (26) 1.10. 用户权限设置 (31) 2. 客户端软件操作 (32) 2.1. 系统登录、锁定、退出 (32) 2.1.1. 系统登录 (32) 2.1.2. 系统锁定 (34) 2.1.3. 系统退出 (34) 2.2. 系统设置 (34) 2.2.1. 服务器管理 (34) 2.2.2. 用户管理 (40) 2.3. 服务器登录 (41) 2.3.1. 刷新服务器 (41) 2.3.2. 登录服务器 (41) 2.3.3. 退出登录服务器 (42) 2.4. 视频浏览、控制 (43) 2.4.1. 浏览视频 (43) 2.4.2. 声音播放控制 (45) 2.4.3. 云镜控制 (45) 2.4.4. 预置位 (46) 2.5. 语音对讲 (46)

半导体照明技术作业答案

某光源发出波长为460nm 的单色光，辐射功率为100W ，用Y 值表示其光通量，计算其色度坐标X 、Y 、Z 、x 、y 。 解：由教材表1-3查得460nm 单色光的三色视觉值分别为0.2908X =，0.0600Y =， 1.6692Z =，则对100W P =，有 4356831000.2908 1.98610lm 6831000.0600 4.09810lm 683100 1.6692 1.14010lm m m m X K PX Y K PY Z K PZ ==××=×==××=×==××=× 以及 )()0.144 0.030x X X Y Z y Y X Y Z =++==++=

1. GaP绿色LED的发光机理是什么，当氮掺杂浓度增加时，光谱有什么变化，为什么？GaP红色LED的发光机理是什么，发光峰值波长是多少？ 答：GaP绿色LED的发光机理是在GaP间接跃迁型半导体中掺入等电子陷阱杂质N，代替P原子的N原子可以俘获电子，又靠该电子的电荷俘获空穴，形成束缚激子，激子复合发光。当氮掺杂浓度增加时，总光通量增加，主波长向长波移动，这是因为此时有大量的氮对形成新的等电子陷阱，氮对束缚激子发光峰增加，且向长波移动。 GaP红色LED的发光机理是在GaP晶体中掺入ZnO对等电子陷阱，其发光峰值波长为700nm的红光。 2. 液相外延生长的原理是什么？一般分为哪两种方法，这两种方法的区别在哪里？ 答：液相外延生长过程的基础是在液体溶剂中溶质的溶解度随温度降低而减少，而且冷却与单晶相接触的初始饱和溶液时能够引起外延沉积，在衬底上生长一个薄的外延层。 液相外延生长一般分为降温法和温度梯度法两种。降温法的瞬态生长中，溶液与衬底组成的体系在均处于同一温度，并一同降温（在衬底与溶液接触时的时间和温度上，以及接触后是继续降温还是保持温度上，不同的技术有不同的处理）。而温度梯度法则是当体系达到稳定状态后，整个体系的温度再不改变，而是在溶液表面和溶液－衬底界面间建立稳定的温度梯度和浓度梯度。 3. 为何AlGaInP材料不能使用通常的气相外延和液相外延技术来制造？ 答：在尝试用液相外延生长AlGaInP时，由于AlP和InP的热力学稳定性的不同，液相外延的组分控制十分困难。而当使用氢化物或氯化物气相外延时，会形成稳定的AlCl化合物，会在气相外延时阻碍含Al磷化物的成功生长。因此AlGaInP 材料不能使用通常的气相外延和液相外延技术来制造。

6100系列使用说明书,视频服务器说明书

6100系列视频服务器 用户使用手册 （Ver2.1） 非常感谢您购买我公司的产品，如果您有什么疑问或需要请随时联系我们。 本手册适用于DS-6100HC、DS-6100HF视频服务器。 本手册可能包含技术上不准确的地方、或与产品功能及操作不相符的地方、或印刷错误。本手册的内容将根据产品功能的增强而更新，并将定期改进或更新本手册中描述的产品或程序，更新的内容将会在本手册的新版本中加入，恕不另行通知。

物品清单 小心打开包装盒，检查包装盒里面应有以下配件： 一台视频服务器 一本用户手册 一根DTE线 一根电源线 一张保修卡 一张合格证 一个光盘 如果发现有所损坏或者任何配件短缺的情况，请及时和经销商联系。

第一章用户手册简介 感谢您购买DS-6100系列视频服务器！ 在您准备使用本产品之前，请先仔细阅读本手册，以便能更好的使用本产品的所有功能。 1.1用途 本手册的用途是帮助您熟悉和正确的使用DS-6100系列视频服务器！ 1.2用户手册概述 第一章：用户手册简介 第二章：产品概述 第三章：硬件安装 第四章：软件安装 第五章：参数配置 第六章：广域网接入 附录Ａ：常见问题解答 附录Ｂ：技术参数

第二章产品概述 2.1产品简介 DS-6100系列视频服务器是专为远程监控而设计的嵌入式数字监控产品，采用最新的达芬奇平台处理芯片，LINUX嵌入式系统，完全脱离PC 平台，系统调度效率高，代码固化在FLASH中，系统运行更加稳定可靠。 DS-6100系列视频服务器具有视频信号和音频信号的硬件同步压缩功能，压缩码流通过网络进行传输，通过网络可进行实时视频和音频预览，支持流协议（RTP/RTCP）,支持IE预览，支持双向语音对讲，多种语言支持等功能。 2.2 产品型号说明 根据编码分辨率分两种： DS-6100HC：1~4路视频，音频输入，每路的视频分辨率最高支持CIF，也可以选择QCIF，不可以安装硬盘。 DS-6100HF: 1~2路视频，音频输入，每路的视频分辨率最高支持4CIF，也可以选择DCIF，2CIF，CIF，QCIF等，不可以 安装硬盘。 2.3主要功能及特点 2.3.1基本功能 视频压缩技术：采用H.264视频压缩技术及OggVorbis音频压缩技术，压缩比高，且处理非常灵活。

三节三爱演讲稿

人们常说爱祖国，爱学习，爱劳动。节约用水，节约用电，节约粮食，然而真正做到的有多少人呢？鲜艳的五星红旗,在雄壮的国歌声中冉冉升起,我们又迎来了崭新的一天.如今有一种风气风行全国,有一种理念深入人心,“三节三爱”已成为一个惹人注目的信息,学校到处张贴“爱学习,爱劳动,爱祖国.节水,节电,节约粮食”的条形标语,我总是驻足观望,细心读来,每次读它都有新的感悟,它所提到的无疑是一种正能量,一种向上的能量,交给我们正确的人生观,荣辱观,同学们都应该带着它乘风破浪,勇往直前! 勤以修身,俭以养德,节约为美,勤俭节约是中华民族的传统美德.学习,是我们学生最大的责任和义务,学习是同本之举,是源头活水,庄子曰“吾生也有涯,而知也无涯”,知识是力量,学习改变命运,爱学习我们才能在知识的海洋徜徉,才能能为自信,自强,自立的一代青年.我们的祖先也有一句名言：劳动最光荣！我们现在的劳动无非就是帮父母扫扫地,擦擦桌子,在学校里整整桌椅,其实就是一件小事,“勿以善小而不为,勿以恶小而为之”.很多的善小都能使他人收益匪浅. 爱国是一种光荣,自始至终我们都为是一个中国人而自豪！我们的祖国有5000年文明历史,有960万平方公里.勤劳智慧的中华儿女共,同开拓了辽阔的疆域,创造了辉煌灿烂的文化.肩负着实现中华民族伟大复兴的我们,要热爱祖国的大好河山,积极维护祖国的主权独立和领土完整,祖国的领土寸土不能丢,不能被分裂侵占；要热爱祖国的历史和文化,提高民族自尊心和自信心,为创造更加辉煌的民族文

化而尽心尽力.“历览前贤国与家,成由勤俭败由奢”.这是历史上的有识之士从家族兴衰、社稷兴亡、朝代更替的无数经验教训中得到的一条深刻警示.近日党中央提出建设节约型社会,就是从这一警示中作出的一个事关国家长远发展和民族兴衰的战略举措. 节约是中华民族的传统美德,是我们民族世代相传的精神财富,也是我们这个民族百折不饶、生生不息的力量源泉.节约这种美德为世代中国人所崇尚.早在春秋时期,俭朴就作为一种公德,为智者仁人所大力倡导.《论语》中就有“夫子温、良、恭、俭、让以得之.”其中“俭”就是节俭.意思是孔子具有包括节俭在内的五种品德,所以能赢得人们的信任.墨子也极力主张要在衣、食、住、行、丧葬等方面“制为节用之法”.“节约”符合“天德”.奢侈浪费就是“亏夺人衣食之财”,侵害别人的生存权.《左传》中说：“俭,德之共也,侈,恶之大也”.把俭朴作为培养良好道德的基础,把侈奢看成是一切恶行的根源.诸葛亮在《诫子书》中说：“夫君子之行,静以修身,俭以养德,非淡泊无以明志,非宁静无以致远”.多少年来,在中国社会发展的各个时期,艰苦朴素、勤劳节俭都作为一种被社会普遍认同的传统美德,得到倡导、保持和发扬.这也是我国由小到大、由弱到强的重要因素. 在全社会大力倡导“节约”的传统美德,重在实践,贵在坚持.我们应牢固树立“以艰苦朴素、勤俭节约为荣、以铺张浪费、奢侈挥霍为耻”的荣耻观；每个家庭都要节约持家,不要铺张浪费,不超前消费；每个学生都要在工作学习生活中自觉弘扬节约的优良作风,养成节约一滴水、一度电、一张纸、一滴油、一粒米的良好习惯.只要我们每个人

LED半导体照明的发展与应用

LED半导体照明的发展与应用 者按：半导体技术在上个世纪下半叶引发的一场微电子革命，催生了微电子工业和高科技ＩＴ产业，改变了整个世界的面貌。今天，化合物半导体技术的迅猛发展和不断突破，正孕育着一场新的革命——照明革命。新一代照明光源半导体ＬＥＤ，以传统光源所没有的优点引发了照明产业技术和应用的革命。半导体ＬＥＤ固态光源替代传统照明光源是大势所趋。１、ＬＥＤ半导体照明的机遇 （１）全球性的能源短缺和环境污染在经济高速发展的中国表现得尤为突出，节能和环保是中国实现社会经济可持续发展所急需解决的问题。作为能源消耗大户的照明领域，必须寻找可以替代传统光源的新一代节能环保的绿色光源。 （２）半导体ＬＥＤ是当今世界上最有可能替代传统光源的新一代光源。 其具有如下优点： ①高效低耗，节能环保； ②低压驱动，响应速度快安全性高； ③固体化封装，耐振动，体积小，便于装配组合； ④可见光区内颜色全系列化，色温、色纯、显色性、光指向性良好，便于照明应用组合； ⑤直流驱动，无频闪，用于照明有利于保护人眼视力； ⑥使用寿命长。 （３）现阶段ＬＥＤ的发光效率偏低和光通量成本偏高是制约其大规模进入照明领域的两大瓶颈。目前ＬＥＤ的应用领域主要集中在信号指示、智能显示、汽车灯具、景观照明和特殊照明领域等。但是，化合物半导体技术的迅猛发展和关键技术的即将突破，使今天成为大力发展半导体照明产业的最佳时机。２００３年我国人均ＧＤＰ首次突破１０００美元大关，经济实力得到了进一步的增强，市场上已经初步具备了接受较高光通量成本（初始成本）光

源的能力。在未来的１０～２０年内，用半导体ＬＥＤ作为光源的固态照明灯，将逐渐取代传统的照明灯。 （４）各国政府予以高度重视，相继推出半导体照明计划，已形成世界性的半导体照明技术合围突破的态势。 ①美国：“下一代照明计划”时间是２０００～２０１０年投资５亿美元。美国半导体照明发展蓝图如表１所示； ②日本：“２１世纪的照明计划”，将耗费６０亿日元推行半导体照明目标是在２００６年用白光ＬＥＤ替代５０％的传统照明； ③欧盟：“彩虹计划”已在２０００年７月启动通过欧共体的资助推广应用白光ＬＥＤ照明； ④中国：２００３年６月１７日，由科技部牵头成立了跨部门、跨地区、跨行业的“国家半导体照明工程协调领导小组”。从协调领导小组成立之日到２００５年年底之前，将是半导体照明工程项目的紧急启动期。从２００６年的“十一五”开始，国家将把半导体照明工程作为一个重大项目进行推动； （５）我国 的半导体ＬＥＤ产业链经过多年的发展已相对完善，具备了一定的发展基础。同时，我国又是照明灯具产业的大国，只要政府和业界协调整合好，发展半导体ＬＥＤ照明产业是大有可为的； ２ＬＥＤ的发展历程（如图１所示） ２．１ＬＥＤ技术突破的历程

半导体照明技术及其应用

《半导体照明技术及其应用》课程教学大纲 （秋季） 一、课程名称：半导体照明技术及其应用Semiconductor Lighting Technology and Applications 二、课程编码： 三、学时与学分：32/2 四、先修课程: 微积分、大学物理、固体物理、半导体物理、微电子器件与IC设计 五、课程教学目标： 半导体照明是指用全固态发光器件LED作为光源的照明，具有高效、节能、环保、寿命长、易维护等显著特点，是近年来全球最具发展前景的高新技术领域之一，是人类照明史上继白炽灯、荧光灯之后的又一场照明光源的革命。本课程注重理论的系统性﹑结构的科学性和内容的实用性，在重点讲解发光二极管的材料、机理及其制造技术后，详细介绍器件的光电参数测试方法，器件的可靠性分析、驱动和控制方法，以及各种半导体照明的应用技术，使学生学完本课程以后，能对半导体照明有深入而全面的理解。 六﹑适用学科专业：电子科学与技术 七、基本教学内容与学时安排： 绪论（1学时） 半导体照明简介、学习本课程的目的及要求 第一章光视觉颜色（2学时） 1光的本质 2光的产生和传播 3人眼的光谱灵敏度 4光度学及其测量 5作为光学系统的人眼 6视觉的特征与功能 7颜色的性质 8国际照明委员会色度学系统 9色度学及其测量 第二章光源（1学时） 1太阳 2月亮和行星 3人工光源的发明与发展 4白炽灯 5卤钨灯 6荧光灯 7低压钠灯

8高压放电灯 9无电极放电灯 10发光二极管 11照明的经济核算 第三章半导体发光材料晶体导论（2学时） 1晶体结构 2能带结构 3半导体晶体材料的电学性质 4半导体发光材料的条件 第四章半导体的激发与发光（1学时） 1PN结及其特性 2注入载流子的复合 3辐射与非辐射复合之间的竞争 4异质结构和量子阱 第五章半导体发光材料体系（2学时） 1砷化镓 2磷化镓 3磷砷化镓 4镓铝砷 5铝镓铟磷 6铟镓氮 第六章半导体照明光源的发展和特征参量（1学时）1发光二极管的发展 2发光二极管材料生长方法 3高亮度发光二极管芯片结构 4照明用LED的特征参数和要求 第七章磷砷化镓、磷化镓、镓铝砷材料生长（3学时）1磷砷化镓氢化物气相外延生长（HVPE） 2氢化物外延体系的热力学分析 3液相外延原理 4磷化镓的液相外延 5镓铝砷的液相外延 第八章铝镓铟磷发光二极管（2学时） 1AlGaInP金属有机物化学气相沉积通论 2外延材料的规模生产问题 3电流扩展 4电流阻挡结构 5光的取出 6芯片制造技术

三爱三节演讲稿范文(精选3篇)

三爱三节演讲稿范文（精选3篇） 三爱三节演讲稿范文 演讲稿特别注重结构清楚，层次简明。在现在社会，能够利用到演讲稿的场合越来越多，还是对演讲稿一筹莫展吗？下面是整理的三爱三节演讲稿范文，欢迎大家分享。 三爱三节演讲稿范文1敬爱的老师，亲爱的同学们： 大家好！今天我演讲的主题是“三爱三节”。 现如今，在祖国的号召下有一种风气正盛行，有一种观念正深入人心，那就是“三爱三节”。“三爱三节”指的是爱学习、爱劳动、爱祖国；节约用水、节约粮食、节约用电。 学习，可以提素质，明心智，辨是非，学习是我们每个人成长、成才、成功的基础。古语云：“书也，善读可以医愚”，书籍是人类进步的阶梯，通过读书可以开拓视野，结识朋友，增长知识，知识就是资本，知识就是财富。对于我们小学生来说，更要养成良好的读书和学习习惯，不迟到、早退；当天作业当天完成，不拖拉、书写工整；上课认真听讲，积极思考；课后认真预习、复习。除学习课本知识以外，多阅读报纸、课外书刊，拓宽自己的视野，丰富自己的知识面，提高自学能力。 劳动，是我们创造一切的源泉。高尔基说过：“世界上最美好的东西，都是由热爱劳动的人双手创造出来的。”劳动是伟大而崇高的，劳动是光荣而神圣的。我们要从小养成热爱劳动的好习惯，在学校，

从身边小事做起，擦桌椅，扫教室，捡纸屑，维护好教室和校园的卫生，让身边环境保持干净整洁；在家里，打扫好房间的卫生，并帮助爸爸妈妈做家务，让忙碌一天的爸爸妈妈回家好好休息。 祖国，是哺育我们的母亲，是生命的摇篮，我因为自己是一个中国人而感到骄傲。自古以来涌现出许许多多的爱国事例：古有岳飞精忠报国、近有中国导弹之父钱学森舍弃国外的荣华富贵依然回国报效祖国、今有罗阳为祖国的强盛而鞠躬尽瘁。我们要树立一个远大的志向，锻炼好身体，培养高尚道德，掌握丰富知识，把自己的学习同祖国的繁荣富强紧密联系在一起，为祖国的振兴贡献自己的力量。 同学们，在我们的周围，勤俭节约无处不在。每个人都有义务把节约当作责任、当作习惯。节约可以从小事做起，从身边做起，时时刻刻严格要求自己节约不浪费：离开教室时，请伸出你的手，关掉电灯；洗手时，把水龙头开得小一些，临走时，将水龙头拧紧；吃饭时，不挑食，不剩饭菜，与父母外出吃饭时，饭菜点的适量，如有剩余，打包带回家。节约的意识大家都有，其实节约做起来并不难。一度电，漫漫黑暗夜的光明希望；一滴水，沙漠饥渴人的精神支柱；一粒米，辛勤劳动者的汗水结晶。 同学们，让我们积极行动起来，从我做起，从现在做起，从身边小事做起，从点点滴滴做起，做到爱学习、爱劳动、爱祖国，节约用水，节约粮食，节约用电。相信通过我们的努力会让我们的校园更美好，让社会更文明，让国家更富强，为构建“资源节约型，环境友好型”社会尽一份责任，让勤俭节约蔚然成风！

无线视频服务器快速使用手册样本

无线网络视频传输系统快速使用手册

第一章前言 本用户手册描述了安装和配置无线网络视频传输系统的简单操作方法。用户经过阅读本手册, 能安装和设置视频编码器的初级参数, 以满足快速使用的要求。 无线网络视频传输系统工作原理: 网络视频编码器用来接收视频源信号加以编码、压缩和传输。经过无线网络将视频信号传输到公网的服务器端。用户经过客户端对服务器进行访问, 获得需要的视频资源。 在下文中介绍了网络视频编码器的安装、客户端和服务器端的安装和简单使用, 如果用户需要进一步了解高级功能, 请参照用户手册。 第二章设备简介 一简介 网络视频编码器是一个集视频采集、实时压缩、网络传输( 有线或无线) 等功能为一体的嵌入式设备。 设备接通电源之后就能够独立工作, 首先把采集的视频图像经H.264算法进行压缩编码, 然后将压缩后的视频数据传输到视频监控流媒体服务器中, 用户能够经过客户端监控软件登录流媒体服务器进行实时视频浏览、监控和管

理。 二外观 设备根据工业设计标准, 采用烤漆金属外壳, 包装精美、小巧, 方便携带或固定放置, 请参下图: 图2-1 外观 三设备重要部分介绍 电源适配器。

天线。 天线接口: 根据数字的不同与每张卡进行对应。 SIM卡插槽: SIM1: 装CDMA SIM卡1; 2: 装CDMA SIM卡2。( 每个SIM卡座旁都有 一个黄色小按钮, 用于取出SIM卡座) CDMA卡的安装。 DC9-24V: 电源插口, 接12V电源适配器( 可适应9-24V电压)

BNC视频输入接口。 RJ45以太网接口: 接网络集线器的以太网端口。该网口用来在设备 使用前对设备进行参数配置。如目的IP地址, 云台参数等。 设备状态指示灯: 指示各种状态, 方便用户掌握设备运行情况 Cell1和Cell2: 指示Modem拨号情况, 如果拨号成功, 则常亮; Data: 指示视频数据传输状况, 不停的闪烁, 表明正常传输视 频数据; Ctrl: 指示控制信号和心跳信号的传输; PWR: 指示设 备电源状态 复位: 该孔内有一个内凹的按钮, 用来对系统设置参数的恢复出厂值。例如: 当一些用户忘记设备的物理地址时经过此键恢复为192.168.0.250。或是忘记密码时可恢复为”888888”。使用方法为: 加电状态下, 按住按钮20秒以上时间, 当六个信号灯连续闪烁两次时, 即复位成功。

流媒体服务器软件使用说明

流媒体服务器软件使用说明 时间：2014-01-24发布出处：海康威视浏览数：73952 流媒体服务器软件是客户端软件（目前版本为iVMS-4200 ）的组成模块之一，点击下载网站上客户端软件，安装时可选择流媒体服务器软件。流媒体服务器软件需要和客户端配合使用才能起到转发效果。 流媒体服务器的使用步骤： 1.在欲做转发服务器的PC或服务器上安装并运行流媒体服务器软件，软件从上到下两块内容依次是连接信息区和命令信息区。（可直接运行，不需配置，或根据需要在配置中改变端口）。 注意：使用流媒体时需要关闭PC或者服务器的防火墙。如有特殊需求不能关闭防火墙，则需要映射554以及端口段。 2.运行软件后，在客户端PC上添加流媒体服务器。在“设备管理”界面选择流媒体服务器，选择“添加设备”。 3.在弹出的对话框中填入运行流媒体服务器软件的PC或服务器的IP地址和端口号点击确定即可。（若没有修改流媒体服务器的端口，使用默认的554就可以）。 4.选择添加的流媒体服务器，点击“配置”，选择需要通过流媒体取流的监控点。 5.在其他需要访问的电脑客户端上重复第2-4这3个步骤，全部都添加完成后即可。添加成功后进行预览，在连接信息区和命令信息区能分别看到提示。 开启流媒体服务器转发后依旧没有效果的可能原因： 1.有部分客户端没有添加流媒体服务器，依然通过直连设备来获取数据流。 无转发效果，有PC通过IE访问设备后，已经占用设备若干并发流路数，此时客户端通过流媒体转发也会有部分通道播放失败。此时，可关掉IE预览测试。 3.流媒体服务器网络上传达到上限，无法有效进行转发。此时需要确认转发的路数没有达到服务器网络负荷能力上限，目前4200流媒体服务器转发能力为进64路，出200路（按2M码流计算，如果码流高于2M，则进出路数相应减少；但如果低于2M码流，最大进出路数不变。）。 4.运行了多个流媒体服务器软件，一台硬盘录像机的图像通过不同的流媒体服务器进行转发。

模拟电子技术基础-第1章 常用半导体器件题解

第一章 常用半导体器件 自 测 题 一、判断下列说法是否正确，用“√”和“×”表示判断结果填入空内。 （1）在N 型半导体中如果掺入足够量的三价元素，可将其改型为P 型半导体。（ ） （2）因为N 型半导体的多子是自由电子，所以它带负电。（ ） （3）PN 结在无光照、无外加电压时，结电流为零。（ ） （4）处于放大状态的晶体管，集电极电流是多子漂移运动形成的。 （ ） （5）结型场效应管外加的栅-源电压应使栅-源间的耗尽层承受反向电压，才能保证其R G S 大的特点。（ ） （6）若耗尽型N 沟道MOS 管的U G S 大于零，则其输入电阻会明显变小。（ ） 解：（1）√ （2）× （3）√ （4）× （5）√ （6）× 二、选择正确答案填入空内。 （1）PN 结加正向电压时，空间电荷区将 。 A. 变窄 B. 基本不变 C. 变宽 （2）设二极管的端电压为U ，则二极管的电流方程是 。 A. I S e U B. T U U I e S C. )1e (S －T U U I （3）稳压管的稳压区是其工作在 。 A. 正向导通 B.反向截止 C.反向击穿 （4）当晶体管工作在放大区时，发射结电压和集电结电压应为 。 A. 前者反偏、后者也反偏 B. 前者正偏、后者反偏 C. 前者正偏、后者也正偏 （5）U G S ＝0V 时，能够工作在恒流区的场效应管有 。 A. 结型管 B. 增强型MOS 管 C. 耗尽型MOS 管 解：（1）A （2）C （3）C （4）B （5）A C

三、写出图T1.3所示各电路的输出电压值，设二极管导通电压U D＝0.7V。 图T1.3 解：U O1≈1.3V，U O2＝0，U O3≈－1.3V，U O4≈2V，U O5≈1.3V， U O6≈－2V。 四、已知稳压管的稳压值U Z＝6V，稳定电流的最小值I Z mi n＝5mA。求图T1.4所示电路中U O1和U O2各为多少伏。 图T1.4 解：U O1＝6V，U O2＝5V。

电子技术各章知识点

电子技术复习 CH14半导体器件 1.本征半导体、N型半导体、P半导体的基本概念；PN的单 向导电特性；温度和参杂浓度对多子和少子的影响。 2.二极管的基本参数（死区电压、导通电压）及相关应用， 学会判断二极管在电路中的工作状态（导通、截止）。掌握含二极管电路的分析方法。 3.了解稳压管的工作原理，基本稳压管稳压电路的分析。(两 稳压管串联、并联) 4.半导体三极管工作状态的特点（放大、饱和、截止）。 5.半导体三极管的管脚的判定 CH15基本放大电路 1.放大电路（共射）的分析方法（直流通路法、微变等效电 路法） 2.静态工作点稳定电路(分压式偏置电路)的结构、特点和分 析方法(静态、动态) 3.射极输出器的特点，电路分析。 4.差分放大电路的输入信号（共模、差模、比较），共模抑制 比的概念（理想共模抑制比=？） CH16集成运算放大器 1.运放的理想化条件 2.运放在线性区和非线性区的分析方法

3. 运放线性应用电路的分析（比例运算[同相（电压跟随器）、反相(反相器)]、反相加法运算、减法运算） CH17电子电路中的反馈 1. 反馈的基本概念 2. 负反馈类型的判断方法（会判断正、负反馈；电压、电流反馈；串联、并联反馈） 3. 负反馈对放大器性能的影响（影响类别？闭环放大倍数？ AF A A f += 1） 4. 自激振荡起振的条件、振荡建立条件、稳振条件？ 5. 典型RC 两种类型电路的电路分析。 CH18直流稳压电源 1. 直流稳压电源的组成及各部分的作用 u 1- + 2. 单相半波、全波(桥式整流)电路的构成和工作原理，二极管的选择依据（计算，见例题和作业题），桥式的输出波形受二极管的影响

三节三爱的演讲稿

节食节粮 从以往得“民以食为天”随着时代逐渐得发展渐渐演变成了“民以食为乐”越来越多新奇古怪花样百出得食物出现在我们桌上，让大家渐渐忘了食物原本得意义。 逢年过节，家里常常来了许多人做客，一套套传统得菜被端了上来，老人们得眼里都布满了笑容与满足，而小孩子却在旁边拿着筷子嘴里嘟囔着：“怎么又就是这些菜呀。” 记得那天，当桌上端上了菜，姐姐就开始抱怨：“这些菜吃了那么多年早腻了，我们出去吃肯德基麦当劳。”桌子被敲得咚咚得响，爷爷奶奶有些生气了，眉间显露出了一股沧桑感，双目盯着那几道菜，眼神飘得很远：“您们这些小孩呀，现在整天就想着吃好得，其实有得吃就已经很不错了，想当年我们那会吃饭吃肉都不就是顿顿都有得呀！” 坐在一旁得大人们也开始议论道：“爸妈，现在就是二十一世纪了，不要老就是跟孩子们说旧时代得事，孩子们，总想着吃些好得，人之常情么。过去得就过去了就别再想了。” 爷爷奶奶听了，神情显得有些尴尬与失望，无奈得摇了摇手：“说得就是这样没错，但就是。。”“好了好了，别说这些了。”话还没说完就被打断了，她们深深得叹了口气。 饭吃完了，桌上剩许多剩饭剩菜，瞧着这些菜，爷爷奶奶想说些什么但还就是犹豫着没有说什么，安安静静得坐在旁边同时我仿佛又听到了她们得叹息。 坐在一旁得我听着大家得絮絮叨叨，想到在书上瞧到过得文章，现在得生活哪有好转，那些受到战争侵略得人呢，她们不就是跟爷爷奶奶那辈一样么。许多人因为战争饭都吃不饱，她们没有心思去想吃好得，因为她们却连吃饭都显得有些奢侈。 想想现在全世界都倡导低碳环保，减少二氧化碳得排放量，减少对地球得污染，在我们开始减少使用塑料袋得次数就是，在我们出门减少用汽车多步行时，在我们提倡全球关灯一小时时，也要想想，节约点食物也不就是我们力所能及得么，别再在饭桌上挑东捡西，别在沉迷于快餐无法自拔，让那么辛苦播种来得食物尽到她们原本应尽到得义务，这不就是比原本在饭桌上留下一堆得剩饭剩菜来得更有意义么？

半导体照明技术学习考试资料

1. GaP绿色LED的发光机理是什么，当氮掺杂浓度增加时，光谱有什么变化，为什么？GaP红色LED的发光机理是什么，发光峰值波长是多少？答：GaP绿色LED的发光机理是在GaP间接跃迁型半导体中掺入等电子陷阱杂质N，代替P原子的N原子可以俘获电子，又靠该电子的电荷俘获空穴，形成束缚激子，激子复合发光。当氮掺杂浓度增加时，总光通量增加，主波长向长波移动，这是因为此时有大量的氮对形成新的等电子陷阱，氮对束缚激子发光峰增加，且向长波移动。 GaP红色LED的发光机理是在GaP晶体中掺入ZnO对等电子陷阱，其发光峰值波长为700nm的红光。 2. 液相外延生长的原理是什么？一般分为哪两种方法，这两种方法 的区别在哪里？ 答：液相外延生长过程的基础是在液体溶剂中溶质的溶解度随温度 降低而减少，而且冷却与单晶相接触的初始饱和溶液时能够引起外 延沉积，在衬底上生长一个薄的外延层。 液相外延生长一般分为降温法和温度梯度法两种。降温法的瞬态生 长中，溶液与衬底组成的体系在均处于同一温度，并一同降温（在 衬底与溶液接触时的时间和温度上，以及接触后是继续降温还是保 持温度上，不同的技术有不同的处理）。而温度梯度法则是当体系 达到稳定状态后，整个体系的温度再不改变，而是在溶液表面和溶 液－衬底界面间建立稳定的温度梯度和浓度梯度。 3. 为何AlGaInP材料不能使用通常的气相外延和液相外延技术来制造？答：在尝试用液相外延生长AlGaInP时，由于AlP和InP的热力学稳定性的不同，液相外延的组分控制很困难。而当使用氢化物或氯化物气相外延时，会形成稳定的AlCl化合物，会在气相外延时阻碍含Al磷化物的成功生长。故AlGaInP材料不能用通常的气相外延和液相外延技术来制造。 4. 对三基色体系的白光LED，列出基色光源的三个最佳峰值波长。对荧光转换的白光LED和多芯片的白光LED，这三基色用什么方法来实现？答：三基色体系的白光LED，基色光源的三个最佳峰值波长分别为450nm、540nm和610nm。对荧光转换的白光LED，是用部分被吸收的AlInGaN 芯片的蓝光和适当的绿光和橙红光两种荧光粉来实现。对多芯片白光LED，是用峰值波长600nm附近的AlGaInP基LED，以及峰值波长450nm 和540nm的AlInGaN LED组成。 5. 简要说明LED封装技术发展三个阶段的时间范围、典型LED及其驱动电流、器件应用领域。 答：LED封装技术发展的3个阶段分别为： （1）1962~1989年期间，典型的LED为?3和?5的LED，驱动电流一般小于等于20mA，主要用做信号指示和显示。 （2）1990~1999年，发展了大光通量LED食人鱼和Snap，驱动电流在50~150mA，主要用于大型信号指示，如汽车信号灯、景观照明。 （3）2000年至今，研发和生产了功率型LED，电流≥350mA，开始用于照明，并开始了更大光通量输出的组件的研制和生产。 6. 画出透明衬底的AlGaInP LED的结构示意图，简要说明其芯片制造流程。 答：结构示意图如下图所示。 此LED结构用的是MOCVD生长在GaAs上的双异质结(AlxGa1-x)0.5In0.5P，并在结构上方VPE生长一个小于50μm厚的GaP 窗层。在外延生长后，用通常的化学腐蚀技术移除GaAs吸收衬底，使双异质结结构的N型层暴露，再通过升高温度和加压，将晶片黏结到200~250μm厚的N型GaP衬底上。1. 画出典型的具有GaP窗层和吸收衬底的双异质结AlGaInP LED的结构示意图，简述为什么需要使用电流扩展窗层。 答：结构示意图如下图所示。 为了使LED芯片获得高效的发光，电流扩展是主要关键之一，如 上图的结构，器件的上方覆盖了圆形的金属顶，电流从芯片的顶部 接触通过P型层流下到达结区，在结区发光。但是假如P型层的电 阻太高，电流将扩展很少，而仅仅限在金属之下，光仅仅发生在电极 之下，而且被芯片内部吸收。有效的最好性能的AlGaInP LED是在 通常的双异质结顶部再生长一个厚的P型窗层，而不用AlGaInP材 料。这个电流扩展窗层与AlGaInP相比，具有高的薄层电导率，而 且对发射光是透明的，可以达到很好的电流扩展效果。 4.LED作为城市景观照明中的首选光源的优点：①色彩丰富纯度高、节能②响应时间短，瞬时达到全光输出，可深度调光③体积小、方向 性强④直流低压驱动，简化系统设计，降低电路成本⑤寿命长，工作 安全可靠，维护费用大大降低。景观常用LED灯具有护栏灯、树灯 5. LED的电学性能特点：LED是单向导电器件。LED是个具有PN结结构的半导体器件，具有势垒电势，所以就有导通阈值电压。LED的电流—电压特性是非线性的。LED的正向压降与PN结结温的温度系数为负。流过LED的电流和LED的光通量的比值也是非线性的。 6. 电源驱动方案：（1）低电压驱动。是指用低于LED正向导通压降的电压驱动LED，如一节普通干电池、镍镉电池供电的低功耗照明器件，LED 手电、头灯、应急灯、路障灯、节能台灯等，采用电荷泵式升压变换器（2）过渡电压驱动。是指给LED供电的电源电压值在LED正向压降附近变动。如一节锂电池或两节串联的铅酸蓄电池，电池充满时在4V以上，快用完时在3V以下，应用有矿灯等，是反极性电荷泵式变换器（3）高压驱动。是指给LED供电的电压值高于LED的正向压降，如6V.12V.24V蓄电池，应用有太阳能草坪灯、太阳能庭院灯等，变换器电路是串联开关降压电路。（4）市电驱动。是对半导体照明应用最具有价值的供电方式，中小功率LED采用隔离式单端反激变换器，大功率用桥式变换电路。 7.可靠性试验指：产品在规定的条件下、在规定的时间内完成规定的功能的能力。产品在设计、应用过程中，不断经受自身及外界气候环境及机械环境的影响，而仍需要能够正常工作，这就需要以试验设备对其进行验证，按试验目的可分为筛选试验、例行试验、鉴定验收试验；按照试验项目可分为环境试验和寿命试验。 8. （1）平均寿命：指一批电子器件产品寿命的平均值（2）可靠寿命：指一批电子器件产品的可靠度下降到时，所经历的工作时间（3）中位寿命：指产品的可靠度降为50%时的寿命（4）特征寿命：指产品的可靠度降为1/e时的寿命（5）LED的寿命：通常用“半衰期”即器件的光输出下降到起始值50%时的时间作为LED的寿命。 用B50和L70来表示功率LED的寿命。L70（B50）表示功率LED比起初始值来，平均流明值下降到维持70%（50%）的时间。 9. 画出器件失效率随时间变化的曲线，说明曲线的各个阶段及其失 效原因。 答：曲线如图分为三个阶段： 第一个阶段称为早期失效或 老化阶段，失效率较高，随工作时间的延长而迅速下降。造成早期 失效的原因大多属生产型缺陷，由产品本身存在的缺陷所致。 第二个阶段为有效寿命阶段，又称随机失效阶段，失效率很低且 很稳定，近似为常数，器件失效往往带有偶然性。 第三个阶段称耗损失效阶段，失效率明显上升，大部分器件相继出现 失效，耗损失效都由于老化、磨损和疲劳等原因使器件性能恶化所致。 10. 伏安特性指流过PN结的电流随电压变化的特性，应将正、反向均包括在内。（1）反向击穿电压Vb：表示器件反向耐压高低的参数，通常是指一定漏电流下器件两端的反向电压值（2）反向电流Ir：给定反向电压下流过器件的反向电流值（3）正向电压Vf：指定正向电流下器件两端的正向电压值。作用：标志着结的体电阻及欧姆接触串联电阻的高低，可在一定程度上反应电极制作的好坏 12. 热管是依靠自身内部工质液相和气体二相变化来实现传热的导热元件，它是由高纯度的无氧铜管及铜丝网或铜粉烧结物组成，内充液体为工作介质。当受热端将工作液相蒸发成气相，气流经过中空管道流到冷却端，冷却后将工作流体凝结成液相，冷凝液借助于铜丝网或铜粉烧结物的毛细组织吸回受热端，完成吸热-放热循环，可在一定温差下将热量传导出。具有重量轻、结构简单、热传输量大、耐用寿命长、导热能力强等优点。回路热管比单管热管效率更高且不受位置影响。

无线视频服务器快速使用手册

. 无线网络视频传输系统 快速使用手册

第一章前言 本用户手册描述了安装和配置无线网络视频传输系统的简单操作方法。用户通过阅读本手册，能安装和设置视频编码器的初级参数，以满足快速使用的要求。 无线网络视频传输系统工作原理： 网络视频编码器用来接收视频源信号加以编码、压缩和传输。通过无线网络将视频信号传输到公网的服务器端。用户通过客户端对服务器进行访问，获得需要的视频资源。 在下文中介绍了网络视频编码器的安装、客户端和服务器端的安装和简单使用，如果用户需要进一步了解高级功能，请参照用户手册。 第二章设备简介 一简介 网络视频编码器是一个集视频采集、实时压缩、网络传输（有线或无线）等功能为一体的嵌入式设备。 设备接通电源之后就可以独立工作，首先把采集的视频图像经H.264算法进行压缩编码，然后将压缩后的视频数据传输到视频监控流媒体服务器中，用户可以通过客户端监控软件登录流媒体服务器进行实时视频浏览、监控和管理。 二外观 设备根据工业设计标准，采用烤漆金属外壳，包装精美、小巧，方便携带或固定放置，请参下图：

图2-1 外观 三设备重要部分介绍 电源适配器。 天线。 天线接口：根据数字的不同与每张卡进行对应。

SIM卡插槽：SIM1：装CDMA SIM卡1；2：装CDMA SIM卡2。（每个SIM卡座旁都有一个黄色小按钮， 用于取出SIM卡座） CDMA卡的安装。 DC9-24V：电源插口，接12V电源适配器（可适应9-24V电压） BNC视频输入接口。 RJ45以太网接口：接网络集线器的以太网端口。该网口用来在设备使用前对设备进行参数配置。如目的IP地址，云台参数等。 设备状态指示灯：指示各种状态，方便用户掌握设备运行情况Cell1和Cell2： 指示Modem拨号情况，如果拨号成功，则常亮；Data：指示视频数据传输

半导体器件(附答案)

第一章、半导体器件（附答案） 一、选择题 1．PN 结加正向电压时，空间电荷区将 ________ A. 变窄 B. 基本不变 C. 变宽 2．设二极管的端电压为 u ，则二极管的电流方程是 ________ A. B. C. 3．稳压管的稳压是其工作在 ________ A. 正向导通 B. 反向截止 C. 反向击穿区 4．V U GS 0=时，能够工作在恒流区的场效应管有 ________ A. 结型场效应管 B. 增强型 MOS 管 C. 耗尽型 MOS 管 5．对PN 结增加反向电压时，参与导电的是 ________ A. 多数载流子 B. 少数载流子 C. 既有多数载流子又有少数载流子 6．当温度增加时，本征半导体中的自由电子和空穴的数量 _____ A. 增加 B. 减少 C. 不变 7．用万用表的 R × 100 Ω档和 R × 1K Ω档分别测量一个正常二极管的正向电阻，两次测量 结果 ______ A. 相同 B. 第一次测量植比第二次大 C. 第一次测量植比第二次小 8．面接触型二极管适用于 ____ A. 高频检波电路 B. 工频整流电路 | 9．下列型号的二极管中可用于检波电路的锗二极管是： ____ A. 2CZ11 B. 2CP10 C. 2CW11 10．当温度为20℃时测得某二极管的在路电压为V U D 7.0=。若其他参数不变，当温度上 升到40℃，则D U 的大小将 ____ A. 等于 B. 大于 C. 小于 11．当两个稳压值不同的稳压二极管用不同的方式串联起来，可组成的稳压值有 _____ A. 两种 B. 三种 C. 四种 12．在图中，稳压管1W V 和2W V 的稳压值分别为6V 和7V ，且工作在稳压状态，由此可知输 出电压O U 为 _____ A. 6V B. 7V C. 0V D. 1V

三爱三节演讲稿600字

三爱三节演讲稿600字 我们生活在地球上，应该懂得哪些应该做，哪些不应该做的。“三爱三节”，你真的做到了吗？下面的文章是小编精心搜集出来的，欢迎阅读！ 三爱三节就是指爱祖国、爱劳动、爱学习、节约用水、节约用电、节约粮食。 作为祖国未来的接班人，我们要做到三节三爱。 我们要爱祖国，祖国是我们的母亲，她养育了我们，给了我们一个温馨的家，我们的祖国就像是一个大花园，而我们就是花园中的花朵，所以我们要爱祖国。我们要爱劳动，高尔基说过：“我们世界上最美好的东西，都是由劳动、由人聪明的手创造出来的。”所以，我们在学校里，要按时值日，打扫卫生，让我们的校园更加整洁美丽;在家里，要多帮妈妈干家务活，分担一些家务;我们要爱学习，因为只有好好学习才能成为一个对社会有用的人，报效国家;我们要节约用水，水是生命之源，没有了水，任何生物都生活不下去，而且，现在我国的一些地区还存在缺水的问题，所以，我们要节约每一滴水，不要让世界上的最后最后一滴水成为我们的眼泪;我们要节约用电，在学校里，风扇、电灯要及时关闭，在家里，当电器不用的时候，要及时把电源拔掉;我们要节约粮食，朱柏庐说过：“一粥一饭，当思来之不易;

半丝半缕，恒念物力维艰。” 所以，我们要珍惜粮食，它们都是农民伯伯用辛勤的汗水浇灌出来的。 我们只有一个祖国，我们应懂得珍惜，保护我们亲爱的祖国，让“三爱三节”传遍中国。 “锄禾日当午，汗滴禾下土，谁知盘中餐，粒粒皆辛苦。”这是唐朝诗人李绅写的悯农，它的意思可能大家都知道，农民伯伯务农很辛苦，每日早出晚归，所以大家要爱惜粮食，那大家都做到了吗? 据调查，每年我们浪费在家里的粮食足够1500万人吃一年，每年我们浪费在食堂里的粮食足够3000万人吃一年，每年浪费餐馆里的粮食足够2亿人吃一年。如果我们停止浪费，一年就可以省下约1000亿斤的粮食，这足够养活3。5亿人。 虽然我们现在生活在高速发展的现代社会，但是大家知道吗?当我们随手扔掉一块馒头的时候，我们是否想到世界上还有许多人正在为一餐饭而辛苦奔波。我们是否想到世界上有许多人正在为一餐而辛苦奔波，还有许多人正因饥饿而在死亡的边缘挣扎。以前我吃东西常常挑三拣四，吃不玩就随手扔掉，根本没有意识到自己在浪费，以为这不算什么。可是当我在电视上看到那些非洲难民因饥饿，瘦骨嶙峋·饥不择食，最饿死在街头那惨不忍睹的情景。还有我国的边远