From Distributed Memory Cycle Detection
to Parallel LTL Model Checking 1
J.Barnat,L.Brim,J.Chaloupka
Faculty of Informatics,Masaryk University,Brno,Czech Republic
Abstract
In [2]we proposed a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations.The algorithm employs back-level edges as computed by the breadth ?rst search.In this paper we describe how to turn the algorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles,counterexample generation and partial order reduction.We discuss these extensions and show experimental results.
Keywords:LTL model checking,breadth ?rst search,distributed memory
1Introduction
The model checking [10]became one of the most frequently used formal meth-ods in the ?eld of system veri?cation.In general,the model checking question asks whether an abstract model of the veri?ed system satis?es desired prop-erties that are expressed by means of temporal logics [16].
Unfortunately,all the known algorithmic solutions to the model checking problem su?er from large space requirements needed to answer the model checking question.These requirements are caused by the fact that the size of the state space of a model grows exponentially with the number of components in the system.Several attempts to address the state explosion by exploiting the aggregate memory of a network of workstations appeared recently (see e.g.[18,14,12,5,6]).
1Research supported by the Grant Agency of Czech Republic grant No.
201/03/0509Electronic Notes in Theoretical Computer Science 133 (2005) 21–39
1571-0661/$ – see front matter ? 2005 Elsevier B.V. All rights reserved.
https://www.doczj.com/doc/049927256.html,/locate/entcs
doi:10.1016/j.entcs.2004.08.056
In this paper we consider linear temporal logic (LTL),a major logic used in formal veri?cation.It is known for very e?cient sequential algorithms based on automata and successful implementation within several veri?cation tools.All the existing explicit state distributed memory approaches to LTL model checking ([4,7,1,15,9])are known to have various disadvantages and shortcomings that prevent each individual algorithm from being considered to be the clear winner.Therefore,the research on distributed memory LTL model checking remains a challenging and open task.
The optimal sequential solution to the LTL model checking problem is based on the depth ?rst search (DFS)traversal of the state space,in partic-ular the postorder as computed by DFS is crucial for cycle detection which is the core problem in LTL model checking.However,when exploring the state space in parallel,the DFS postorder is not generally maintained due to di?erent speeds of involved workstations.As a consequence,those algo-rithms that parallelize DFS based LTL model checking su?er from additional technical machinery that is necessary to maintain the DFS postorder in the distributed memory environment.In [2]we proposed a parallel graph algo-rithm for detecting cycles in very large oriented graphs distributed over a network of workstations.The main twist is that our new algorithm does not employ DFS postorder for cycle detection because it is based on the breadth ?rst search (BFS).It exploits the fact that every cycle has the most distant and the nearest vertex and that when traveling through any (nontrivial)cycle we have to “return back”to a vertex that is closer to the source at least once.Hence,a necessary condition for a path in a graph to form a cycle is that it contains such a back-level edge .Back-level edges are computed by BFS which can be (unlike DFS)reasonably parallelized.
In this paper we describe how to turn the graph algorithm into a real explicit state distributed memory LTL model checker by extending it with the detection of accepting cycles,counterexample generation and partial order reduction.
The rest of the paper is organized as follows.In the next section we recall the main ideas of the graph algorithm as given in [2].The following sections deal with accepting cycle detection,counterexample generation,and partial order reduction,respectively.In a separate section,we summarize the experimental evaluation of the algorithm.
2Detecting Cycles in Parallel
The algorithm given in [2]is designed to be performed on a network of work-stations.Its task is to decide whether there is a cycle in a distributed graph.
J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39
22
J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3923 A distributed graph is such a graph whose vertices are divided into as many disjoint sets as there are participating workstations.In particular,a parti-tion function is introduced to assign to each vertex a workstation the vertex belongs to(the workstation owns the vertex).The entire distributed compu-tation is started and terminated by one of the workstations involved.This distinguished workstation is called the manager.
The graph is supposed to be given implicitly,i.e.by an initial vertex and a function that for a given vertex returns its immediate successors.During the computation of the algorithm all the generated vertices of the graph are stored on the corresponding workstations.Thus each workstation keeps its own part of the distributed graph.If an exploration should proceed to a vertex that does not belong to the workstation,a message containing the vertex is sent to the workstation owning it and the local exploration of the vertex is skipped. The vertex is further processed by the destination workstation.
Before explaining the idea of the algorithm we recall the de?nition of a back-level edge.In short,a back-level edge is such an edge in the graph that does not increase the distance from the initial vertex.For simplicity,we assume that all vertices of the given graph are reachable.
De?nition2.1Let G=(V,E)be a graph with the initial vertex s and let u be an arbitrary vertex.The distance of the vertex u,denoted by d(u),is the length of the shortest path between s and u.An edge(u,v)∈E is called a back-level edge if and only if d(u)≥d(v).The set of all vertices with the same distance is referred to as a level.By Level k we denote the set of all vertices with the distance k,i.e.Level k={u∈V|d(u)=k}.
It is easy to see that for each cycle in the graph there is a maximal k such that the cycle contains a vertex from Level k.Moreover,any edge on the cycle leading from a vertex in Level k has to be a back-level edge.Since all vertices in the cycle have a successor it is obvious that each cycle in the graph contains at least one back-level edge.
The cycle detection algorithm works as follows.There are two proce-dures that the algorithm performs alternately.The task of the?rst procedure (henceforth called primary)is to?nd all the back-level edges by exploring the graph gradually level by level,while the task of the second procedure(hence-forth called nested)is to test each discovered back-level edge for being a part of a cycle.The primary procedure is implemented as a level synchronized breadth?rst search of the graph.As soon as a level is completely explored, the nested procedures are initiated for all the back-level edges emanating from a vertex on the current level(called current back-level edges)in order to detect cycles.Thus the goal of a nested procedure initiated for a back-level edge is
to hit the vertex from which the back-level edge emanates (called target ).If at least one nested procedure succeeds then the presence of a cycle is ensured and the algorithm is terminated.Otherwise,the primary procedure continues with the exploration of the next level.Each nested procedure searches for its target in a depth ?rst manner.Since there are many nested procedures per-formed concurrently,the target of each nested procedure has to be propagated by the procedure itself.Unlike the standard DFS,the vertices are not marked as visited and so may be revisited.Note that the search space of nested pro-cedures can be limited to the vertices that have already been visited by the primary procedure.
Obviously,the nested procedures may revisit some vertices many times.To prevent this we suggested several optimizations that decrease the revisiting factor fairly.The ?rst idea is to eliminate repeated visits that are made by the same nested procedure.For this purpose we store at each vertex the identi?cation (target)of the last nested procedure that walked through the vertex.If a nested procedure visits a vertex it has visited previously,it is not allowed to pass through it unless the vertex was visited by another nested procedure in the meantime.To illustrate the optimization let us consider the graph a )in Figure 1.It can be easily seen that the nested procedure initiated for the back-level edge (A,B )will visit the vertex G four times (along all the paths from B to G )without the optimization,but only twice (from E and F )if the optimization is considered.
Another optimization we suggested reduces vertex revisits that are made by di?erent nested procedures.In order to do so we introduced an ordering on the nested procedures induced by an ordering of their targets.At each vertex we store the identi?er of the highest nested procedure that passed through it.Only a procedure with higher identi?er is allowed to proceed through the vertex.This technique reduces revisiting of vertices quite a lot.Unfortunately,it breaks the cycle detection capability because a nested procedure that could reveal a cycle may be stopped before reaching its target.The situation is illustrated on the graph b )in Figure 1.Let us suppose an ordering in which A >F .If the nested procedure [A ](the one corresponding to the back-level edge (A,C )and having A as its target)reaches the vertex C before the nested procedure [F ]then the nested procedure [F ]is stopped at the vertex
C .However,the nested procedure [A ]continues through the vertices E,F,B to the vertex C where it ?nishes without revealing the cycle.
To address this problem we change the identi?cation of each nested proce-dure to a pair [T,n ]where T is the target vertex and n is the number of current back-level edges the procedure has passed through.Hence,the identi?cation is dynamically modi?ed as the procedure continues.We also need to rede?ne
J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39
24
a)
?>=<89:;B @@@@@@@@@?>=<89:;C @@@@@@@@@?>=<89:;D ~~~~~~~~~?>=<89:;E @@@@@@@@@?>=<89:;F ~~~~~~~~~?>=<89:;A
?>=<89:;G ?>=<89:;H b)?>=<89:;B ?>=<89:;C ?>=<89:;E ?>=<89:;A ?>=<89:;F c)?>=<89:;B ?>=<89:;C @@@@@@@@@?>=<89:;D ~~~~~~~~~?>=<89:;76540123E ~~~~~~~~~?>=<89:;F ?>=<89:;A ?>=<89:;G d)?>=<89:;B
?>=<89:;C
?>=<89:;76540123E
?>=<89:;A
?>=<89:;F Fig.1.Revisits reduction and accepting cycle detection
the ordering of the nested procedures.A nested procedure identi?ed as [A,x ]is less than a nested procedure identi?ed as [B,y ]if A F .There are two back-level edges on the current level and so there are two nested procedures initiated,namely [A,0]and [F,0].When they reach the vertex C they have both passed one current back-level edge.If the nested procedure [A,1]for the back-level edge (A,C )reaches the vertex C before procedure [F,1]for the back-level edge (F,B ),the latter one is stopped.In such a case the procedure for the back-level edge (A,C )con-tinues in exploration of the graph.When it visits the vertex C for the second time,its identi?cation is [A,2]which is obviously greater then [A,1]and so the procedure is not stopped and continues through the vertex C again.It J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–3925
goes through the vertices E and F and increases its number of passed current back-level edges when it reaches the vertex B .At that moment the number of passed current back-level edges by the procedure for the back-level edge (A,C )exceeds the total number of current back-level edges (which is two),the presence of a cycle is detected and the algorithm terminates.
We now focus our attention on the model checking problem and show how to turn the distributed memory cycle detection algorithm into an explicit state distributed memory LTL model checker by extending it with the detection of accepting cycles,counterexample generation and we show how to combine it with partial order reduction.
3Accepting cycles
The LTL model checking problem can be reduced to the language emptiness problem for B¨u chi automata [19].The given system is modeled by a sys-tem automaton with some states marked as accepting and the (negation of the)veri?ed LTL formula is transformed into a property automaton .The two automata are combined together to form a synchronous product automaton that is tested for the language emptiness.If the language of the automaton is empty then the model of the system satis?es the veri?ed property.In the other case the accepting run of the product automaton (so called counterexample )gives a behavior of the model that breaks the property.A B¨u chi automaton accepts an empty language if and only if there is no reachable accepting cycle in the corresponding graph.As regards the terminology we switch to a more convenient one and speak of states instead of vertices and transitions instead of edges whenever appropriate.
Unless under special circumstances,we cannot directly use the algorithm from [2]to detect the language emptiness of a B¨u chi automaton because the al-gorithm cannot distinguish between accepting and non-accepting cycles.Nev-ertheless,we can exploit the veri?ed property to decompose the examined graph into several components (each being a set of strongly connected compo-nents of the graph)to perform limited accepting cycle detection.In general,the components can be of one of the three types [11]:non-accepting,fully accepting,and partially accepting.A non-accepting component contains no accepting states,a fully accepting component contains accepting states only,and a partially accepting component contains both.It is obvious that as for the model checking,the accepting cycle detection need not be made in the non-accepting components of the graph at all and can be replaced by a sim-ple cycle detection in the fully accepting components of the graph.Since the types of components are completely determined by the veri?ed property we
J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39
26
J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3927 are able to precompute the decomposition of the product automaton easily in advance.In[2]we performed the LTL model checking on those graphs that were made of non-accepting or fully accepting components only.
The basic idea behind detection of accepting cycles in partially accepting components is to prevent the algorithm from detecting non-accepting cycles. For this purpose each nested procedure maintains an additional(accepting) bit to indicate that it has passed through an accepting state since its last pass through a current back-level edge.In particular,this accepting bit is set to true whenever the procedure reaches an accepting state and is set to false whenever the procedure passes a current back-level edge.The bit is set to false initially.
There are two ways the algorithm detects a cycle:by hitting the target of the procedure or by exceeding the number of current back-level edges.To prevent a nested procedure from exceeding the number of current back-level edges on a non-accepting cycle we modify the nested procedure to count a current back-level edge only if the accepting bit is set to true.As regards the ?rst way(hitting the target),we modify the nested procedure to report a cycle only if it reaches the target state and the bit is set to true.The pseudo-code of procedure Search-for-accepting-cycle is given in Figure2.
We demonstrate the behavior of the procedure on the graphs b)and d)in Figure1.The nested procedure for back-level edge(A,C)arrives at state C as a procedure[A,0]because A is not an accepting state and the accepting bit is initially set to false which means that the procedure does not increase its counter of passed back-level edges when it passes the edge(A,C).Similarly, the nested procedure for back-level edge(F,B)arrives at state B as procedure [F,0].
Let us?rst assume that procedure[F,0]arrives at state C before procedure [A,0]or that A Let us assume now that A>F and procedure[A,0]arrives at state C before procedure[F,0]does.In such a case procedure[F,0]is stopped when it arrives at state C,while procedure[A,0]continues in the search.In the case of the graph b)procedure[A,0]passes current back-level edge(F,B) without increasing its counter of passed current back-level edges because its accepting bit remains set to false.This means that the procedure does not change its identi?cation and so it is stopped when it arrives at state C for the second time.In the case of the graph d)the[A,0]procedure sets its proc Search-for-accepting-cycles (nmbrbl ) while (?Synchronize ()∨BBLQ =?)do if (BBLQ =?) then (q ,prelevel ,target ,bl ,abit ):=dequeue (BBLQ ); if d (q ) then if (IsAccepting (q )) then abit :=true ? if (q =target ∧abit =true ) then Accepting-Cycle-Detected() ? if (prelevel =Level ?1∧abit =true ) then bl :=bl +1 abit :=false if (bl >nmbrbl ) then Accepting-Cycle-Detected() ? ? if ((Level ?1>q .level )∨ (Level ?1=q .level ∧ (target >q .target ∨ (target =q .target ∧bl >q .bl )∨ (target =q .target ∧bl =q .bl ∧ abit >q .abit )))) then q .target :=target q .bl :=bl q .level :=Level ?1 q .abit :=abit foreach t ∈Successors (q )do if (Owner (t )=WorkstationId ) then Send message to Owner (t ): enqueue (BBLQ , (t,d (q ),target ,bl ,abit ))) else push (BBLQ , (t,d (q ),target ,bl ,abit )) ? od ? ? ? od end Fig.2.Improved procedure Check-BL-edges with accepting cycle detection J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39 28 J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3929 accepting bit to true when it passes the accepting state E which allows the procedure to increase its counter of passed back-level edges when it passes the back-level edge(F,B).Note that the accepting bit is reset to false when the counter is increased.The procedure then arrives at state C for the second time being identi?ed as[A,1].This means that the procedure is not stopped but it continues in the search.At state E it sets its accepting bit to true and passes the back level-edge(F,B)changing its identi?er to[A,2].Then it goes through state C for the third time.At the state E it sets the accepting bit to true again and after passing the back-level edge(F,B)it exceeds the number of current back-level edges.Hence,the existence of an accepting cycle is correctly detected. Note that if the algorithm is modi?ed to detect accepting cycles only,it may happen that there are non-accepting cycles that are completely above the current level.See the cycle B,D,B in the graph c)in Figure1.However, these non-accepting cycles do not in?uence the cycle detection at all because they have neither accepting states nor current back-level edges.Finally,note that there may be accepting cycles that cannot be detected by the?rst way of cycle detection(i.e.by hitting the target).Let us consider the graph c) from Figure1and an ordering in which G>A.The nested procedure[A,0] is stopped at state G because[A,0]<[G,0].The nested procedure[G,0] sets its accepting bit to true at state E and so turns itself into[G,1]when passing the back-level edge(A,C).Hence,whenever it arrives at its target its accepting bit is set to false.Therefore,in this case the cycle will be detected by procedure[G,3]at state C by exceeding the number of current back-level edges. Theorem3.1The accepting cycle detection algorithm always terminates and reports the presence of an accepting cycle if and only if there is an accepting cycle in the product automaton graph. The proof exploits the correctness of the algorithm for distributed back-level edge detection as presented in[2].In addition,several facts have to be taken into account.If there is an accepting cycle in the graph then at least one (shallowest)cycle is explored completely by a nested procedure because either all queues BBLQ are emptied before the next level of the graph is processed or the presence of an accepting cycle is reported.Another important fact is that no nested procedure can pass through a non-accepting cycle in?nitely many times.For a more detailed proof see the full version of the paper[3]. 4Counterexample Generation Model checking algorithms should be able to provide the user with a counterex-ample in the case the veri?ed property is violated.In general,the computed counterexamples can be quite long which might make it di?cult to locate an error.Thus computing the shortest possible counterexample greatly facilitates the debugging process.In this section we present a technique to generate short counterexamples. A counterexample consists of two parts:an accepting cycle and a path that reaches it from the initial state s .In the sequential Nested DFS algorithm,the counterexample is simply generated by following the DFS search stacks:the DFS stack of the nested search is used to reconstruct the accepting cycle while the DFS stack of the primary search gives a path to it.However,in our algorithm we do not have any DFS search stacks,hence a di?erent approach has to be considered. Recall that our algorithm uses,similarly to the Nested DFS,two search procedures.Unlike the Nested DFS,the primary search is a breadth ?rst search.Both search procedures build parent graphs that are utilized for coun-terexample generation. More precisely,for each vertex v the value par (v )is stored during the primary search which is the parent of the vertex v in the search (called BFS parent).Note that it is assigned only once during the whole computation.In addition,we also store the value par -dfs (v )which is the parent of the vertex v in a nested search (called DFS parent).It is assigned every time a nested procedure is allowed to pass through the vertex.In both cases,the parents induce edges in the following way.If v is a vertex and par (v )is the BFS parent of v ,then (v,par (v ))is the induced edge in the BFS parent graph ,similarly the DFS parents de?ne the DFS parent graph .In the following we show how the counterexample can be found by traversing the BFS and DFS parent graphs. The accepting cycle part of a counterexample is generated using the DFS parents.Once the existence of an accepting cycle in the graph is detected,one could be tempted to follow the DFS parents back to and through the cycle.However,due to the fact that several nested procedures can be run in parallel,a vertex can be visited several times each time changing its DFS parent.As a result,the DFS parent graph may not contain a cycle even though the input graph contains a cycle.A possible situation is exempli?ed in Figure 3.Suppose the ?rst nested procedure starts from the vertex F and the DFS parent graph is build as the procedure continues (see Figure 3.a).Suppose that after the procedure passes through the vertex C the second nested search J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39 30 a)?>=<89:;B ?>=<89:;C ?>=<89:;E ?>=<89:;A ?>=<89:;F b)?>=<89:;B ?>=<89:;C ?>=<89:;E ?>=<89:;A ?>=<89:;F Fig.3.Interrupting a cycle in the DFS parent graph which has been started from the vertex A visits the vertex C before the ?rst procedure actually closes the cycle.Further suppose that A >F .When exploring the vertex C by the second procedure,the DFS parent for C is reset to point to the vertex A ,hence the possible cycle in the DFS parent graph is interrupted (see Figure 3.b). To solve this problem we assign to the nested search that detected the cycle a new (highest)identi?cation and we re-execute it independently.In our example in Figure 3we start the nested search from the vertex F once more,the second search from A is not performed. During the generation of the counterexample the manager workstation is used as a “collector”to which all the workstations participating in the gen-eration send information.Note that the vertices forming a counterexample are spread across the network according to the partition function.The coun-terexample is generated in two steps.In the ?rst one the DFS parent graph is traversed starting at the state where the cycle was detected.The visited vertices are marked in order to discover the cycle.Once an already marked vertex is visited,the cycle can be reconstructed from the vertices that have been sent and saved on the manager workstation.Moreover,the manager is able to determine the vertex v with the smallest distance on the cycle.In the second step of the generation the BFS parents are traversed from v back to the initial vertex of the graph.After ?nishing the second step,the whole coun-terexample can be put together using the information stored on the manager workstation. A signi?cant positive feature of our algorithm is related to the length of counterexamples it provides.Since the algorithm is primarily based on breadth ?rst search exploration,the counterexamples tend to be short.See the section on experiments for a few examples. J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–3931 5Partial Order Reduction In this section we describe how to combine partial order reduction with our distributed memory algorithm.We start by a brief review of the partial order reduction method following mainly the presentation of [10]before explaining the proposed distributed approach. To describe partial order reduction method it is not su?cient to use graphs as the semantical models.The concurrent systems that we analyze are mod-eled in a more appropriate way as state transition systems (labeled transition systems).If S is the set of states ,a transition is a relation α?S ×S .A state transition system is then de?ned as a tuple M =(S,s 0,T,L ),where s 0∈S is an initial state ,T is a set of transitions α?S ×S ,and L :S →2AP is a labeling function that assigns to each state a subset of some set AP of atomic propositions . A transition α∈T is enabled in a state s if there is a state s such that α(s,s ).The set of all transitions enabled in a state s is denoted enabled(s).We presuppose that transitions are deterministic,i.e.,for every αand s there is at most one s with α(s,s ),and denote it as α(s )=s .If α(s,s )we say that s is a successor of s . The partial order method exploits the fact that concurrent transitions can be interleaved in either order.This can be formalized by de?ning an indepen-dence relation on pairs of transitions. An independence relation I ?T ×T is a symmetric,anti-re?exive relation,satisfying the following two conditions for each state s ∈S and for each (α,β)∈I : (i)Enabledness –If α,β∈enabled (s )then α∈enabled (β(s )). (ii)Commutativity –If α,β∈enabled (s )then α(β(s ))=β(α(s )). The dependency relation is the complement of I .Heuristic methods are uti-lized for an e?cient computation of a dependence relation according to the conditions mentioned above. The independence relation suggests a potential reduction to the state tran-sition system by selecting only one from the independent transitions originat-ing from a state s .However,this cannot guarantee that the reduced state transition system is a correct replacement of the full one as it does not take into account the property to be checked.Also,eliminating one of the in-termediate states α(s )or β(s )may cause some of its successors (which are signi?cant for veri?cation)not to be explored.Additional conditions for the correctness of the reduction are needed.They are described in the following. First,we make it precise what it means that a property is taken into J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39 32 J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3933 account by de?ning the concept of visibility of a transition. A transitionα∈T is invisible with respect to a set of propositions AP ?AP if for each pair of states s,s ∈S such thatα(s,s ),L(s)∩AP =L(s )∩AP holds.A transition is visible if it is not invisible.The set AP is usually induced by the set of atomic propositions included in the veri?ed formula. The reduced state transition system is generated by a modi?ed generation algorithm which explores only a subset of transitions,enabled at each state encountered during the generation,called an ample set.The ample set can be de?ned in a manner that does not depend on the particular way the state transition system is generated.This is accomplished by a set of conditions relating the full state transition system to the corresponding reduced one. Note that there could be more than one ample set satisfying the conditions for a given state.We say that a state s is fully expanded whenever ample(s)= enabled(s). Let AP be a set of atomic propositions.Ample conditions with respect to the set AP are: C0ample(s)=?if enabled(s)=?. C1Along every path in the full state graph M that starts at s,the following condition holds:a transition that is dependent on a transition in ample(s) cannot be executed without a transition in ample(s)occurring?rst. C2If enabled(s)=ample(s),then everyα∈ample(s)is invisible w.r.t.to AP . C3(cycle closing condition)A cycle in the reduced state graph M R is not allowed if it contains a state in which some transitionαis enabled,but is never included in ample(s)for any state s on the cycle. The conditions characterize the ample sets needed to generate reduced state transition systems su?cient for checking safety and liveness properties. Our aim is to combine partial order reduction with our distributed memory algorithm.The reduced system is computed by a generation algorithm which systematically explores states in such a way that for every state s it chooses a set ample(s)?enabled(s)and follows the transitions from ample(s)only.The key part of such an algorithm is without any doubts the distributed memory checking of the ample conditions. While checking the conditions C0and C2is easy and can be done locally, checking conditions C1and C3is as hard as solving the reachability prob-lem.Nevertheless,the condition C1can be checked locally using the same approximating heuristics as in the sequential case(see[10]).Therefore,the cycle closing condition C3is the only one which is di?cult to be checked in a distributed environment.In the sequential case when exploring the state graph by depth ?rst search ,the condition C3is checked in constant time us-ing the search stack .In fact,the following stronger condition is used instead of C3. C3-dfs If a state s is not fully expanded,then no transition in ample (s )leads to a state on the search stack. Our aim is to develop a counterpart of the condition C3-dfs for the breadth ?rst search based generation of the state transition system which is distributed among several workstations.A new proviso is motivated by the fact that a necessary condition for closing a cycle in breadth ?rst search is that the state closing the cycle has already been visited during the search.Hence,we use the following cycle closing condition which can be easily checked. C3-bfs If a state s is not fully expanded,then ample (s )does not contain a back-level edge,i.e.a transition that leads to a state that is on the current or previous level of the breadth ?rst search. To utilize partial order reduction within our distributed memory on-the-?y algorithm we use the similar approach as implemented e.g.in the model checker SPIN [13].The approach combines the construction of the state space with checking that it satis?es the speci?cation by exploring the product graph.The only condition that needs attention is obviously the cycle condition C3-bfs .It can be shown that it is correct to check the condition with respect to cycles of the product.We have implemented the method and experimentally con?rmed reductions in space and time. 6Experimental evaluation We implemented the algorithm from scratch,thus the implementation misses many optimizations commonly used in standard sequential tools (e.g.SPIN).In particular,our implementation of the partial order reduction is quite far from being optimal.For comparison reasons we implemented the Nested DFS algorithm without any optimizations as well.All the experiments were con-ducted on a homogeneous network of twelve workstations interconnected by 100Mbps switched Ethernet.Each workstation was equipped with an Intel Pentium 42.6GHz CPU and 1GB RAM. We measured the performance of the algorithm on various model checking problems,each given by a model and a formula.The models include Elevator model (elev),Leader election protocol (lead),Peterson solution for mutual exclusion (pet),Dinning philosophers problem (phil),and RealTime Ethernet protocol (rte).All the models were parametrized:Elevator by the number of served ?oors,Leader election,Peterson,and Philosophers by the number of J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39 34 Problem Model(M)Veri?ed property(?)M ? |=? elev1Elevator G(r1=?(?p1U(p1U(p1∧o))))no elev2Elevator G(r1=?(?p1U(p1U(?p1U(p1U(p1∧o))))))yes lead1Leader election FG(one leader)yes lead2Leader election F(more leaders)no pet1Peterson G(p0in cs=?F(?p0in cs))yes pet2Peterson G(?p0in cs=?F(p0in cs))no pet3Peterson-error GF(someone in cs)no phil1Philosophers GF(phil0eats)no phil2Philosophers GF(someone eats)yes rte1RT Ethernet G(r0=?(?ce U(ce U(?ce∧(rt0R?ce)))))yes rte2RT Ethernet G(w0=?(?ce U(ce U(?ce∧(rt0R?ce)))))no Fig.4.Models and veri?ed properties participating processes,and RT Ethernet by the number of network nodes. For each model we veri?ed a few LTL formulas trying to cover both cases,i.e. the case when the model satis?es the formula and the case it does not.See the table in Figure4for the list of model checking problems we used. The table in Figure5shows the lengths of the generated counterexamples for selected model checking problems.The column“Counterexample Length”gives the lengths of the counterexamples as produced by our algorithm while the column“Counterexample Length(NDFS)”gives the lengths of counterex-amples as produced by the Nested DFS algorithm.It can be seen that our algorithm produces signi?cantly shorter counterexamples than the standard Nested DFS does.On the other hand,the time needed by the Nested DFS al-gorithm to discover and generate a counterexample is shorter in general.The di?erence is obviously caused by the fact that our algorithm explores many more states in comparison to the Nested DFS algorithm before it discovers an accepting cycle.Time in seconds needed to generate the counterexamples is given in the same table. Other experiments were performed to evaluate the partial order reduction based on the condition C3-bfs.See the table in Figure6.We measured the number of states in the full graph(the column“no POR”)and the number of states in the reduced graph(the column“POR”).In addition,we measured the number of states in the graph that was reduced by the standard partial order reduction as given in[10](the column“POR-DFS”).This value was measured using the standard sequential DFS algorithm(“—”means the algo-rithm exceeds the available memory).Note that a reduction was achieved only J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3935 Problem Counterexample Length Counterexample Length (NDFS)Time Time (NDFS)elev1(9) 853231361elev1(10) 653565271lead2(4) 747431lead2(5) 9292691pet2(3) 396311pet2(4) 8512871pet3(4) 1221511pet3(5) 1262511phi1(12) 5411611phi1(13) 51857911phi1(14) 51857912phi1(15) 51207301635rte2(9) 20717478544rte2(10)244605207618 Fig.5.Counterexample length and generation time Problem Number of states no POR Number of states POR Number of states POR-DFS elev2(10) 111306211130621113062lead1(4) 1105376068160681lead1(5) 362901114878911487891pet1(3) 242923351815pet1(4) 132104130965103963pet1(5) 95161429478643—phi2(12) 847653847653847653phi2(13) 24685482468548—rte1(10)575927757592775759277 Fig.6.Partial Order Reduction on the Leader election and the Peterson models.While the reduction based on C3-bfs condition was the same as the standard partial order reduction in the case of Leader election model,it was slightly worse in the case of Peterson model. Finally,we measured the impact of the suggested partial order reduction J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39 36 J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3937 on the counterexample generation.The table in Figure7shows counterex-ample lengths(“CE Length”),time needed to generate them(“Time”),and the deepest levels that were reached during the veri?cation(“Level”).It can be seen that if the partial order reduction is employed then the shallowest accepting cycles may get slightly deeper.This may increase the number of states that are explored by the algorithm before an accepting cycle is discov-ered and the time needed to discover and generate the counterexample(see the row pet2(4)).Nevertheless,the impact of the partial order reduction on the lengths of counterexamples is generally minimal. Problem CE Length CE Length(POR)Time Time(POR)Level Level(POR) lead2(4)7474337373 lead2(5)929269619191 pet2(3)3938112021 pet2(4)858973943133 pet3(4)12141179 pet3(5)121511710 Fig.7.Impact of partial order reduction on counterexample generation 7Conclusions and Related Work We proposed an extension of the algorithm presented in[2]to a full LTL model checking algorithm without loosing any of its positive features.In particular, we show how to detect accepting cycles,generate counterexamples,and how to employ partial order reduction. As expected the counterexamples were very short compared to those re-turned by the Nested DFS algorithm.This is due to the breadth?rst like nature of the state space generation.However,the time to?nd the counterex-ample was generally longer and more states had to be explored.We stress that the shortness of a counterexample is crucial in debugging. Another positive feature of the algorithm is its behavior on graphs with a small number of back-level edges.In such cases the behavior of our algorithm for the full LTL model checking practically equals to the reachability analysis. There were several models con?rming this. On the other hand,there are several drawbacks associated with the breadth ?rst approach.We have mentioned it may generally take more time to?nd a counterexample.Furthermore,the Nested DFS algorithm is sometimes able to?nd an error in extremely large graphs,while our algorithm can succeed only if the error is not“far”from the initial vertex in these cases.Another drawback arises when the graph contains many back-level edges.Moreover,if the graph does not contain an accepting cycle,it must be fully explored,and frequent revisiting of states causes the time of the computation to be much longer than the time of a simple reachability analysis. As ?rstly argued in [14]the partial order reduction technique exploiting the C3-dfs condition is hardly transformed to the distributed memory state space generation.On the other hand,the reduction achieved by our algorithm combined with the C3-bfs condition is in many cases practically comparable to the reduction in the standard sequential Nested DFS algorithm.Of course,in some cases the C3-bfs is too weak to give a signi?cant reduction.In [17]the distributed algorithm Twophase is proposed.In contrast to the sequential Nested DFS algorithm algorithm,Twophase is much simpler as it works only with singleton ample sets,i.e.,whenever there is no singleton satisfying the ample conditions,the state is fully expanded.We have not compared our al-gorithm directly to the Twophase algorithm.Recently,yet another approach to partial order reduction in distributed environment has been proposed in [8].The technique is used to generate reduced state space,however it is not pos-sible to combine it directly with on-the-?y breath ?rst search algorithms. The distributed counterexample generation (if considered)is typically per-formed as two reachability procedures:the ?rst one localizes a reachable vertex on an accepting cycle,while the second one generates the cycle.BFS parent graph have been used for the ?rst search in [9,7]. References [1]J.Barnat,L.Brim,and I.ˇCern′a .Property Driven Distribution of Nested DFS.In M.Leuschel and U.Ultes-Nitsche,editors,Proceeding of the 3rd International Workshop on Veri?cation and Computational Logic (VCL’2002),pages 1–10,October 2002. [2]J.Barnat,L.Brim,and J.Chaloupka.Parallel Breadth-First Search LTL Model-Checking.In 18th IEEE International Conference on Automated Software Engineering (ASE’03),pages 106–115.IEEE Computer Society,Oct.2003. [3]J.Barnat,L.Brim,and J.Chaloupka.Distributed Memory LTL Model-Checking Based on Breadth First Search.Technical Report FIMU-RS-2004-07,Faculty of Informatics,Masaryk University Brno,2004. [4]J.Barnat,L.Brim,and J.Stˇr ′?brn′a .Distributed LTL Model-Checking in SPIN.In Matthew B.Dwyer,editor,Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN’2001),volume 2057of LNCS ,pages 200–216,Toronto,Canada,2001.Springer-Verlag. [5]G.Behrmann.A performance study of distributed timed automata reachability analysis.In Proc.Workshop on Parallel and Distributed Model Checking ,volume 68of Electronic Notes in Theoretical Computer Science .Elsevier Science Publishers,2002. [6]B.Bollig,M.Leucker,and M.Weber.Parallel model checking for the alternation free μ-calculus.In Tiziana Margaria and Wang Yi,editors,Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01),volume 2031of LNCS ,pages 543–558.Springer-Verlag,2001. J.Barnat et al./Electronic Notes in Theoretical Computer Science 133(2005)21–39 38 J.Barnat et al./Electronic Notes in Theoretical Computer Science133(2005)21–3939 [7]L.Brim,I.ˇCern′a,P.Krˇc′a l,and R.Pel′a nek.Distributed LTL model checking based on negative cycle detection.In Ramesh Hariharan,Madhavan Mukund,and V.Vinay,editors, Proceedings of Foundations of Software Technology and Theoretical Computer Science(FST–TCS’01),volume2245of LNCS,pages96–107.Springer Verlag,2001. [8]L.Brim,I.ˇCern′a,P.Moravec,and J.ˇSimˇs a.Distributed partial order reduction of state spaces.In Proceedings of the3rd International Workshop on Parallel and Distributed Methods in Veri?cation(PDMC’04).To appear. [9]I.ˇCern′a and R.Pel′a nek.Distributed explicit fair cycle detection.In Thomas Ball and Sriram K.Rajamani,editors,Model Checking Software,10th International SPIN Workshop, volume2648of LNCS,pages49–73.Springer-Verlag,2003. [10]E.M.Clarke,O.Grumberg,and D.A.Peled.Model Checking.The MIT Press,Cambridge, Massachusetts,1999. [11]S.Edelkamp,A.Lluch-Lafuente,and S.Leue.Directed model-checking in HSF-SPIN.In Matthew B.Dwyer,editor,8th International SPIN Workshop,number2057in LNCS,pages 57–79.Springer,2001. [12]H.Garavel,R.Mateescu,and I.M Smarandache.Parallel State Space Construction for Model- Checking.In Matthew B.Dwyer,editor,Proceedings of the8th International SPIN Workshop on Model Checking of Software(SPIN’2001),volume2057of LNCS,pages216–234,Toronto, Canada,2001.Springer-Verlag. [13]G.J.Holzmann.The Model Checker SPIN.IEEE Transactions on Software Engineering, 23(5):279–295,May1997.Special issue on Formal Methods in Software Practice. [14]F.Lerda and R.Sisto.Distributed-memory model checking with SPIN.In Proceedings of the 6th International SPIN Workshop on Model Checking of Software(SPIN’99),volume1680of LNCS,pages22–39.Springer-Verlag,1999. [15]A.Lluch-Lafuente.Simpli?ed distributed model checking by localizing cycles.Technical Report176,Institute of Computer Science at Freiburg University,2002. [16]Z.Manna and A.Pnueli.The Modal Logic of Program.In Proceedings of the6th International Colloquium on Automata,Languages,and Programming(ICALP1979),volume71of LNCS, pages385–409.Springer-Verlag,1979. [17]R.Palmer and G.Gopalakrishnan.Partial order reduction assisted parallel model-checking (full version).Technical report,University of Utah,August,2002. [18]U.Stern and D.L.Dill.Parallelizing the mur?veri?er.In O.Grumberg,editor,Proceedings of Computer Aided Veri?cation(CAV’97),volume1254of LNCS,pages256–267.Springer-Verlag,1997. [19]M.Y.Vardi and P.Wolper.An automata-theoretic approach to automatic program veri?cation (preliminary report).In Proceedings1st Annual IEEE Symp.on Logic in Computer Science, LICS’86,Cambridge,MA,USA,16–18June1986,pages332–344.IEEE Computer Society Press,Washington,DC,1986. 第二章蛋白质的结构与功能 蛋白质元素组成：C、H、O、N、S。 特点：各种蛋白质含氮量接近，平均为16% 100克样品中蛋白质含量（g%）=每克样品含氮克数×6.25×100 氨基酸：蛋白质的基本组成单位，蛋白质是高分子化合物，可以受酸、碱或蛋白酶作用水解为氨基酸。 分类：①非极性侧链氨基酸 ②极性中性侧链氨基酸 ③酸性氨基酸（含有两个羧基）（谷氨酸、天冬氨酸） ④碱性氨基酸（含有两个以上氨基）（精氨酸、赖氨酸、组氨酸） 通式：组成人体的氨基酸均为L构型（L—α—氨基酸，氨基在左侧） D构型（D—α—氨基酸，氨基在右侧） 氨基酸之间通过肽键连接。 蛋白质的一级结构：在蛋白质分子中，从N—端至C—端的氨基酸排列顺序称为蛋白质的一级结构。 胰岛素一级结构：胰岛素由51个氨基酸残基组成，3个二硫键（在A6与A11、A20与B19、A7与B7号半胱氨酸之间）。 蛋白质二级结构连接键：氢键。 形式：α—螺旋：①多肽链主链以肽单元为单位。 ②螺旋每圈含3.6个氨基酸残基。 ③螺旋中的每个肽键的亚氨基氢和第四个肽键的酰基氧相互靠近形成氢键。 ④各氨基酸残基的R集团伸向螺旋外侧。 Β—折叠：①多肽链呈伸展状态。 ②两段以上的β—折叠结构平行排列，它们之间靠链间肽键的酰基氧与亚氨基氢形成氢键。 ③两条肽链的走向可以相同，也可以相反。 ④R基团交错伸向锯齿状结构的上下方。 Β—转角和无规则卷曲。 蛋白质三级结构：由一条多肽链构成的蛋白质，具有三级结构才能发挥生物学火性。 连接键：次级键。 蛋白质四级结构：指蛋白质分子中各亚基的空间排布及亚基接触部位的相互作用。 亚基：每一条多肽链都有完整的三级结构，称为亚基，亚基与亚基之间呈特定的三维空间排布，并以非共价键相连接。 等电点：净电荷为零，呈兼性离子状态，此时溶液的pH值称为该蛋白质的等电点。 蛋白质胶体性质的稳定因素：蛋白质表面的水化膜和电荷的排斥作用使蛋白质不易聚沉，稳定地分散在水中，成为稳定的亲水胶体。 蛋白质变性：在某些物理或化学因素作用下，蛋白质的空间结构受到破坏，从而导致其理化性质的改变和生物学活性的丧失（主要是二硫键和非共价键的破坏，不涉及一级结构的改变）。 改变：溶解度降低，黏度增加，结晶能力消失，生物学活性丧失，易被蛋白酶水解，光吸收性增加，分子不对称性增加。 因素：加热、乙醇等有机溶剂、强酸、强碱、重金属离子及生物碱试剂等。 第 22 次课 2 学时 注：本页为每次课教案首页 2,4,6,7,8 《生物化学》科学出版社 现代生物学精要速览中文版 王镜岩等译 高等教育出版社 罗纪盛等 第十章糖代谢(2) Glycometabolism 二、柠檬酸循环(TCA，1953年获得诺贝尔奖) ?EMP：G--------→2丙酮酸(在细胞浆中) ?丙酮酸进线粒体－－→乙酰CoA ?TCA：乙酰CoA进入TCA(在线粒体基质中) ?电子传递水平磷酸化(在线粒体内膜上) 1.EMP G--------→2丙酮酸 ●净得2ATP ●得2NADH+H+ 2. TCA(柠檬酸循环、三羧酸循环第92页) tricarboxylic acid cycle) Krebs循环 有氧条件下，将酵解作用产生的丙酮酸氧化脱羧成乙酰CoA，再经一系列氧化和脱羧，最终 生成二氧化碳和水并产生能量。 2 丙酮酸 + 2 GDP + 2 Pi + 4 H2O + 2 FAD + 8 NAD --------→6 CO2 + 2 GTP + 2 FADH2 + 8 NADH＋H＋ ?化学历程 ?能量计量 ?调控 ?生物学意义 三羧酸循环的发现历史 Albert Szent Gyorgyi观察用丙酮酸与肌肉组织一起在有氧条件下保温，丙酮酸可以被彻底氧化，生成二氧化碳和水。因此认为葡萄糖或糖原的有氧分解也循着糖酵解途径，有氧分解可以说是无氧分解的继续。 H. Krebs通过总结大量的实验结果，认为糖的氧化过程不是直线进行的，而是以循环方式进行。于是他于1937年提出了三羧酸循环假设并用实验证明了三羧酸循环的存在。 (1)化学历程 TCA循环的准备阶段：丙酮酸--→乙酰CoA TCA循环阶段： ①准备阶段(丙酮酸进入线粒体－－→乙酰CoA) 丙酮酸 + CoA-SH + NAD+→ Acetyl-CoA + CO2 + NADH + H+ 丙酮酸脱氢酶复合体系 有三种酶组成：三种酶均以二聚体的形式存在。 ?E1——丙酮酸脱氢酶(24条肽链) ?E2 ——二氢硫辛酸转乙酰基酶(24条肽链) ?E3——二氢硫辛酸脱氢酶(12条肽链) 砷化物：可与E2－SH共价结合，使酶失去活性。 练习题 ●糖酵解的终产物是丙酮酸 ●糖酵解的脱氢步骤反应是 ( ) 1.简述脂类的消化与吸收。 2.何谓酮体？酮体是如何生成及氧化利用的？ 3.为什么吃糖多了人体会发胖（写出主要反应过程）？脂肪能转变成葡萄糖吗？为什么？ 4.简述脂肪肝的成因。 5.写出胆固醇合成的基本原料及关键酶？胆固醇在体内可的转变成哪些物质？ 6.脂蛋白分为几类？各种脂蛋白的主要功用？ 7.写出甘油的代谢途径？ 8.简述饥饿或糖尿病患者，出现酮症的原因？ 9．试比较生物氧化与体外物质氧化的异同。 10．试述影响氧化磷酸化的诸因素及其作用机制。 11．试述体内的能量生成、贮存和利用 12．试从蛋白质营养价值角度分析小儿偏食的害处。 13．参与蛋白质消化的酶有哪些？各自作用？ 14．从蛋白质、氨基酸代谢角度分析严重肝功能障碍时肝昏迷的成因。 15．食物蛋白质消化产物是如何吸收的？ 16．简述体内氨基酸代谢状况。 17．1分子天冬氨酸在肝脏彻底氧化分解生成水、二氧化碳和尿素可净生成多少分子ATP？简述代谢过程。 18．简述苯丙氨酸和酪氨酸在体内的分解代谢过程及常见的代谢疾病。 19．简述甲硫氨酸的主要代谢过程及意义。 20．简述谷胱甘肽在体内的生理功用。 21．简述维生素B6在氨基酸代谢中的作用。 22．讨论核苷酸在体内的主要生理功能 23.简述物质代谢的特点？ 24.试述丙氨酸转变为脂肪的主要途径？ 25．核苷、核苷酸、核酸三者在分子结构上的关系是怎样的？ 26．参与DNA复制的酶在原核生物和真核生物有何异同？ 27．复制的起始过程如何解链？引发体是怎样生成的？ 28．解释遗传相对保守性及其变异性的生物学意义和分子基础。 29．什么是点突变、框移突变，其后果如何？ 30.简述遗传密码的基本特点。 31.蛋白质生物合成体系包括哪些物质，各起什么作用。 32．简述原核生物基因转录调节的特点。阻遏蛋白与阻遏机制的普遍性。33．简述真核生物基因组结构特点。 34．同一生物体不同的组织细胞的基因组成和表达是否相同？为什么？35．简述重组DNA技术中目的基因的获取来源和途径。 36．作为基因工程的载体必须具备哪些条件？ 37．什么叫基因重组？简述沙门氏菌是怎样逃避宿主免疫监视的？38．简述类固醇激素的信息传递过程。 39．简述血浆蛋白质的功能。 40．凝血因子有几种？简述其部分特点？ 41．简述红细胞糖代谢的生理意义。 42．试述维生素A缺乏时，为什么会患夜盲症。 43．简述佝偻病的发病机理。 44．维生素K促进凝血的机理是什么？ 食品添加剂的现状和发展趋势 食品添加剂是指在食品或食品加工中使用的各种微量的物质，通常其添加量不超过食品质量的2％。添加目的为：①改进和保持食品的营养价值；②延长食品的货架期；③方便食品的加工；④增强食品的风味，改变食品的色泽；⑤确保微生物的安全性；⑥保持食品品质的连续性和统一性。 1、食品添加剂市场 据统计，目前全球开发的食品添加剂总数已达1．4万多种，其中直接使用的品种有300o余种，常的有680余种。美国是世界上食品添加剂便用量最大、使用品种最多的国家．目前允许直接使用的有230o种以上，消费量已超过14o万吨（不包括淀粉及其衍生物、香精/香料和调味料）；西欧消费量已近50075~，其中淀粉及其衍生物的数量高达40万吨。 食品添加剂已．成为医药、农用化学品及饲料添加剂之后的第四类倍受人们关注的精细化工行业。目前食品添加剂的世界市场价值为200亿美元，其中，调味品占30~，4、氢化胶体占17％、酸化剂占13％、调味增强剂占12％、甜味剂占6％、色素占5％、乳化剂占5％、维生素和矿物质占5％、酶占4％、化学防腐剂占2％、抗氧化剂占1％。j负计禾来5年内冥年增长率为2％-3％。全球调味品和香料的市场价值为12o亿美，其中调味品约占49％（59亿美元）。调味品市场中，饮料占31％、佐料占23％、奶制品占14％、其他占32％。需求增长最强劲的食品添加剂将是维生素、矿物质、调味增强剂和脂肪代用品。 罗氏（R.h）和巴斯夫公司是世界上重要的食品添加剂和精细化学品生产商。维生素是罗氏公司维生素和精细化学品部最大的业务部门，几乎占全球销售额的50％，其次是精细化学品占30％、类胡萝卜素占20％。罗氏新上市的营养药品包括用于眼科保健的玉米黄质、番茄红素和叶黄素，以及供功能饮料用的水溶性维生素E制品等。罗氏公司也加快投资中国市场，与上海新亚药业公司合资兴建了1000吨／年维生素B工厂，还有罗氏泰山（上海）维生素A新厂，以及在无锡兴建4万吨／年柠檬酸工厂。巴斯夫公司在全球维生素市场上约占25％的份额，该公司在韩国Gunsan建成3000吨／年维生素B 工厂和世界规模的维生素C及维生素B的工厂。 我国食品添加剂的生产随食品加工业的发展而不断发展壮大，目前已批准使用的添加剂共有21类1474种，产品门类齐全，基本可以满足食品工业的需要。我国各类食品添加剂的年产品量已超过200万吨，其中味精达60万吨以上，柠檬酸的产量近20万吨。表1列出我国主要的食品添加剂生产企业和产量。我国食品添加剂的总量已可以满足市场需求，但由于我国多数食品添加剂企业生产规模小，技术水平低，因此产品质量方面尚存在一些差距。因此少数用量少、档次高的食品添加剂仍依赖进El。一些合资的食品加工企业和引进的食品加工生产线为了保证其产品的质量，仍以较高的价格购买国外的同类产品。 2、营养添加剂 牛磺酸近年来，国内外研究表明，牛磺酸是一种具有多种生理功 第一部分核酸 一、填空 1．核酸最初是从中分离出来的一种含磷较多的酸性物质。 2．核酸按组成不同分为和。RNA主要存在于中，功能是；DNA主要存在于，功能是。 3．核酸完全水解的产物有、、。 4．核酸中戊糖有和两种，在RNA中含，在DNA中含。核酸中的嘌呤碱有、两种，嘧啶碱有、和三种。 5．RNA中含有、、和四种含氮碱，DNA中含、、和四种含氮碱。 6．组成核酸的基本单位是，它由、和各一分子缩合而成。 7．1953年、提出DNA分子具有双螺旋结构假说。 8．DNA的二级结构为结构。RNA据其功能不同分为、、。 9．维持DNA双螺旋结构的维系力主要是和。 10．、、、是组成DNA的基本单位，、、、是组成RNA的基本单位。 二．名词 1、Tm 2、增色效应 3、DNA的复性 三、选择 1．已知一段DNA一条链为5'AGCTGACCTAGA3'，其另一条互补链为（）。 A 5'TCTAGGTCAGCT3' B 5'CUCAGGUCAGCU3' C 5'CACATTGAUTAT3' D 5'UCACUCGGGAUC3' 2．DNA变性后的特征变化是（）。 A 磷酸二酯键断裂 B A260增高 C A280增高 D 分子量变小 3．已知某双链DNA的一条链中A=30%、G=24%，其互补链的碱基组成正确的是 A T和C 46% B A和T 46% C A和G 54 % D T和C 54% 4．作为第二信使的核苷酸是( ) A cAMP B cCMP C AMP D cUMP 5．DNA的T m值的叙述正确的是（） A 与溶液浓度无关 B与分子大小无关 C 无种属特异性 D G—C碱基对含量高，T m值也高。 6.核酸分子中，储存遗传信息的关键部分是( ) A 戊糖磷酸的骨架 B 碱基序列 C 戊糖构象 D 磷酸二酯键 7．参与构成DNA分子的单糖是( ) A 核糖 B 脱氧核糖 C 葡萄糖 D 果糖 8．只存在于RNA而不存在于DNA的碱基是( ) A 尿嘧啶 B 腺嘌呤 C 鸟嘌呤 D 胞嘧啶 9．DNA是( ) A 核糖核苷酸 B 核糖核酸 C 脱氧核糖核酸 D 核蛋白体10．DNA的二级结构是（） A 超螺旋 B 双螺旋 C 局部双螺旋 D 发夹式结构11．关于DNA和RNA彻底水解产物的叙述，正确的是（） A 碱基相同，戊糖相同 B 碱基相同，戊糖不同 C 碱基不同，戊糖相同 D 部分碱基相同，戊糖不同 12．核酸最初是从（）分离出的呈酸性的物质。 A 线粒体 B 细胞核 C 叶绿体 D 细胞质 13．DNA分子中碱基配对规律是（）；RNA分子中碱基配对规律是（）。 A A－T，G－C B G－C，A－U C A－U，A－C D A－C，G－A 14．核酸一级结构的维系力是（） A 氢键 B 磷酸二酯键 C 范德华力 D 碱基堆积力 15. 核酸分子中，碱基配对主要依赖于（）化学键 A 氢键 B 糖苷键 C 磷酸二酯键 D 碱基堆积力 16．DNA的T m叙述正确的是（） A 20%的DNA解链时的温度 B 40%的DNA解链时的温度 C 50%的DNA解链时的温度 D 60%的DNA解链时的温度 17．关于tRNA的叙述不正确的是（） A 通常由70—90个核苷酸组成 B 含有较多稀有碱基 生物化学是一门较年轻的学科，在欧洲约在160年前开始，逐渐发展，一直到1903年才引进“生物化学”这个名词而成为一门独立的学科，但在我国，其发展可追溯到远古。我国古代劳动人民在饮食、营养、医、药等方面都有不少创造和发明，生物化学的发展可分为：叙述生物化学、动态生物化学及机能生物化学三个阶段。 （一）叙述生物化学阶段 1.饮食方面：公元前21世纪，我国人民已能造酒，相传夏人仪狄作酒，禹饮而甘之，作酒必用曲，故称曲为酒母，又叫做酶，与媒通，是促进谷物中主要成分的淀粉转化为酒的媒介物。现在我国生物化学工作者将促进生物体内化学反应的媒介物（即生物催化剂）统称为酶，从《周礼》的记载来推测，公元前12世纪以前，已能制饴，饴即今之麦芽糖，是大麦芽中的淀粉酶水解谷物中淀粉的产物。《周礼》称饴为五味之一。不但如此，在这同时，还能将酒发酵成醋。醋亦为五味之一。《周礼》上已有五味的描述。可见我国在上古时期，已使用生物体内一类很重要的有生物学活性的物质——酶，为饮食制作及加工的一种工具。这显然是酶学的萌芽时期。 2.营养方面：《黄帝内经·素问》的“藏气法时论”篇记载有“五谷为养，五畜为益，五果为助，五菜为充”，将食物分为四大类，并以“养”、“益”、“助”、“充”表明在营养上的价值。这在近代营养学中，也是配制完全膳食的一个好原则。谷类含淀粉较多，蛋白质亦不少，宜为人类主食，是生长、发育以及养生所需食物中之最主要者；动物食品含蛋白质，质优且丰富，但含脂肪较多，不宜过多食用，可用以增进谷类主食的营养价值而有益于健康，果品及蔬菜中无机盐类及维生素较为丰富，且属于粗纤维，有利食物消化及废物的排出；如果膳食能得到果品的辅助，蔬菜的充实，营养上显然是一个无可争辩的完全膳食。膳食疗法早在周秦时代即已开始应用，到唐代已有专书出现。盂诜（公元7世纪）著《食疗本草》及昝殷（约公元8世纪）著《食医必鉴》等二书，是我国最早的膳食疗法书籍。宋朝的《圣济总录》（公元前12世纪）是阐明食治的。元朝忽思慧（公元14世纪）针对不同疾患，提出应用的食物及其烹调方法，并编写成《饮膳正要》。由此可看出我国古代医务工作者应用营养方面的原理，试图治疗疾患的一些端倪。 3.医药方面：我国古代医学对某些营养缺乏病的治疗，也有所认识，如地方性甲状腺肿古称“瘿病”，主要是饮食中缺碘所致，有用含碘丰富的海带、海藻、紫菜等海产品防治。公元4世纪，葛洪著《肘后百一方》中载有用海藻酒治疗瘿病的方法。唐·王焘（公元8世纪）的《外台秘要》中载有疗瘿方36种，其中27种为含碘植物。而在欧洲直到公元1170年才有用海藻及海绵的灰分治疗此病者。脚气病是缺乏维生素B1的病。孙思邈（公元581～682年）早有详细研究，认为是一种食米区的疾病，分为“肿”、“不肿”及“脚气入心”三种，可用含有维生素B1的车前子、防风、杏仁、大豆、槟榔等治疗。酿酒用的曲及中药中的神曲（可生用）均含维生素B1较丰富，且具有水解糖类的酶，可用以补充维生素B1的不足，亦常用以治疗胃肠疾患。夜盲症古称“雀目”，是一种缺乏维主素A的病症。孙思邈首先用含维生素A较丰富的猪肝治疗。我国最早的眼科专著《龙木论》记载用苍术、地肤子、细辛、决明子等治疗雀目。这些药物都是含有维生素A原的植物。 我国研究药物最早者据传为神农。神衣后世又称炎帝，是始作方书，以疗民疾者。《越绝书》上有神农尝百草的记载。自此以后，我国人民开始用天然产品治疗疾病，如用羊靥（包括甲状腺的头部肌肉）治甲状腺肿，紫河车（胎盘）作强壮剂，蟾酥（蟾蜍皮肤疣的分泌物） 一、独立的生命单位 细胞是包含了全部生命信息和体现所有基本特点的独立的生命单位。 细胞包含3个体系： ●遗传信息的复制、维持和表达体系 ●新陈代谢体系 ●构成维持生命结构有序性体系，如细胞骨架系统 真核细胞是如何进化来的？ 共生假说：认为真核细胞是一种复合体,它是若干原核细胞与真核细胞祖先的胞质共生 的结果 渐进式进化：认为原核细胞到真核细胞是一种渐进、直接进化的过程。 根据分子分类研究结果，却认为真核细胞、原核细胞和古细菌细胞同属于由共同祖先平行 进化而来的种类。 二、限制细胞大小的自然规律 ● Relationship Between Cells Volume(细胞体积） 一个生活细胞要维持正常的独立生活功能，最低限度需要容纳下为自身生存和繁殖 所必须的足够的DNA、蛋白质分子以及其他内部结构的空间(最低限度需要500～1000种不 同类型的酶和蛋白质)。 ● Cell Surface Area（表面积） 细胞必须有足够的表面积才能从环境中获得充足的营养和水分。 ◆细胞维持体积的相对恒定 1～10μm之间，而真核细胞的直径平均为3～30μm; ,如人的卵细胞直径只有0.1mm,而鸵鸟的卵细胞的直 径则有5cm; ,不依生物个体的大小而增大或缩小。如人、牛、马、 鼠、象的肾细胞、肝细胞的大小基本相同; ,与细胞的数量成正比,而与细胞的大小无关,把这种 现象为“细胞体积的守恒定律”。 细胞化学成分 水:85% 无机盐:1.5% 蛋白质:10% 脂质:2% 糖类:0.4% DNA: 0.4% RNA : 0.7% 三、原核细胞 主要特点 1.遗传物质仅一个环状DNA 2.无核膜，有细胞壁 3.无细胞器, 无细胞骨架 4.以无丝分裂或出芽繁殖 代表生物：支原体、细菌、蓝藻 四、真核细胞 三大结构体系 生物膜系统质膜、内膜系统（细胞器） 遗传信息表达系统染色质(体)、核糖体、mRNA、tRNA等等 细胞骨架系统胞质骨架、核骨架 食品添加剂现状和发展趋势 食品添加剂是指在食品或食品加工中使用的各种微量的物质，通常其添加量不超过食品质量的2％。添加目的为：①改进和保持食品的营养价值；②延长食品的货架期；③方便食品的加工；④增强食品的风味，改变食品的色泽；⑤确保微生物的安全性；⑥保持食品品质的连续性和统一性。 l、食品添加剂市场 据统计，目前全球开发的食品添加剂总数已达1．4万多种，其中直接使用的品种有300o余种，常的有680余种。美国是世界上食品添加剂便用量最大、使用品种最多的国家．目前允许直接使用的有230o种以上，消费量已超过14o万吨(不包括淀粉及其衍生物、香精/香料和调味料）；西欧消费量已近50075~，其中淀粉及其衍生物的数量高达40万吨。 食品添加剂已．成为医药、农用化学品及饲料添加剂之后的第四类倍受人们关注的精细化工行业。目前食品添加剂的世界市场价值为200亿美元，其中，调味品占30~,4、氢化胶体占17％、酸化剂占13%、调味增强剂占12％、甜味剂占6％、色素占5％、乳化剂占5％、维生素和矿物质占5％、酶占4％、化学防腐剂占2％、抗氧化剂占1％。j 负计禾来5年内冥年增长率为2％-3％。全球调味品和香料的市场价值为12o亿美，其中调味品约占49％(59亿美元)。调味品市场中，饮料占31％、佐料占23％、奶制品占14％、其他占32％。需求增长最强劲的食品添加剂将是维生素、矿物质、调味增强剂和脂肪代用品。 罗氏(R。h)和巴斯夫公司是世界上重要的食品添加剂和精细化学品生产商。维生素是罗氏公司维生素和精细化学品部最大的业务部门，几乎占全球销售额的50%，其次是精细化学品占30%、类胡萝卜素占20％。罗氏新上市的营养药品包括用于眼科保健的玉米黄质、番茄红素和叶黄素，以及供功能饮料用的水溶性维生素E制品等。罗氏公司也加快投资中国市场，与上海新亚药业公司合资兴建了1000吨／年维生素B工厂，还有罗氏泰山(上海)维生素A新厂，以及在无锡兴建4万吨／年柠檬酸工厂。巴斯夫公司在全球维生素市场上约占25％的份额，该公司在韩国Gunsan建成3000吨／年维生素B工厂和世界规模的维生素C及维生素B的工厂。 专升本生物化学问答题答案(A4)解读 温医成教专升本《生物化学》思考题参考答案 下列打“*”号的为作业题，请按要求做好后在考试时上交 问答题部分：（答案供参考） 1、蛋白质的基本组成单位是什么？其结构特征是什么？ 答：组成人体蛋白质的氨基酸仅有20种，且均属L-氨基酸（甘氨酸除外）。 *2、什么是蛋白质的二级结构？它主要形式有哪两种？各有何结构特征？ 答：蛋白质分子中某一段肽链的局部空间结构，即该段肽链主链骨架原子的相对空间位置，并不涉及氨基酸残基侧链的构象。 α-螺旋、β-折叠。 α-螺旋：多肽链的主链围绕中心轴做有规律的螺旋上升，为右手螺旋，肽链中的全部肽键 都可形成氢键，以稳固α-螺旋结构。 β-折叠：多肽链充分伸展，每个肽单元以Cα为旋转点，依次折叠成锯齿状结构，肽链间形成氢键以稳固β-折叠结构。 *3、什么是蛋白质变性？变性的本质是什么？临床上的应用？（变性与沉淀的关系如何？）（考过的年份：2006 答：某些理化因素作用下，使蛋白质的空间构象遭到破坏，导致其理化性质改变和生物活性的丢失，称为蛋白质变性。 变性的本质：破坏非共价键和二硫键，不改变蛋白质的一级结构。 变性的应用：临床医学上，变性因素常被应用来消毒及灭菌。此外, 防止蛋白质变性也是有效保存蛋白质制剂（如疫苗等）的必要条件。 （变性与沉淀的关系：变性的蛋白质易于沉淀，有时蛋白质发生沉淀，但并不变性。） 4、简述细胞内主要的RNA及其主要功能。（同26 题） 答：信使RNA（mRNA）：蛋白质合成的直接模板； 转运RNA(tRNA)：氨基酸的运载工具及蛋白质物质合成的适配器； 核蛋白体RNA(rRNA)：组成蛋白质合成场所的主要组分。 *5、简述真核生物mRNA的结构特点。 答：1. 大多数真核mRNA的5′末端均在转录后加上一个7-甲基鸟苷，同时第一个核苷酸的C′2也是甲基化，形成帽子结构：m7GpppNm-。 2. 大多数真核mRNA的3′末端有一个多聚腺苷酸(polyA)结构，称为多聚A尾。 6、简述tRNA的结构特点。 答：tRNA的一级结构特点：含10~20% 稀有碱基，如DHU；3′末端为— CCA-OH；5′末端大多数为G；具有T C 。 tRNA的二级结构特点：三叶草形，有氨基酸臂、DHU环、反密码环、额外环、TΨC环组成。tRNA的三级结构特点：倒L形。 7、试述酶与一般催化剂相比有哪些异同点。 答：酶与一般催化剂的共性：1．本身反应前后无变化，2．不改变化学反应平衡常数，3．降低反应的活化能 酶的催化特性：1. 高度的催化效率，2.高度专一性，3．高度的不稳定性，酶易失活，4．酶的催化活性的可调节性。 *8、何谓酶的竞争性抑制作用，其动力学特点如何？并以此解释磺胺药抑制细菌在体内繁殖的机理。 （举例说明酶的竞争性抑制作用及其实际应用意义）（考过的年份：2012、2011、2010、2009、2008 答：抑制剂与底物结构相似（1分）,共同竞争酶的活 简答题、问答题 1．组成蛋白质的氨基酸有多少种?其结构特点是什么? 答：组成蛋白质的氨基酸有20种。结构特点：（1）除脯氨酸是α-亚氨基酸外，所有氨基酸均为α-氨基酸；（2）除甘氨酸外，其它氨基酸的α-碳原子（分子中第二个碳，Cα）均为不对称碳原子，D-型和L-型两种立体异构体，但天然蛋白质中的氨基酸都是L-型氨基酸；（3）氨基酸之间的不同，主要在于侧链R 的不同。 2．蛋白质分子结构可分为几级?维持各级结构的化学键是什么? 答：蛋白质分子结构分为一、二、三、四级；维持各级结构的化学键分别是肽键、二硫键，氢键，次级键（疏水键），次级键（疏水键）。 3、酶作为一种生物催化剂有何特点? 答：酶具有高效性、专一性、活性可调性。 4、解释酶的活性部位、必需基团二者之间的关系。 答： 必需基团 5、说明米氏常数的意义及应用。 答：米氏常数等于酶促反应速度为最大反应速度一半时的底物浓度。 应用： （1）米氏常数是酶的特征性常数，每一种酶都有它的Km 值，与酶的性质、催化的底物和酶促反应条件（如温度、pH 、有无抑制剂等）有关，而与酶浓度无关。 （2）K m 值可用于表示酶和底物亲和力的大小。 （3）当使用酶制剂时，可以根据K m 值判断使酶发挥一定反应速度时需要多大的底物浓度；在已规定底物浓度时，也可根据K m 值估算出酶能够获得多大的反应速度。 6、什么是竞争性和非竞争性抑制?试用一两种药物举例说明不可逆抑制剂和可逆抑制剂对酶的抑制作用? 答：竞争性抑制：抑制剂结构与底物的结构相似，它和底物同时竞争酶的活性中心，因而妨碍了底物与酶的结合，减少了酶分子的作用机会，从而降低了酶的活性。非竞争性抑制：抑制剂和底物不在酶的同一部位结合，抑制剂与底物之间无竞争性，酶与底物结合后，还可与抑制剂结合，或者酶和抑制剂结合后，也可再同底物结合，其结果是形成了三元复合物(ESI)。可逆抑制剂：增效联磺的杀菌作用：增效联磺抑制细菌的二氢叶酸合成酶、二氢叶酸还原酶德活性，使细菌体内四氢叶酸的合成受到双重抑制，使细菌因核酸的合成受阻而死亡。不可逆抑制剂：有机磷农药能共价结合胆碱酯酶活性中心上的羟基，使胆碱酯酶失活。临床药物解磷定（PAM ）可解除有机磷化合物对胆碱酯酶的抑制。 7、简述糖酵解的生理意义。 答：（1）糖酵解是机体在缺氧情况下迅速获得能量的重要方式。例如剧烈｛ 活性中心内 活性中心外 维持酶活性中心的空间构象 ｛ 结合基团：能与底物结合 催化基团：催化底物发生化学反应 食品酸味剂的研究应用现状及发展趋势 李俊文 哈尔滨工业大学食品科学与工程学院 摘要：本文着重介绍柠檬酸，乳酸，苹果酸，酒石酸等几种常用食品酸味剂在食品工业中应用现状并展望了食品酸味剂的发展趋势 关键词：酸味剂，柠檬酸，乳酸，苹果酸，酒石酸 酸味剂具有增进食品质量的许多功能特性，例如改变和维持食品的酸度并改善其风味；增进抗氧化作用，防止食品酸败；与重金属离子络合，具有阻止氧化或褪变反应、稳定颜色、降低浊度、增强胶凝特性等作用。我国现已批准许可使用酸味剂的有：柠檬酸、乳酸、磷酸、酒石酸、苹果酸、偏酒石酸、乙酸、盐酸、己二酸、富马酸、氢氧化钠、碳酸钾、碳酸钠、柠檬酸钠、柠檬酸酸钾、碳酸氢三钠、柠檬酸一钠等17种。 1柠檬酸及其钠盐 1.1柠檬酸及其应用 柠檬酸广泛用于食品工业，是一种重要的食品添加剂。柠檬酸在食品加工中的应用应根据不同产品和不同口味来调整添加量，以达到最佳效果。 1 .1.1 酸味剂 柠檬酸作为酸味剂具有酸味圆润滋美的特点，广泛用于汽水、果汁、果冻、水果罐头等生产加工中。通常使用量为0.1%～0.5%，具体使用量可视品种和需要而定。在某些果蔬制品中还可以通过柠檬酸和糖来调节制品的糖酸比。同时通过柠檬酸调整pH值还可改善产品品质和风味。 1.1.2 蔗糖转化剂 在蔗糖液中添加适量柠檬酸可使其转化为转化糖，可提高蔗糖的饱和度和粘度，增大渗透压。因此用于果酱、果冻中有改善风味、防腐和促进蔗糖转化的作用，防止蔗糖晶析而发砂，改善产品质地。 1.1.3 稳定色素 果蔬原料放在1%～2%的食盐和0.1%的柠檬酸混合液中浸渍，可抑制果蔬原料酶褐变引起的变色。同时由于柠檬酸的高酸性，它还具有良好的防腐功能，能抑制细菌增殖，且能增强抗氧化剂的作用。如切去皮后的果蔬原料在0.1%的抗坏血酸溶液中浸渍后可防止氧化变褐。在使用时一般以柠檬酸作增效剂，以控制酚酶的活力，防止酶褐变。 1.1.4 面制品改良剂 在面食制品中用小苏打疏松剂时，制品往往碱度增大，口味变劣。若柠檬酸和小苏打同时使用，可使小苏打分子在反应过程中产生的二氧化碳被吸收，不致使碳酸钠积累，从而降低面制品的碱度，改善口味。 此外，柠檬酸还可作为冷冻水果和水果加工品中维生素的稳定剂，以及作为软饮料、冷饮、糖果、焙烤食品、胶姆糖的增香剂。 1.2柠檬酸钠及其应用 柠檬酸钠是一种无色晶体或白色结晶粉末，目前最重要的柠檬酸盐。柠檬酸钠主要由淀粉类物质经发酵生成柠檬酸，再跟碱类物质中和而产生。柠檬酸钠用作食品添加剂，需求量 第23章三羧酸循环(生物化学下册p92) 3学时 学习重点： ◆熟悉柠檬酸循环途径中的各步酶促反应，以及各步反应酶的作用特点。 ◆会分析和计算酵解和柠檬酸循环中产生的能量，以及底物分子中标记碳的去向。 葡萄糖的有氧氧化包括四个阶段。 ①糖酵解产生丙酮酸（2丙酮酸、2ATP、2NADH） ②丙酮酸氧化脱羧生成乙酰CoA ③三羧酸循环（CO2、H2O、A TP、NADH） ④呼吸链氧化磷酸化（NADH-----ATP） 三羧酸循环：乙酰CoA经一系列的氧化、脱羧，最终生成CO2、H2O、并释放能量的过程，又称柠檬酸循环、Krebs循环。 原核生物：①~④阶段在胞质中 真核生物：①在胞质中，②~④在线粒体中 一、丙酮酸脱羧生成乙酰CoA 1、反应式： 2、丙酮酸脱氢酶系 丙酮酸脱氢酶系是一个十分庞大的多酶体系，位于线粒体膜上，电镜下可见。 E.coli丙酮酸脱氢酶复合体： 分子量：4.5×106，直径45nm，比核糖体稍大。 酶辅酶每个复合物亚基数 丙酮酸脱羧酶（E1）TPP 24 二氢硫辛酸转乙酰酶（E2）硫辛酸24 二氢硫辛酸脱氢酶（E3）FAD、NAD+12 此外，还需要CoA、Mg2+作为辅因子 这些肽链以非共价键结合在一起，在碱性条件下，复合体可以解离成相应的亚单位，在中性时又可以重组为复合体。所有丙酮酸氧化脱羧的中间物均紧密结合在复合体上，活性中间物可以从一个酶活性位置转到另一个酶活性位置，因此，多酶复合体有利于高效催化反应及调节酶在反应中的活性。 3、反应步骤 反应过程 （1）丙酮酸脱羧形成羟乙基-TPP （2）二氢硫辛酸乙酰转移酶（E2）使羟乙基氧化成乙酰基 （3）E2将乙酰基转给CoA，生成乙酰-CoA （4）E3氧化E2上的还原型二氢硫辛酸 （5）E3还原NAD+生成NADH 4、丙酮酸脱氢酶系的活性调节 从丙酮酸到乙酰CoA是代谢途径的分支点，此反应体系受到严密的调节控制，此酶系受两种机制调节。 （1）可逆磷酸化的共价调节 丙酮酸脱氢酶激酶（E A）（可被ATP激活） 丙酮酸脱氢酶磷酸酶（E B） 磷酸化的丙酮酸脱氢酶（无活性） 去磷酸化的丙酮酸脱氢酶（有活性） （2）别构调节 ATP、CoA、NADH是别构抑制剂 ATP抑制E1 CoA抑制E2 NADH抑制E3 5、能量 1分子丙酮酸生成1分子乙酰CoA，产生1分子NADH（2.5A TP）。 二、三羧酸循环（TCA）的过程 TCA循环：每轮循环有2个C原子以乙酰CoA形式进入，有2个C原子完全氧化成CO2放出，分别发生4次氧化脱氢，共释放10A TP。 1、反应步骤 概述三羧酸循环（图，见书） （1）、乙酰CoA+草酰乙酸→柠檬酸 柠檬酸合酶，TCA中第一个调节酶：受ATP、NADH、琥珀酰CoA、和长链脂肪酰CoA 的抑制；受乙酰CoA、草酸乙酸激活。 柠檬酸合酶上的两个His残基起重要作用： 一个与草酰乙酸羰基氧原子作用，使其易受攻击；另一个促进乙酰CoA的甲基碳上的质子离开，形成烯醇离子，就可与草酰乙酸缩合成C-C键，生成柠檬酰CoA，后者使酶构象变化，使活性中心增加一个Asp残基，捕获水分子，以水解硫酯键，然后CoA和柠檬酸相继离开酶。 氟乙酰CoA可与草酰乙酸生成氟柠檬酸，抑制下一步反应的酶，据此，可以合成杀虫剂、灭鼠药。 氟乙酸本身无毒，氟柠檬酸是乌头酸酶专一的抑制剂，氟柠檬酸结合到乌头酸酶的活性部位上，并封闭之，使需氧能量代谢受毒害。它存在于某些有毒植物叶子中，是已知最能致死的简单分子之一。LD50为0.2mg/Kg体重，它比强烈的神经毒物二异丙基氟磷酸的LD50 1、简述脂类得消化与吸收。 2、何谓酮体？酮体就是如何生成及氧化利用得？ 3、为什么吃糖多了人体会发胖（写出主要反应过程）？脂肪能转变成葡萄糖吗？为什么？ 4、简述脂肪肝得成因。 5、写出胆固醇合成得基本原料及关键酶？胆固醇在体内可得转变成哪些物质？ 6、脂蛋白分为几类？各种脂蛋白得主要功用？ 7、写出甘油得代谢途径？ 8、简述饥饿或糖尿病患者，出现酮症得原因？ 9．试比较生物氧化与体外物质氧化得异同。 10．试述影响氧化磷酸化得诸因素及其作用机制。 11．试述体内得能量生成、贮存与利用 12．试从蛋白质营养价值角度分析小儿偏食得害处。 13．参与蛋白质消化得酶有哪些？各自作用？ 14．从蛋白质、氨基酸代谢角度分析严重肝功能障碍时肝昏迷得成因。 15．食物蛋白质消化产物就是如何吸收得？ 16．简述体内氨基酸代谢状况。 17．1分子天冬氨酸在肝脏彻底氧化分解生成水、二氧化碳与尿素可净生成多少分子ATP？简述代谢过程。 18．简述苯丙氨酸与酪氨酸在体内得分解代谢过程及常见得代谢疾病。 19．简述甲硫氨酸得主要代谢过程及意义。 20．简述谷胱甘肽在体内得生理功用。 21．简述维生素B6在氨基酸代谢中得作用。 22．讨论核苷酸在体内得主要生理功能 23、简述物质代谢得特点？ 24、试述丙氨酸转变为脂肪得主要途径？ 25．核苷、核苷酸、核酸三者在分子结构上得关系就是怎样得？ 26．参与DNA复制得酶在原核生物与真核生物有何异同？ 27．复制得起始过程如何解链？引发体就是怎样生成得？ 28．解释遗传相对保守性及其变异性得生物学意义与分子基础。 29．什么就是点突变、框移突变，其后果如何？ 30、简述遗传密码得基本特点。 31、蛋白质生物合成体系包括哪些物质，各起什么作用。 32．简述原核生物基因转录调节得特点。阻遏蛋白与阻遏机制得普遍性。 33．简述真核生物基因组结构特点。 34．同一生物体不同得组织细胞得基因组成与表达就是否相同？为什么？ 35．简述重组DNA技术中目得基因得获取来源与途径。 36．作为基因工程得载体必须具备哪些条件？ 37．什么叫基因重组？简述沙门氏菌就是怎样逃避宿主免疫监视得？ 38．简述类固醇激素得信息传递过程。 39．简述血浆蛋白质得功能。 40．凝血因子有几种？简述其部分特点？ 41．简述红细胞糖代谢得生理意义。 42．试述维生素A缺乏时，为什么会患夜盲症。 43．简述佝偻病得发病机理。 第九章糖代谢 1. 什么是物质代谢？什么是能量代谢？二者之间的关系如何？ 答：物质代谢：研究各种生理活性物质（如糖、蛋白质、脂类、核酸等）在细胞内发生酶促反应的途径及调控机理，包含旧分子的分解和新分子的合成； 能量代谢：研究光能或化学能在细胞内向生物能（ATP）转化的原理和过程，以及生命活动对能量的利用。 能量代谢和物质代谢是同一过程的两个方面，能量转化寓于物质转化过程之中，物质转化必然伴有能量转化。 2. 中间代谢：消化吸收的营养物质和体内原有的物质在一切组织和细胞中进行的各种化学变化称为中间代谢。 3. 呼吸商（respiratory quotient 简称 RQ）：指生物体在同一时间内，释放二氧化碳与吸收氧气的体积之比或摩尔数之比，即指呼吸作用所释放的 CO2 和吸收的 O2 的分子比。 4. 自养型生物：为能够利用无机物合成有机物的类型，又分为光合自养——绿色植物，和化能自养——硝化细菌等。 5. 异养型生物：不能自己合成有机物，必须依靠自养生物制造的有机物生存。 6. 简述活体内实验及其意义。 答：1）用整体生物材料或高等动物离体器官或微生物细胞群体进行中间代谢实验研究称为活体内实验，用“in vivo”表示。2）活体内实验结果代表生物体在正常生理条件下，在神经、体液等调节机制下的整体代谢情况，比较接近生物体的实际。 7. 活体外实验：用从生物体分离出来的组织切片，组织匀浆或体外培养的细胞、细胞器及细胞抽提物进行中间代谢实验研究称为活体外实验，用“in vitro”表示。 8. 简述代谢途径的探讨方法 答：1）代谢平衡实验；2）代谢障碍实验（代谢途径阻断实验）；3）使用抗代谢物；4）代谢物标记追踪实验；5）测定特征性酶；6）核磁共振波谱法。 9. 简述糖的生理功能 答：1）作为生物体的结构成分；2）作为生物体内的主要能源物质；3）在体内转变为其他物质；4）作为细胞识别的信息分子。 10. 糖的分解途径有哪些？ 答：糖酵解、糖的有氧氧化、磷酸戊糖途径 11. 简述血糖中糖的来源？ 答：食物中多糖的消化吸收；乳酸、氨基酸、甘油等物质的糖异生；自身糖原的降解。12. 糖酵解：是将葡萄糖转变成乳酸并同时生成 ATP 的一系列反应，是一切有机体中都存在的葡萄糖降解途径。 13. 简述糖酵解的过程 答：1）己糖磷酸酯的生成：葡萄糖→果糖-1,6-二磷酸2）丙糖磷酸的生成（磷酸己糖的裂解）：果糖-1,6-二磷酸→2 分子磷酸丙糖3）丙酮酸的生成：甘油醛-3-磷酸→丙酮酸4）乳酸的生成：丙酮酸→乳酸 14. 简述糖酵解的特征 答：1）反应部位在胞液2）不需氧的产能过程（底物水平磷酸化） 1 G→ 2 ATP，Gn（G）→ 3 ATP 3）终产物乳酸：释放入血，进入肝脏代谢；分解利用；乳酸循环。 4）有 3 步不可逆反应 生物化学复习资料 1天然不饱和脂肪酸的碳-碳双键都是顺式构型。 2.亚油酸，α亚麻酸和花生四烯酸是维持人体和动物正常生命活动所必需的脂肪酸，但哺乳动物体内不能合成或合成量不足，必须从食物中摄取，所以称为必须脂肪酸。 3氨基酸是蛋白质的结构单位，自然界中的氨基酸有300多种，但用来合成蛋白质的氨基酸只有20种，这20种氨基酸称为标准氨基酸。 4肽键：在蛋白质分子内，一个氨基酸的α-羧基与另一个氨基酸的α-氨基缩合形成的化学键称为肽键。 5肽：氨基酸通过肽键连接构成的分子称为肽。 6蛋白质的一级结构：蛋白质分子内的氨基酸的排列顺序称为蛋白质的一级结构，包括二硫键的位置。 7蛋白质的二级结构：是指多肽链主链的局部构象，不涉及侧链的空间排布。8蛋白质的二级结构的四种类型：α螺旋，β折叠，β转角，无规卷曲。 9.蛋白质一级结构与其功能的关系：蛋白质的一级结构决定其构象，进而决定其生理功能。改变蛋白质的一级结构可以直接影响其功能。 每一种蛋白质分子都有自己特定的氨基酸组成和排列顺序即一级结构，蛋白质的一级结构包含了指导其形成天然构象所需的全部信息。 10蛋白质的一般性质：紫外线吸收特征； 11两性解离与等电点：蛋白质是两性电解质，因为它们有肽键主链C端的羧基、谷氨酸的γ-羧基和天冬氨酸的β-羧基，可以给出H+而带负电荷；也有肽链主链N端的氨基、赖氨酸的ε-氨基、精氨酸的胍基和组氨酸的咪唑基，可以结合成H﹢而带正电荷。这些基团的解离状态决定蛋白质的带电荷状态，而解离状态受溶液的pH值影响。在某一pH值下，蛋白质的静电荷为零，则该pH值称为蛋白质的等电点（pI）。如果溶液pH 生物化学的发展史 [大] [中] [小] 发布人：圣才学习网发布日期：2008-01-25 14:18 共1564人浏览 大约在19世纪末，德国化学家李比希（J.Liebig）初创了生理化学，在他的著作中首次提出了“新陈代谢”这个词。以后德国的霍佩赛勒（E.F.Hoppe-seyler）将生理化学建成一门独立的学科，并于1877年提出“Biochemie”一词，译成英语为“Biochemistry”，即生物化学。生物化学的发展大体可分为三个阶段： 一、静态生物化学阶段 大约从19世纪末到20世纪30年代，主要是静态的描述性阶段。发现了生物体主要由糖、脂、蛋白质和核酸四大类有机物质组成,并对生物体各种组成成分进行分离、纯化、结构测定、合成及理化性质的研究。 1、1929年，德国化学家Fischer Hans发现了血红素是血红蛋白的一部分，但不属于氨基酸，进一步确定了分子中的每一个院子，获1930年诺贝尔化学奖。得很多糖和氨基酸的结构，确定了糖的构型，并指出蛋白质是通过肽键连接的。 2、通过食物的分析和营养的研究发现了一系列维生素，并阐明了它们的结构。1911年，Funk 结晶出治疗“脚气病”的复合维生素B，提出“Vitamine”，意即生命胺。后来由于相继发现的许多维生素并非胺类，又将“Vitamine”改为“Vitamin”。与此同时，人们又认识到另一类数量少而作用重大的物质--激素。它和维生素不同，不依赖外界供给，而由动物自身产生并在自身中发挥作用。肾上腺素、胰岛素及肾上腺皮质所含的甾体激素都是在这一时期发现的。 3、1926年，Sumner从半刀豆中制得了脲酶结晶，并证明它的化学本质是蛋白质。此后四、五年间Nothrop等人连续结晶了几种水解蛋白质的酶,如胃蛋白酶、胰蛋白酶等，并指出它们都是蛋白质，确立了酶是蛋白质这一概念。 4、中国生物化学家吴宪（1893～1959）在1931年提出了蛋白质变性的概念。吴宪堪称中国生物化学的奠基人，他在血液分析、蛋白质变性、食物营养和免疫化学等四个领域都做出了重要贡献，并培养了许多生化学家。 虽然对生物体组成的鉴定是生物化学发展初期的特点，但直到今天，新物质仍不断在发现。如陆续发现的干扰素、环核苷磷酸、钙调蛋白、粘连蛋白、外源凝集素等，已成为重要的研究课题。 早已熟知的化合物也会发现新的功能，20世纪初发现的肉碱，50年代才知道是一种生长因子，而到60年代又了解到是生物氧化的一种载体；多年来被认为是分解产物的腐胺和尸胺，后来被发现与精胺、亚精胺等多胺有多种生理功能，如参与核酸和蛋白质合成的调节，对DNA超螺旋起稳定作用以及调节细胞分化等。 二、动态生物化学阶段 第二阶段约在20世纪30～50年代，主要特点是研究生物体内物质的变化，即代谢途径，所以称动态生化阶段。在这一阶段，确定了糖酵解、三羧酸循环以及脂肪分解等重要的分解代谢途径，对呼吸、光合作用以及腺苷三磷酸(ATP)在能量转换中的关键位置有了较深入的认识。主要研究成果有: 1、1932年,英国科学家Krebs在前人工作的基础上，用组织切片实验证明了尿素合成反应，提出了鸟氨酸循环。并进一步对生物体内被氧化的过程进行了研究，于1937年又提出了各种化学物质的中心环节--三羧酸循环的基本代谢途径。 2、1940年,德国科学家Embden和Meyerhof提出了糖酵解代谢途径。 3、1949年，E.Kennedy等证明F.Knoop提出的脂肪酸β-氧化过程是在线粒体中进行的，并生化 期末复习
三羧酸循环-河北科技大学大学英语精品课
生化简答题(附答案)
食品添加剂的现状和发展趋势
生物化学
生物化学的发展
第二章 细胞生物学汇总
(发展战略)食品添加剂状态和发展方向
专升本生物化学问答题答案(A4)解读
生物化学(简答题、问答题)
食品酸味剂的研究应用现状及发展趋势
三羧酸循环
生物化学简答题
生物化学期末复习(简答、名词解释)
生物化学复习重点
生物化学的发展史
相关主题
文本预览