Model Checking for E-Business Control and Assurance
Bonnie Brinton Anderson, James V. Hansen, Paul Benjamin Lowry,
and Scott L. Summers
Abstract
Model checking is a promising technique for the veri?cation of complex software systems. As the use of the Internet for conducting e-business extends the reach of many organizations, well-designed software becomes the foundation of reliable implementation of e-business processes.These distributed, electronic methods of conducting transactions place reliance on the control structures embedded in the transaction processes.De?ciencies in control structures of processes that support
e-business can lead to loss of physical assets, digital assets, money, and consumer con?dence. Yet, assessing the reliability of e-business processes is complex and time-consuming.This paper explicates how model-checking technology can aid in the design and assurance of e-business processes in complex digital environments. Speci?cally, we demonstrate how model checking can be used to verify e-business requirements concerning money atomicity, goods atomicity, valid receipt, and communication-link failure. These requirements are fundamental to many e-business applications.
Model checking can be used to test a broad range of systems requirements—not only for system designers, but also for auditors and security specialists. Systems that are examined by auditors need to have adequate controls built in prior to implementation and will need adequate auditing after implementation to ensure that none of the processes have been corrupted. Model checkers may also provide value in examining the processes of highly integrated applications as found in enterprise resource planning systems.
Index Terms：
Atomicity, data typing, e-Business, model checking,process and communication protocols.
I. INTRODUCTION
Internet-based business operations offer considerable potential, but they are accompanied by a broad range of often unprecedented risks.An actual or perceived lack of system security and reliability can signi?cantly constrain the growth of the digital economy. While progress is being made in reducing Internet computational risks through a variety of software patches and cryptographic algorithms, these efforts address only a small portion of the larger challenge of establishing the
necessary security and reliability of e-business systems. To resolve this challenge, systematic management of the associated operational risks is essential [1].
According to Wang et al. [2], management of operational risks requires careful examination of the e-business infrastructure. Distributed Internet computing is changing e-market structures and e-business models in fundamental ways. Although the ?exibility of distributed e-operations supports open accessibility and dynamic interactions,?exibility can intensify problems arising from e-market information asymmetry and e-business operational uncertainty. These problems militate against innovative e-commerce developments. Although e-commerce offers the opportunity for businesses to gain ef?ciency and effectiveness through network-based ad-hoc partnerships, many businesses do not take advantage of these opportunities because of the heightened risks of operational uncertainty and perceived information asymmetry among unfamiliar business partners.
Manuscript received November 18, 2003; revised May 17, 2004. This paper was recommended by Associate Editor S. Lakshmivarahan.
The authors are with the Marriott School of Management and
Kevin and Debra Rollins Center for e-Business, Brigham Young
University, Provo, UT 84602 USA (e-mail: Bonnie_Anderson@https://www.doczj.com/doc/ea5817992.html,;
James_Hansen@https://www.doczj.com/doc/ea5817992.html,, Paul_Lowry@https://www.doczj.com/doc/ea5817992.html,; Scott_Summers@
https://www.doczj.com/doc/ea5817992.html,).
Digital Object Identi?er 10.1109/TSMCC.2004.843181
These issues take on added importance as new business models and architectures—such as Internet auctions, web services [3] and the semantic web [4]—offer broad support for loosely coupled, e-commerce transactions where buyers and sellers may not have any prior trading experience with one another. For example, the web services [3] platform provides the Universal Description, Discovery and
Integration (UDDI) registry for discovery of e-commerce services, WSDL for service description, and SOAP for transaction execution. These facilities require no prior knowledge of buyer and seller by either party.In such environments, merchants and customers may be reluctant to trust one another and the following situations may arise: A customer is unwilling to pay for a product without being certain the correct product will be sent. A merchant is unwilling to send a product without certainty of receiving payment. If a merchant delivers the product without receiving payment, a fraudulent customer may receive the product and then disappear, with a resulting loss to the merchant. If a customer pays before receiving the product, a merchant may not deliver or may deliver a wrong product. These possibilities underscore the need for carefully designed e-commerce models that are robust under all events.
As Wang et al. [5] note, e-system complexity and human limitations make it impossible to imagine all scenarios and guarantee correct processing under all circumstances—even for carefully designed and implemented code. Much of this
dif?culty is due to interconnectivity, which widens the potential range of error or vulnerability. Variation in execution of concurrent processes in nonstop, nondeterministic systems increases the potential for automation failures. Consequently mini mizing ?aws in transaction protocols is crucial for the survival and sustainability of e-business. Stakeholders, such as system designers,users, and auditors need methods to preclude these subtle but potentially critical mistakes—before erroneous processing occurs or an attacker exploits them—to enhance control and assurance to e-commerce users. Model checking offers a promising method for addressing these issues.
II. MODEL CHECKING FUNDAMENTALS
Automation failures occur when an automated system behaves differently than its stakeholders expect. If the actual system behavior and the stakeholders model are both described as ?nite state transition systems, then mechanized techniques known as model checking can be used to automatically discover any scenarios that cause the behaviors of the two descriptions to diverge from one another. These scenarios identify potential failures and pinpoint areas where design changes or revisions should be considered
Model checking can trace through all relevant states with respect to any given requirement. Since model checking operates on logic rather than individual execution paths, veri?cation can be more thorough and ef?cient than test runs and simulation. Some of the most compelling features of model checkers are summarized as follows [6].
1) They help delimit a system’s boundary or the interface between the system and its environment.
2) They precisely de?ne a system’s desired properties.
3) They characterize a sys tem’s behavior more accurately. Most current methods focus on functional behavior only (e.g., ―What is the correct answer?‖) but some can handle real-time behavior as well (e.g., ―Is the correct answer delivered on time?‖).
4) They can aid in proving that a system meets required speci?cations. By providing counterexamples that show how speci?cations are not satis?ed, model checkers can pinpoint the circumstances under which a system does not meet its speci?cations.
This can also help to correct the system.
These features of model checkers aid stakeholders in two important ways.
1) Through speci?cation, by focusing a system designer’s attention to crucial questions, such as: What is the interface? What are the assumptions about the application’s environment? What is the system supposed to do under this condition or that condition?
What happens if that condition is not met? What are the system’s invariant properties?
2) Through veri?cation, by providing additional assurance. Relying on proof that
a system meets its security goals is better than relying on opinion—even expert
opinion.
It should be emphasized that any proof of correctness is relative to both the formal speci?cation of a system and the formal speci?cation of the desired properties: a system proven correct with respect to an incorrect speci?cation leaves no assurance about the system at all.
The process of proving entails three actions: First, the system of interest must be modeled. A mathematical model is constructed that expresses the semantic structure
of an e-business implementation.
Second, all properties to be guaranteed in the implementation are formally
speci?ed. In an e-business context, one such speci?cation might be that goods must always be received before payment is initiated.
Third, a proof is provided. Typically, a proof relies on induction over traces of the e-commerce communication and transaction operations.
In general, verifying that any e-business process is resilient to hidden ?aws and errors is a daunting task. Manual methods are slow and error prone. Even theorem provers, which provide a formal structure for verifying standard characteristics, may require human intervention and can be time-consuming. Moreover, even if a failure is found using a theorem prover, it may provide little help in locating the source of the failure [2]. Simulations offer computational power, but they are ad hoc in nature and there is no guarantee they will explore all important contingencies [2].
In contrast, model checking is an evolving technology that can provide effective and ef?cient evaluation of e-business processes. Model checking was originally developed for validating highly complex integrated circuits and software packages [7], [8], but it has recently been adopted to tackle the complexity of e-commerce transactions [9],
[2], [10]. Current model-checking technology is based on automated techniques that are considerably faster and more robust than other approaches, such as simulation or theorem proving. Model checkers can analyze very large state spaces in minutes. Additionally, model checkers aid failure correction by supplying counterexamples when processing failures are discovered [11].Although model checking is still relatively new [9], [2], [10], it has shown impressive performance in the analysis of complex hardware and software processes [7], [8]. The extended fair-exchange protocol [10] used in this paper incorporates methods fundamental to a broad class of e-business processes, including distributed processing, parallelism,concurrency,
communication uncertainties, and continuous operations.For this study, we use the failures-divergence re?nement (FDR) model checker, which is based on the concurrency theory of communicating sequential processes (CSP) [8]. FDR veri?es whether a requirement is s atis?ed in a particular system design by performing tests on a re?nement of that system. That is to say, veri?cation is done by comparing the two models to check whether one is a re?nement of the other.
A CSP process is represented as a labeled transition system (LTS),which is a set of nodes representing the states of the process that are connected by directed arcs, labeled with an event. LTS describes the evolution of state transition. Starting from the distinguished node no the state is always one of the nodes, and progress is made by performing one of the actions possible for that node. Most actions are visible to the external environment and can only happen with its cooperation. Internal actions cannot be seen from the outside or occur automatically [8].
Such trace re?nements are normally used for proving requiredproperties. The
re?nement-checking algorithm in FDR is abstracted as follows:
BEGIN
Initialize explorer with a pair of initial nodes;
WHILE
explorer is not complete
Examine a fresh pair of nodes from the explorer
IF
Nodes are compatible in appropriate model
THEN
Add mutually reachable successor pairs to explorer
ELSE
Return counterexample with explorer path to this pair
END
END
The objective is to establish that performance requirements are satis?ed by the system design.
III. CASE STUDY
Fig. 1 represents the high-level abstraction of a protocol proposed in [10]. The essential processes are summarized in the following paragraphs. We ?rst provide an overview and then provide the necessary details for model checking.
Messages are exchanged between a customer, a merchant, and a trusted third party (TTP). A merchant has several digital products to sell. The merchant places a description of each product in an online catalog service with a TTP, along with a copy of the encrypted product.
When a customer ?nds a product of interest by browsing the catalog, the customer downloads the encrypted product and then sends a purchase order to the
merchant. The customer cannot use the product unless it has been decrypted, and the merchant does not send the decrypting key unless the merchant receives a payment token through the purchase order process. The customer does not pay unless the customer is sure that the correct and complete product has been received. The TTP provides anonymous support for purchase order validation, payment token approval, and approval of the overall transaction between the customer and the merchant.
At a detailed level, the customer ?rst browses the product catalog located at the TTP and chooses a product. The customer then downloads the encrypted product along with the product identi?er, which is a ?le that contains information about the product such as its description and checksum. If the identi?er of the encrypted product ?le matches the identi?er in the product identi?er ?le, the transaction proceeds. If the identi?ers do not match, an advice is send to the TTP, and the customer waits for the corre ct encrypted product ?le. This process ensures that the customer receives the product that was requested from the catalog.
Next, the customer prepares a purchase order (PO) containing the customer’s identity, the merchant identi?er, the product identi?er, and the product price. A cryptographic checksum is also prepared. The PO,along with the cryptographic checksum, is then sent to the merchant.
The combination of the PO and cryptographic checksum allows the merchant to ascertain whether the received PO is complete or whether it was altered in transit. Upon receipt of the PO, the merchant examines its contents. If the merchant is
satis?ed with the PO, the merchant endorses it and digitally signs the cryptographic checksum of the ention of state transition. Starting from the distinguished node the state dorsed PO. This is forwarded to the TTP. The TTP is involved in the is always one of the nodes, and progress is made by performing one of the actions possible for that node. Most actions are visible to the external environment and can only happen with its cooperation. Internal actions cannot be seen from the outside or occur automatically [8].
process to prevent the merchant from later claiming nonacceptance of the terms and conditions of the transaction.The merchant also sends the TTP a single-use decrypting key for the product. The merchant next sends a copy of the encrypted product to the customer, together with a signed cryptographic checksum. The signed cryptographic checksum establishes the product origin and also provides a check to verify whether the product has been corrupted during transit.
Upon receipt of this second copy of the encrypted product, the customer validates that the ?rst and second copies of the product are identical. Through this process, the customer can be assured of receiving the actual product ordered. The customer then requests the decrypting key from the TTP. To do this, the customer forwards the PO and a signed payment token to the TTP, together with the cryptographic checksum.
The payment token contains the customer’s identity, the identity of the customer’s ?nancial institution, the customer’s bank account number with the
?nancial institution, and the amount to be debited from the customer’s account.
To verify the transaction, the TTP ?rst compares the digest included in the PO from the customer with the digest of the same PO from the merchant. If the two do not match, the TTP aborts the transaction. Otherwise, the TTP proceeds by validating the payment token with the customer’s ?nancial institution by presenting the token and the sale price.
If the ?nancial institution d oes not validate the token, the TTP aborts the transaction and advises the merchant accordingly. If the ?nancial institution does validate the token, the TTP sends the decrypting key to the customer and the payment token to the merchant, both digitally sig ned with the TTP’s private key.Secure channels guarantee the con?dentiality of all messages throughout this protocol. The protocol ensures money atomicity if the payment token generated by the customer contains the amount to be debited from the customer’s account and credited to the merchant’s account. Consequently, no money is created or destroyed in the system by this protocol.
Goods atomicity is guaranteed if the TTP hands over the payment token only when the customer acknowledges receipt of the product.
The process also ensures that the product is actually available to the customer for use only when the customer consents to payment by acknowledging receipt of the product.
Delivery veri?cation is guaranteed if the TTP receives a cryptographic checksum of the product from the merchant. Also, the customer independently generates a checksum of the product received and sends it to the TTP. Using these two copies of the checksum (available at the TTP), both the merchant and the customer demonstrate proof of the contents of the delivered good.
Controls are integrated into the modeling process by specifying limits or
boundaries within the model. We offer several examples:
Message types in the implementation can be constrained such that only certain types can be sent by the various agents. For example, it can be asserted that a customer may send only certain types of messages to the TTP and merchant. The
e-business model can then be t ested to determine if this speci?cation can be violated under any conditions.
The content allowable in various messages can be also be stipulated and tested. It also may be important to specify the conditions under which agents can abort a transaction, if at all.
Therearealso issues of protection from interruption. Systemsare often designed under the assumption that transaction links are completely reliable. The reality may be that technical failures or attacks may undermine this expectation. It is safer to specify and verify properties to cope with unreliable communications or communication failures.
IV. MODEL CHECKING THE SYSTEM
For purposes of demonstration, we encoded the above-described
e-business system [10] in the model checker FDR. FDR has been used in a variety of hardware and software applications, and has recently been applied toward testing for atomicity in two commercial e-commerce payment systems [9]. We illustrate several control features of model checking in the discourse that follows. We intend for the discussion to be nontechnical and use actual code only when it is straightforward; in other instances, we use pseudocode.
A. Data Types and Message Control
We ?rst consider the use of data typing. Data typing allows an ana-
lyst to ensure that only speci?ed types of messages are communicated from one trading party to another. Consider the following data-type
speci?cations:
--Data types
data type KEY =key
data type PO= po
data type ENCRYPTEDGOODS= eGoodsValid eGoodsInvalid
data type TOKEN =paymentToken
data type MESSAGE= transAborted
--Channel declarations
channel coutm: {po}
channel moutc: {eGoodsValid, eGoodsInvalid}
channel moutt: {key1}
channel toutc: {key1, eGoodsValid, eGoodsInvalid,
transAborted}
channel toutm: {payment Token,
transAborted}
channel minc: {po}
channel tinc: {payment Token}
channel cinm: {eGoodsValid, eGoodsInvalid}
channel tinm: {key}
channel cint: {key, eGoodsValid, eGoodsInvalid,
transAborted}
channel mint: {paymentToken,
transAborted}
channel coutt: {paymentToken}
In this example, all of the data types are simple, except for encrypted goods, which allows two values: eGoodsValid (for valid encrypted goods) and eGoodsInvalid (for invalid encrypted goods). In general,any ?nite number of values for a data type can be speci?ed. This useful control is used to specify the messages allowed on various channels as shown above. For instance, the only allowable transmissions on the channel toutm (for channel out from TTP to merchant) are payment Token or transAborted messages. Any other message by an intruder would be disallowed.
Another example concerns the channel cint (for channel in to the customer from the trusted-third party): The only allowable messages are a key, eGoodsValid, eGoodsInvalid, or transAborted. One might ask why eGoodsInvalid is allowed since this represents an invalid product. The reason is that it is not known that eGoodsInvalid is invalid until the customer checks the product against the description of the ordered product.
The remaining channels impose similar restrictions. If the system is expressed in this way, the model checker can later verify whether there are any circumstances under which these constraints can be violated.
B. Ensuring Transaction Completion
Three of the most important requirements of e-business trading are as follows.
1) Money is neither created nor destroyed in the course of an e-commerce transaction. A transaction should ensure the transfer of funds from one party to another without the possibility of the creation or destruction of money. No viable
e-business payment method can exist without supporting this property [13], which is commonly known as money atomicity.
2) Both the customer and merchant receive evidence that the goods sent (or received) are those to which both parties agreed. This is of particular importance when dealing with goods that can be transferred electronically (as we do here). This property is commonly known as valid receipt. The combination of both 1 and 2 is fundamental [14].
3) The customer must be able to verify that the product about to be received from the merchant is the same as the product that was ordered, before the customer pays for
the product [15]. This property is commonly known as goods atomicity.
Model checking allows us toverify that our system guarantees the sere quirements by writing them as speci?cations in the model checker. FDR returns the results of these large search spaces expeditiously. If a speci?cation is not satis?ed, the model checker returns a counterexample that allows an analyst to quickly see how there quirement can be violated.This, in turn, aids in modifying the system to resolve the problem. As an example, we consider a speci?cation for requirement 1 above.
Speci?cation requirem ent_1
IF NOT transaction trace=STOP
OR
{customer sends paymentToken to TTP;
merchant receives paymentToken from TTP;
STOP;}
OR
{customer sends paymentToken to TTP;
customer receives transAborted message from TTP;
STOP;}
THEN
Requirement 1 is violated;
End requirement _1;
This speci?cation asserts the following:
1) The customer must send payment to the TTP, and the merchant must subsequently receive that payment from the TTP, or
2) The customer can send payment to the TTP and (in the case where the payment is invalid) the customer then receives a transaction aborted message from the TTP.
3) If neither speci?ciation 1(nor 2) is satis?ed, the requirement is violated.
The following is an example of what the model checker might returnas a counterexample in case the requirement fails under some set of conditions.
1) The customer receives the encrypted goods from the TTP and then sends a purchase order to the merchant.
2) The merchant sends the encrypted goods to the customer and sends a key to the TTP, after which the encrypted goods are received by the customer who sends a payment token to the TTP.
3) The TTP then receives the key from the merchant and the payment token from the customer.
4) The TTP sends the payment token to the merchant, after which the customer receives the key from the TTP. The process then stops. Since the next step should have been the receipt of the payment token by the merchant (from the TTP), we know where to look to examine the failure.
In the above case, the model checker showed that the failure occurred in the
e-process that controls the sending of a decrypting key from the merchant to the TTP. Once this failure was identi?ed, the problem was identi?ed and recti?ed as shown by a subsequent run of the model checker.
C. Controlling Communication Link Failures
Suppose, however, that unreliability exists on the link from the merchant to the TTP. Such link unreliability could result from technical failure, as well as malicious intrusion by a hacker. Consideration of this contingency can be included in
model-checker representation by the following e-process:
Procedure comm mc
IF product is IN eGoodsValid, eGoodsInvalid
THEN
CUSTOMER receives product from MERCHANT OR
PROCEDURE comm mc;
End comm mc;
This representation means that if all goes well, the transmittal of a payment token from the customer to the TTP will be followed by the receipt of a payment token from the customer. Yet the comm mc procedure above allows unspeci?ed delays because each transmission can nondeterministically be followed over and over by the comm mc procedure. What happens when we subject our unreliable link to exami-nation by the model checker? It returns the following counterexample.
1) The valid encrypted goods are sent from the TTP and received by the customer.
2) A purchase order is transmitted from the customer and received by the merchant.
3) The merchant sends the valid encrypted goods, which are re-
ceived by the customer; the merchant also sends a key to the
TTP, which is received.
4) The customer sends a payment token to the TTP, which is received.
5) The TTP sends a key to the customer, which is received.
6) The TTP sends a payment to the merchant, but this payment is not received.
The model checker has found a failure that violates both requirement 1 and requirement 2. An inspect ion of the requirement 1 speci?cation repeated below shows that the sending of a payment token from the customer to the TTP must ?nally be followed by the receipt of that token by the merchant (sent by the TTP) or by the transmittal of a transaction aborted message from the TTP to the customer.
Speci?cation requirement 1
IF NOT transaction trace=STOP
OR
{customer sends paymentToken to TTP;
merchant receives paymentToken from TTP;
STOP;}
OR
{customer sends paymentToken to TTP;
customer receives transAborted message from TTP;
STOP;}
THEN
Requirement 1 is violated;
End requirement _1;
In addition, requirement 2 stipulates that a customer receives the product only after the customer has paid for the product. Since the merchant never received the payment token, no encrypted goods were transmitted from the merchant to the customer. These problems can be resolved by modifying the comm mc procedure in the following way:
Procedure comm mc
IF product is IN eGoodsValid, eGoodsInvalid
THEN
CUSTOMER receives product from MERCHANT OR
PROCEDURE time out;
End comm mc;
The time out procedure aborts the transaction if goods are not received within a speci?ed period. Adding this procedure obviates the problem identi?ed above.
There are other areas of possible vulnerability that can be explored in a similar fashion. The point of these examples is to demonstrate that once a requirement is speci?ed, its implementation can readily be veri?ed with a model checker. This is a critical step in designing e-business standards since translating concepts to implementation often leads to error or omission.
V. DISCUSSION
The objective of this paper is to provide an accessible explication and demonstration of the ef?ciency and effectiveness of using a model checker to evaluate the reliability of transaction protocols within e-business processes. In particular, when many processes are distributed and automated, there are many states within those processes
that need to be evaluated. Evidence suggests that such an evaluation is beyond the practical capabilities of manual procedures, theorem provers, and simulation, leaving e-business partners vulnerable to unforeseen failures and corresponding costs and losses. Model checkers do not guarantee discovery of all vulnerabilities; but if designers are a ble to identify a full range of speci?cations that a system must satisfy,model checkers provide ef?cient and effective veri?cation. Notably,model checkers provide counterexamples that de?ne sequences of processes that lead to failure.
We have shown that the key elements of an e-business protocol can be represented using a model checker such as FDR. Since the elements of the e-business protocol that we have incorporated in this study are a subset of the protocols within a large class of e-business applications,there is considerable potential for broader applications. Given current concerns about Internet security, model checkers may have potential in both designing and auditing a variety of system implementations. For example, as web-support services develop the capability for accessing public registries of vendors, both search and subsequent transaction processes may bene?t from application of model-checking technology.
Model checkers may also prove valuable in examining the processes of highly integrated applications found in enterprise resource-planning(ERP) systems.
A feature of model checking that should be of particular interest to e-business designers is the capability of developing speci?cation statements that must be satis?ed by implementation. For demonstration purposes, our presentation has focused on money atomicity, goods atomicity, valid receipt, and communication link failures because these are fundamental to e-business; however, model checking can be used to test a wide variety of protocol features. This approach should help not only systems designers, but also auditors. Systems that are examined by auditors need to have adequate controls built in prior to implementation and will need adequate auditing
after implementation to ensure that none of the processes have been corrupted.
Where as model checking provides a viable formal method for evaluating the security and reliability of e-business processes, some limitations apply. As noted previously, there is little purpose in verifying an e-business system with an incorrect model. This study assumes the model will be correctly de?ned and coded into a model checker. Model checkers do not build correct models; instead, they help verify the models.
The CSP model-checking language can be complex for practitioners to use, but more accessible approaches are becoming available. For example, a recently developed model-checking language called Casper has overcome CSP’s complexity by adding a higher-level language whose interpreter translates code into CSP.
Whate ver language is used, it is important to emphasize that once a speci?cation is veri?ed it can be continually reused, regardless of the system used to conduct the process. Thus, the up-front investment in process modeling and model checking can yield long-term dividends in terms of system security and reliability as system upgrades and changes are implemented.
Future research could explore issues related to ensuring the accuracy of the model coded into the model checker. Additional studies could also examine ways to educate potential users of e-business systems on features that have been veri?ed and their meaning. Research might also be conducted on comparative performance and
ef?ciency of alternative model checkers. Finally, empirical tests of model-checking principles may help to validate the accuracy and effectiveness of these theories.
VI. CONCLUSION
E-business is moving forward at a rapid pace across the globe, exposing businesses to e-business processes that rely on interdependen cies among customers, merchants, and TTPs. New e-business foci, such
as web services and pervasive computing, will extend the reach of e-business, but these may also increase complexity and exposure pos sibilities. This will necessitate proactive veri?cation of related models.
Model checking could become a fundamental tool in this process.
REFERENCES
[1] W. Janssen, R. Mateescu, S. Mauw, P. Fennema, and P. van der Stappen,
“Model checking for managers,‖ in Proc. 6th Int. SPIN Workshop Practical Aspects Model Checking, Toulouse, France, Sep. 1999, pp. 92–107.
[2] W. Wang, Z. Hidvegi, A. Bailey, and A. Whinston, ―E-process design and assurance using model checking,‖ IEEE Trans. Comput., vol. 33,no. 10, pp. 48–53, Oct. 2000.
[3] F. Coyle, XML, Web Services, and the Data Revolution. Reading,
MA:Addison-Wesley, 2002.
[4] J. Kopena and W. Regli, ―DAMLJessKB: A tool for reasoning with the semantic web,‖ IEEE Intell. Syst., vol. 18, no. 3, pp. 74–77, May/Jun.2003.
[5] W. Wang, Z. Hidvegi, A. Bailey, and A. Whinston, ―Model checking—Arigor ous and ef?cient tool for e-commerce internal control and assurance,‖ in Working Paper. Atlanta, GA: Gozuita School Bus., Emory Univ., 2001.
[6] J. Wing, ―A symbiotic relationship between formal methods and security,‖ in Proc. Workshops Computer Security, Fault Tolerance, Software Assurance: From Needs to Solution, CMU-CS-98-188, 1998, pp. 1–12.
[7] G. Lowe, ―Breaking and ?xing the Needham-Schroeder public-key protocol using FDR,‖ in Proc. Tools Algorithms Construction Analysis Systems: Second International Workshop, 1996, pp. 147–166.
[8] A. Roscoe, The Theory and Practice of Concurrency. Upper SaddleRiver, NJ: Prentice-Hall, 1998.
[9] N. Heintze, J. Tygar, J. Wing, and H. Wong, ―Model checking electroniccommerce protocols,‖ in Proc. 2nd USENIX Workshop Ele ctronic Commerce, 1996, pp. 147–165.
[10] I. Ray, I. Ray, and N. Narasimhamurthi, ―A fair exchange e-commerce protocol with automated dispute resolution,‖ in Proc. 14th Annu, IFIP
WG 11.3 Working Conf. Database Security, Schoorl, The Netherlands,Aug. 2000, pp. 27–38.
[11] E. Clarke, O. Grumberg, and D. Peled, Model Checking. Cambridge,MA: MIT Press, 1999.
[12] P. Ryan and S. Schneider, The Modeling and Analysis of Security Pro-tocols: The CSP Approach. Reading, MA: Addison-Wesley, 2001.
01 THE ELEMENTS AND THE PERIODIC TABLE 01 元素和元素周期表 The number of protons in the nucleus of an atom is referred to as the atomic number, or proton number, Z. The number of electrons in an electrically neutral atom is also equal to the atomic number, Z. The total mass of an atom is determined very nearly by the total number of protons and neutrons in its nucleus. This total is called the mass number, A. The number of neutrons in an atom, the neutron number, is given by the quantity A-Z. 质子的数量在一个原子的核被称为原子序数,或质子数、周淑金、电子的数量在一个电中性原子也等于原子序数松山机场的总质量的原子做出很近的总数的质子和中子在它的核心。这个总数被称为大量胡逸舟、中子的数量在一个原子,中子数,给出了a - z的数量。 The term element refers to, a pure substance with atoms all of a single kind. T o the chemist the "kind" of atom is specified by its atomic number, since this is the property that determines its chemical behavior. At present all the atoms from Z = 1 to Z = 107 are known; there are 107 chemical elements. Each chemical element has been given a name and a distinctive symbol. For most elements the symbol is simply the abbreviated form of the English name consisting of one or two letters, for example: 这个术语是指元素,一个纯物质与原子组成一个单一的善良。在药房“客气”原子的原子数来确定它,因为它的性质是决定其化学行为。目前所有原子和Z = 1 a到Z = 107是知道的;有107种化学元素。每一种化学元素起了一个名字和独特的象征。对于大多数元素都仅仅是一个象征的英文名称缩写形式,一个或两个字母组成,例如: oxygen==O nitrogen == N neon==Ne magnesium == Mg
美国大学校名英文缩写 英文缩写英文全称中文全称 AAMU Alabama A&M 阿拉巴马农业机械大学ADELPHI Adelphi University 艾德菲大学AMERICAN American University 美国大学 ANDREWS Andrews University 安德鲁大学 ASU Arizona State University 亚利桑那州立大学AUBURN Auburn University 奥本大学 -B- BAYLOR Baylor University 贝勒大学 BC Boston College 波士顿学院 BGSU Bowling Green State University 博林格林州立大学BIOLA Biola University 拜欧拉大学BRANDEIS Brandeis University 布兰迪斯大学BROWN Brown University 布朗大学 BSU Ball State University 波尔州立大学 BU* Boston University 波士顿大学 BU SUNY Binghamton 纽约州立大学宾厄姆顿分校BYU Brigham Young Univ. Provo 百翰大学 *BU通常意义上指Boston University -C- CALTECH California Institute of Technology 加州理工大学 CAU Clark Atlanta University 克拉克亚特兰大大学 CLARKSON Clarkson University 克拉逊大学CLARKU Clark University 克拉克大学CLEMSON Clemson University 克莱姆森大学 CMU* Carnegie Mellon University 卡耐基梅隆大学CMU Central Michigan University 中央密歇根大学COLUMBIA Columbia University 哥伦比亚大学CORNELL Cornell University 康奈尔大学CSU* Colorado State 科罗拉多州立大学 CSU Cleveland State University 克里夫立大学CU* University of Colorado Boulder 科罗拉多大学波德分校 CU University of Colorado Denver 科罗拉多大学丹佛分校 CUA Catholic University of America 美国天主教大学 CWRU Case Western Reserve Univ. 凯斯西储大学*CMU 通常意义上指 Carnegie Mellon University *CSU 通用 *CU 通用
1 Unit5元素周期表 As our picture of the atom becomes more detailed 随着我们对原子的描述越来越详尽，我们发现我们陷入了进退两难之境。有超过100多中元素要处理，我们怎么能记的住所有的信息？有一种方法就是使用元素周期表。这个周期表包含元素的所有信息。它记录了元素中所含的质子数和电子数，它能让我们算出大多数元素的同位素的中子数。它甚至有各个元素原子的电子怎么排列。最神奇的是，周期表是在人们不知道原子中存在质子、中子和电子的情况下发明的。Not long after Dalton presented his model for atom( )在道尔顿提出他的原子模型（原子是是一个不可分割的粒子，其质量决定了它的身份）不久，化学家门开始根据原子的质量将原子列表。在制定像这些元素表时候，他们观察到在元素中的格局分布。例如，人们可以清楚的看到在具体间隔的元素有着相似的性质。在当时知道的大约60种元素中，第二个和第九个表现出相似的性质，第三个和第十个，第四个和第十一个等都具有相似的性质。 In 1869,Dmitri Ivanovich Mendeleev,a Russian chemist, 在1869年，Dmitri Ivanovich Mendeleev ,一个俄罗斯的化学家，发表了他的元素周期表。Mendeleev通过考虑原子重量和元素的某些特性的周期性准备了他的周期表。这些元素的排列顺序先是按原子质量的增加,,一些情况中, Mendeleev把稍微重写的元素放在轻的那个前面.他这样做只是为了同一列中的元素能具有相似的性质.例如,他把碲(原子质量为128)防在碘(原子质量为127)前面因为碲性质上和硫磺和硒相似, 而碘和氯和溴相似. Mendeleev left a number of gaps in his table.Instead of Mendeleev在他的周期表中留下了一些空白。他非但没有将那些空白看成是缺憾，反而大胆的预测还存在着仍未被发现的元素。更进一步，他甚至预测出那些一些缺失元素的性质出来。在接下来的几年里，随着新元素的发现，里面的许多空格都被填满。这些性质也和Mendeleev所预测的极为接近。这巨大创新的预计值导致了Mendeleev的周期表为人们所接受。 It is known that properties of an element depend mainly on the number of electrons in the outermost energy level of the atoms of the element. 我们现在所知道的元素的性质主要取决于元素原子最外层能量能级的电子数。钠原子最外层能量能级（第三层）有一个电子，锂原子最外层能量能级（第二层）有一个电子。钠和锂的化学性质相似。氦原子和氖原子外层能级上是满的，这两种都是惰性气体，也就是他们不容易进行化学反应。很明显，有着相同电子结构（电子分布）的元素的不仅有着相似的化学性质，而且某些结构也表现比其他元素稳定（不那么活泼） In Mendeleev’s table,the elements were arranged by atomic weights for 在Mendeleev的表中，元素大部分是按照原子数来排列的，这个排列揭示了化学性质的周期性。因为电子数决定元素的化学性质，电子数也应该（现在也确实）决定周期表的顺序。在现代的周期表中，元素是根据原子质量来排列的。记住，这个数字表示了在元素的中性原子中的质子数和电子数。现在的周期表是按照原子数的递增排列，Mendeleev的周期表是按照原子质量的递增排列，彼此平行是由于原子量的增加。只有在一些情况下（Mendeleev注释的那样）重量和顺序不符合。因为原子质量是质子和中子质量的加和，故原子量并不完全随原子序数的增加而增加。原子序数低的原子的中子数有可能比原子序数高的原
一、国家及校级奖项、称号 国家奖学金National Scholarship 国家励志奖学金National Encouragement scholarship 三好学生标兵Pacemaker to Merit Student 三好学生Merit Student 学习优秀生Model Student of Academic Records 突出才能奖Model Student of Outstanding Capacity 先进个人Advanced Individual/Outstanding Student 优秀工作者Excellent staff 优秀学生干部Excellent Student Cadre 优秀共青团员Excellent League Member 优秀毕业生Outstanding Graduates 优秀志愿者Outstanding Volunteer 先进班集体Advanced Class 优秀团干Outstanding League Cadres 学生协会优秀干部Outstanding leaders of Student Association 学生协会工作优秀个人Outstanding Individual of Student Association 精神文明先进个人Spiritual Advanced Individual 社会工作先进个人Advanced Individual of Social Work 文体活动先进个人Advanced Individual of Cultural and sports activities 道德风尚奖Ethic Award 精神文明奖High Morality Prize 最佳组织奖Prize for The Best Organization 突出贡献奖Prize for The Outstanding Contribution 工作创新奖Prize for The Creative Working 团队建设奖Prize for The Team Contribution 大学英语四级CET4 (College English Test Band 4 Certificate) 大学英语六级CET6 (College English Test Band 6 Certificate) 全国计算机一级证书First-level Certificate for National Computer 全国计算机二级证书Second-level Certificate for National Computer 全国计算机三级证书Third-level Certificate for National Computer 全国计算机四级证书Fourth-level Certificate for National Computer 学生会Student Union 团委会Youth League Committee 学生社团Students’ Association 体育部Sports Department 文艺部Arts Department 学习部Learning Department
01.THE ELEMENTS AND THE PERIODIC TABLE 01元素和元素周期 表。 The number of protons in the nucleus of an atom is referred to as the atomic number, or proton number, Z. The number of electrons in an electrically neutral atom is also equal to the atomic number, Z. The total mass of an atom is determined very nearly by the total number of protons and neutrons in its nucleus. This total is called the mass number, A. The number of neutrons in an atom, the neutron number, is given by the quantity A-Z. 原子核中的质子数的原子称为原子序数，或质子数，卓电子数的电中性的原子也等于原子序数Z，总质量的原子是非常接近的总数量的质子和中子在原子核。这被称为质量数，这个数的原子中的中子，中子数，给出了所有的数量 The term element refers to, a pure substance with atoms all of a single kind. To the chemist the "kind" of atom is specified by its atomic number, since this is the property that determines its chemical behavior. At present all the atoms from Z = 1 to Z = 107 are known; there are 107 chemical elements. Each chemical element has been given a name and a distinctive symbol. For most elements the symbol is simply the abbreviated form of
Uｎit 1 The RｏotｓoｆCｈemisｔry Ｉ．Ｃoｍpreｈensioｎ. 1。Ｃ 2. Ｂ3．D 4. C 5. B ＩI。Ｍａｋe ａsenｔeｎｃe ｏut of ｅach ｉｔem ｂy reaｒranging ｔhe wordｓin ｂracｋets. 1.Tｈｅｐuｒiｆｉcation of aｎorganｉc compounｄis usually a matter of consｉｄerａｂlｅdｉfｆicｕｌtｙ, and iｔis nｅcｅｓsaｒy to eｍploy vａrious methoｄs fｏr thｉｓpurpｏse。 2.Science is an ｅｖeｒ－iｎcｒｅasing boｄy ofａccｕｍｕlａｔed anｄ ｓｙsｔｅmatiｚed knowledｇe ａnd iｓalsｏan activｉty bｙwｈic ｈｋnowledge iｓｇenerated。 3.Lifｅ，aftｅr all, is onｌy cｈeｍistry,in faｃｔ, a sｍall example of ｃ hｅｍistry ｏbsｅｒved oｎａsｉngle munｄane pｌａnet。 4.Peoplｅaｒe made of molｅculｅｓ; sｏmｅｏf ｔhｅmｏleculｅs in p ｅople aｒe rａｔher ｓimple whｅreas otｈerｓａｒｅhｉghly compｌex。 5.Chｅｍistry ｉｓever preseｎｔin ｏｕｒｌｉves frｏm ｂｉｒtｈ tｏｄeａthｂeｃａｕse withoｕt chｅmｉｓtrｙｔhere iｓneither life nor deａth. 6.Maｔhｅｍaｔics apｐeａｒs ｔo be almost as humaｎkiｎｄand ａｌ ｓo ｐermeaｔeｓall aspeｃts of ｈuman life, aｌthough ｍａｎｙof us are ｎｏｔfuｌly ａwａrｅoｆtｈis. III。Tｒanｓlatioｎ. 1.（a)chｅmicaｌprｏcess (b) natuｒal scienｃe（c）the teｃhｎｉ ｑｕe of distｉllaｔioｎ 2.Iｔｉs theａtｏｍs that ｍａkｅuｐｉron, waｔeｒ，oｘygen and the lｉke/anｄso on／aｎｄsｏfortｈ/aｎd otherｗiｓe. 3.Cheｍisｔｒy haｓa very long hｉｓtorｙ, ｉnｆaｃｔ，human a ｃtivity in chｅｍｉstrｙgｏes bａｃk ｔo ｐreｒecｏrｄed tｉmｅｓ/pｒedatiｎg reｃｏrded times． 4.Aｃcoｒdｉng to/Froｍthe eｖapoｒaｔion oｆwaｔeｒ，pｅople know ／reaｌized ｔｈat ｌiquidｓcａn ｔurn/bｅ/changeｉｎto gases ｕndeｒcertain conditions/circｕmsｔance／enｖironment。 5.Yoｕｍusｔknow ｔhe propｅｒtieｓｏfｔｈe materiaｌbeｆore y ｏu use it. IＶ．Ｔrａnslation 化学是三种基础自然科学之一,另外两种是物理和生物.自从宇宙大爆炸以来，化学过程持续进行,甚至地球上生命的出现可能也是化学过程的结果。人们也许认为生命是三步进化的最终结果,第一步非常快，其余两步相当慢.这三步
第一名The First Prize 第二名The Second Prize 第三名The Third Prize 三好学生标兵Pacemaker to Merit Student 三好学生Merit Student 学习优秀生Model Student of Academic Records 突出才能奖Model Student of Outstanding Capacity 先进个人Advanced Individual/Outstanding Student 优秀工作者Excellent staff 优秀学生干部Excellent Student Cadre 优秀共青团员Excellent League Member 优秀毕业生Outstanding Graduates 优秀志愿者Outstanding Volunteer 先进班集体Advanced Class 优秀团干Outstanding League Cadres 学生协会优秀干部Outstanding cadres of Student Association 学生协会工作优秀个人Outstanding Individual of Student Association 精神文明先进个人Spiritual Advanced Individual 社会工作先进个人Advanced Individual of Social Work 文体活动先进个人Advanced Individual of Cultural and sports activities 道德风尚奖Ethic Award 精神文明奖 最佳组织奖 突出贡献奖 工作创新奖High Morality Prize Prize for The Best Organization Prize for The Outstanding Contribution Prize for The Creative Working 团队建设奖Prize for The Team Contribution 体育道德风尚奖PE Morality Award 优秀指导教师奖Excellent Guide Teacher Award 突出贡献奖Outstanding Contribution Award 工作创新奖Innovation Award 团队建设奖Teamwork Award 最佳台风奖Best Stage Style Award 最佳人气奖Best Popularity Award 优秀组织奖Outstanding Organization Award 最佳创意奖Best Creativity Award 优秀团体奖Excellent Group Award 优秀节目奖Best Program Award 十佳新秀奖Top Ten Outstanding Rising Stars Award 最具潜质奖Most Potentiality Award 最佳才艺奖Outstanding Talent Award 最佳气质奖Outstanding Quality Award 最佳口才奖Best Eloquence Award 最佳演员奖Best Actor Award
Unit 1 Chemical Industry 化学工业 1.Origins of the Chemical Industry Although the use of chemicals dates back to the ancient civilizations, the evolution of what we know as the modern chemical industry started much more recently. It may be considered to have begun during the Industrial Revolution, about 1800, and developed to provide chemicals roe use by other industries. Examples are alkali for soapmaking, bleaching powder for cotton, and silica and sodium carbonate for glassmaking. It will be noted that these are all inorganic chemicals. The organic chemicals industry started in the 1860s with the exploitation of William Henry Perkin‘s discovery if the first synthetic dyestuff—mauve. At the start of the twentieth century the emphasis on research on the applied aspects of chemistry in Germany had paid off handsomely, and by 1914 had resulted in the German chemical industry having 75% of the world market in chemicals. This was based on the discovery of new dyestuffs plus the development of both the contact process for sulphuric acid and the Haber process for ammonia. The later required a major technological breakthrough that of being able to carry out chemical reactions under conditions of very high pressure for the first time. The experience gained with this was to stand Germany in good stead, particularly with the rapidly increased demand for nitrogen-based compounds (ammonium salts for fertilizers and nitric acid for explosives manufacture) with the outbreak of world warⅠin 1914. This initiated profound changes which continued during the inter-war years (1918-1939). 1．化学工业的起源 尽管化学品的使用可以追溯到古代文明时代，我们所谓的现代化学工业的发展却是非常近代（才开始的）。可以认为它起源于工业革命其间，大约在1800年，并发展成为为其它工业部门提供化学原料的产业。比如制肥皂所用的碱，棉布生产所用的漂白粉，玻璃制造业所用的硅及Na2CO3. 我们会注意到所有这些都是无机物。有机化学工业的开始是在十九世纪六十年代以William Henry Perkin 发现第一种合成染料—苯胺紫并加以开发利用为标志的。20世纪初，德国花费大量资金用于实用化学方面的重点研究，到1914年，德国的化学工业在世界化学产品市场上占有75%的份额。这要归因于新染料的发现以及硫酸的接触法生产和氨的哈伯生产工艺的发展。而后者需要较大的技术突破使得化学反应第一次可以在非常高的压力条件下进行。这方面所取得的成绩对德国很有帮助。特别是由于1914年第一次世界大仗的爆发，对以氮为基础的化合物的需求飞速增长。这种深刻的改变一直持续到战后（1918-1939）。 date bake to/from: 回溯到 dated: 过时的，陈旧的 stand sb. in good stead: 对。。。很有帮助
中外高校校名国内研究所中文全称和英文缩写 对照 集团文件发布号：（9816-UATWW-MWUB-WUNN-INNUL-DQQTY-
中文全称英文缩写 浙江大学ZHEJIANG UNIV 中国科学院CHINESE ACAD SCI 清华大学TSINGHUA UNIV 东南大学SOUTHEAST UNIV 大连理工大学DALIAN UNIV TECHNOL 南京大学NANJING UNIV 四川大学SICHUAN UNIV 上海交通大学SHANGHAI JIAO TONG UNIV 中山大学SUN YAT SEN UNIV 华中科技大学HUAZHONG UNIV SCI TECHNOL 北京大学PEKING UNIV 山东大学SHANDONG UNIV 复旦大学FUDAN UNIV 南开大学NANKAI UNIV 北京邮电大学BEIJING UNIV POSTS TELECOMMUN 中国科学技术大学UNIV SCI TECHNOL CHINA 吉林大学JILIN UNIV 西安交通大学XI AN JIAO TONG UNIV 哈尔滨工业大学HARBIN INST TECHNOL 天津大学TIANJIN UNIV 兰州大学LANZHOU UNIV 华南理工大学S CHINA UNIV TECHNOL 武汉大学WUHAN UNIV 湖南大学HUNAN UNIV 华南师范大学S CHINA NORMAL UNIV 北京航天航空大学BEIJING UNIV AERONAUT ASTRONAUT 东北大学NORTHEASTERN UNIV 电子科技大学UNIV ELECT SCI TECHNOL CHINA 华东科技大学 E CHINA UNIV SCI TECHNOL 中南大学CENT S UNIV 西安电子科技大学XIDIAN UNIV 同济大学TONGJI UNIV 厦门大学XIAMEN UNIV 北京交通大学BEIJING JIAOTONG UNIV 东吴大学SOOCHOW UNIV 安徽大学ANHUI UNIV 北京理工大学BEIJING INST TECHNOL 香港城市大学CITY UNIV HONG KONG 湘潭大学XIANGTAN UNIV 北京师范大学BEIJING NORMAL UNIV
黄冈师范学院 2009—2010学年度第一学期期末试卷考试课程：专业英语考核类型：考试A卷 考试形式：闭卷出卷教师：杨一思 考试专业：化学考试班级：应用化学200601 一、Translate the following into English（20 points） 1.过滤 2.浓缩 3.结晶化 4.吸附 5. 蒸馏6．超临界的 7.二氯甲烷 8.热力学平衡 9.亲电性 10.表面张力 11.共轭的 12.酮 13.平衡常数 14.丙基 15.丁基 16.亚甲基 18.环己酮 19.同位素 20.标准熵 二、Translate the following into Chinese（20 points） 1. methyl propanoate 2. rate constant 3. ethyl methyl ketone 4. free energy 5. radical intermediate 6. isobutyl methyl ether 7. 3-chloropropene 8. primary radical 9. n-propyl bromide 10. bond energy 11. circulating electrons 12. local magnetic fields 13. tetramethylsilane 14. mass to charge ratios 15 phenylamine 16 amide 17. amine 18. nucleophile 19. perchlorate 20. carbocation 三、Translation the following into chinese （40 points） A卷【第1页共 3 页】
仅供参考 Introduction to Organic Chemistry 1. Sources of Organic Compounds The major sources of organic chemicals are coal, petroleum, and agricultural products. Both coal and petroleum were formed through the geologic processes of changing animal and plant remains into carbon-containing residues. About one-third of all organic chemicals are derived from coal and about one-half from the petroleum industry 有机化合物的来源 有机化学药品的主要来源是煤、石油和农产品。动植物的遗体通过地质作用变成含碳残基然后形成煤和石油。三分之一的所有有机化合物品是从煤中得到的，一般来自于石油工业。 2. The Methods and Objectives of Organic Chemistry Because of the tremendous number of organic compounds known, and of the many more being synthesized daily, the study of organic chemistry is not the study of individual compounds, it is the study of groups or families of compounds all closely related to each other. Obviously, the former approach would be prohibitive[prE5hibitiv]. Once the structural relationships of certain typical members of a particular group or family of compounds are understood, these structural features are understood for any one of the many members of the family, even though some may not be known compounds. 因为已知的有机化合物的数目庞大，而且还在逐日合成更多的品种，所以有机化学不是研究单个的化合物，而是把彼此密切相关的化合物按类或族来研究。显然，以前的方法是不可取的，一旦典型的一类特殊化合物被认识，这些结构特征将适用于这类化合物，甚至是一些未知的化合物， For each group or family of compounds often called homologous series of compounds, structural features are important. In studying organic chemistry, it is not enough to know the identities of the elements and how many atoms of each element are present in a given molecule. More importantly, the order in which these atoms are linked together to form
南京大学Nanjing University 东南大学Southeast University 南京航空航天大学Nanjing University of Aeronautics and Astronautics 南京理工大学Nanjing university ofscience ＆technology 南京工业大学Nanjing tech university 南京邮电大学Nanjing University of Posts and Telecommunications 南京林业大学Nanjing forestry university 南京信息工程大学Nanjing University of Information Science & Technology 南京农业大学Nanjing Agricultural University 南京医科大学Nanjing medical university 南京中医药大学Nanjing university of Chinese medicine 中国药科大学China Pharmaceutical University 南京师范大学Nanjing Normal University 南京财经大学Nanjing University Of Finance & Economics 江苏警官学院Jiangsu police institute 南京体育学院Nanjing Sport Institute 南京艺术学院Nanjing University of the Arts 三江学院Sanjiang university 南京工程学院Nanjing institute of technology 南京审计大学Nanjing audit university 南京晓庄学院Nanjing xiaozhuang university 南京特殊教育师范学院Nanjing Normal University Of Special Education 南京森林警察学院Nanjing forest police college 东南大学成贤学院southeast university chengxian college 金陵科技学院jinling institute of technology 南京大学金陵学院Nanjing university jinling college 南京理工大学紫金学院Nanjing University of Science and Technology ZiJin College 南京航空航天大学金城学院 nanhang Jincheng college 中国传媒大学南广学院Communication University of China, Nanguang College
Unit10 Nomenclature of Hydrocarbons碳氢化合物的命名 Alkanes烷烃 理想的，每一种化合物都应该由一个明确描述它的结构的名称，并且通过这一名称能够画出它的结构式。为了这一目的，全世界的化学家接受了世界纯粹与应用化学会（IUPAC）建立的一系列规则。这个系统就是IUPAC系统，或称为日内瓦系统，因为IUPAC的第一次会议是在瑞士日内瓦召开的。不含支链的烷烃的IUPAC命名包括两部分（1）表明链中碳原子数目的前缀；（2）后缀－ane，表明化合物是烷烃。用于表示1至20个碳原子的前缀见表 表中前4个前缀是由IUPAC选择的，因为它们早已在有机化学中确定了。实际上，它们甚至早在它们成为规则之下的结构理论的暗示之前，它们的地位就确定了。例如，在丁酸中出现的前缀but－，一种表示在白脱脂中存在的四个碳原子的化合物（拉丁语butyrum白脱（黄油））。表示5个或更多碳原子的词根来源于希腊或拉丁词根。 含取代基的烷烃的IUPAC名称由母体名称和取代基名称组成，母体名称代表化合物的最长碳链，取代基名称代表连接在主链上的基团。 来源于烷烃的取代基称为烷基。字母R－被广泛用来表示烷烃的存在.烷烃的命名是去掉原烷基名称中的－ane加上后缀－yl。例如，烷基CH3CH2－称为乙基。 CH3－CH3乙烷（原碳氢化合物）CH3CH2－乙基（一个烷基） 下面是IUPAC的烷烃命名规则： 1. 饱和碳氢化合物称为烷烃。 2. 对有支链的碳氢化合物，最长的碳链作为主链，IUPAC命名按此主链命名。 3. 连接在主链上的基团称为取代基。每一取代基有一名称和一数字.这一数字表示取代基连接在主链上的碳原子的位置。 4. 如果有多于一个的相同取代基，要给出表示支链位置的每个数字。而且，表示支链数目的数字由前缀di－，tri－，tetra－，penta－等表示。 5. 如果有一个取代基，主链碳原子编号从靠近支链的一端开始，使支链位号最小。如果有两个或多个取代基，支链从能使第一个取代基位次较小的一侧编号。 6. 如果有两个或多个取代基，它们按字母顺序排列。当排列取代基时，前缀iso－（异）和neo－（新）也按字母排列，前缀sec－（仲）和tert－（特）在字母排列中忽略 此外，按字母排列取代基时，表示倍数的前缀2，3，4等也被忽略。 Alkenes烯烃 烷烃的碳原子间只有单键。烯烃在两个碳原子间有双键（两个键）。考虑到两个碳原子间以双键相连。因为双键用去了两个碳原子的共4个电子。所以只剩下4个电子以供成
１０级应用化学（2）班郑禄春 B2０1０06３224 Lessｅn ２4 ChemicａｌＲeaｃtionｓ Conseｒvation of mａｓs ａnd ｅｎergy(质量与能量守恒) Ｔwo ｃonseｒvaｔｉｏn laws（定律) apｐlｙｔo aｌｌｃhemical reaｃtionｓ: E ｎergy can neitheｒ be cｒｅated nｏr deｓtroｙed, anｄｍａｔteｒｃaｎneither ｂｅ created nor deｓtｒｏyed. Thus the ａtoms taking part in a chemical reactioｎ may be reａrrangｅd, bｕt all ｔhe atoms preseｎt ｉn the reacｔan ｔs must also be preｓent in ｔhe prodｕctｓ, and the tｏtaｌｍasｓ oｆ tｈe ｒeactants muｓt equaｌ thｅｔotaｌｍａss ｏｆthe prｏducts. 化学反应 质量守恒和能量守恒 两个守恒定律(定律)适用于所有的化学反应:能量既不能创造也不能消灭,物质也不能创造也不能消灭。因此原子参与化学反应可能重新安排，但所有的原子出现在反应物必须包含在产品,反应物的总质量必须等于生产物的总质量。 What is ａ chｅmicaｌ reaction? A chｅmicaｌreaｃtiｏn occｕｒs whｅn sｕbsｔａnｃes (tｈe ｒｅactantｓ) colｌide (碰撞）ｗiｔh ｅnouｇｈ energｙ tｏｒearｒａnge to form difｆerent c ｏｍpounds (ｔhe ｐrｏdｕcts）. The changｅ iｎ enerｇy that occurs wheｎ a reaction take pｌａｃe ｉs deｓcriｂed by therｍｏdｙｎaｍics（热力学）anｄt ｈe ｒａｔｅ oｒ speed at which a reacｔioｎocｃurｓis descｒibed by kiｎeticｓ (动力学) . Reacｔions in ｗhiｃh ｔｈe ｒeaｃtａnｔｓaｎd ｐrｏductｓcoｅxist arｅ coｎｓidｅｒed ｔo be in equilｉｂriuｍ(处于平衡）. A chｅｍiｃａl ｅｑuaｔion ｃonsｉｓts ｏf the ｃhemｉｃal fｏrmｕｌａ（化学式)of thｅ rea ｃｔants, and ｔhe cｈemical fｏｒmｕla of ｔhe ｐrodｕcts. The twｏａre separateｄ bｙａn → uｓually read aｓ“yｉelｄs”ａnｄeach ｃhemicａl forｍula is sｅpａｒatｅd frｏm otheｒs by ａ plus sｉgn (加号）． Sometime ｓ a trｉangｌe is dｒawｎ over ｔhe arrow symbol tｏｄenotｅ enerｇy ｍuｓt ｂe addeｄｔo ｔｈe subsｔances ｆor ｔhe ｒeａcｔiｏn to beｇｉn． Eａch ｃｈemiｃaｌ formula may be pｒｅｃeded by a sｃalaｒ（数量的) ｃoｅｆficienｔｉndicatｉng thｅ proｐorｔion (比例) ｏｆ that substaｎce nｅｃｅssary to ｐｒoｄｕce ｔhe rｅacｔion in forｍulａ. Foｒinstanｃe， thｅｆoｒmｕla ｆoｒ the buｒning of mｅthane(CH4 + 2O2 →ＣO2 + 2H2O） iｎdｉｃates that twｉce as much Ｏ2 aｓ CH４ iｓ nｅｅded, and wｈen tｈey reａct， twicｅas ｍuch H2O as ＣO2 wｉll be produceｄ. This is ｂecａuse durｉng tｈe reａctiｏｎ，each atom ｏｆ cａrbon needｓ eｘａctlｙ two atoms ｏf oxygen ｔo combｉnｅ with, to ｐroduｃe the CO2, and ｅvｅry twｏaｔｏms of ｈydrｏgen need an atｏm ｏf oxygen tｏcombine wiｔｈｔo proｄuce ｔhｅH２O． If thｅ pｒｏportiｏns ｏf thｅ reactaｎtｓarｅ nｏｔ reｓpecｔed, when ｔhey arｅ foｒｃｅd ｔｏreacｔ, eitheｒ not all oｆｔhe ｓuｂstance used wilｌparticipate in tｈe re ａｃｔion, or the reａctiｏｎ that wｉll take pｌace ｗilｌbｅ dｉｆfｅｒent ｆｒom tｈe ｏne noteｄin ｔhｅ equatｉon.. 什么是化学反应 一个化学反应发生在物质（反应物）碰撞有足够的能量去重新排列,形成不同的化合物(产品）。当反应发