Under consideration for publication in Formal Aspects of Computing
Speci?cation and Veri?cation of the Tree Identify Protocol of IEEE1394 in Rewriting Logic
Alberto Verdejo,Isabel Pita,and Narciso Mart′?-Oliet
Dpto.de Sistemas Inform′a ticos y Programaci′o n
Universidad Complutense de Madrid.Spain
Abstract.We present three descriptions,at di?erent abstract levels,of the tree identify protocol from the IEEE1394serial multimedia bus standard.The descriptions are given using the language Maude based on rewriting logic.Particularly,the time aspects of the protocol are studied.We prove the correctness of the protocol in two steps.First,the descriptions are validated by an exhaustive exploration of all the possible states reachable from an initial con?guration of a network,checking that always only one leader is chosen. Then,we give a formal proof showing that the desirable properties of the protocol are always ful?lled by any network,provided that the network is connected and acyclic.
Keywords:Rewriting logic,Maude,IEEE1394,tree identify protocol,object-oriented speci?cations.
1.Introduction
Rewriting logic[Mes92,Mes98]and its implementation language Maude[CDE+02,CDE+00b]have emerged as an excellent framework where communication protocols can be speci?ed and analyzed[DMT98,DMT00]. Rewriting logic was?rst proposed by Meseguer as a uni?ed framework for concurrency in1990.Since then much work has been done on the use of rewriting logic as a logical and semantic framework[MOM93],and on the development of the Maude language[CDE+02].In the last few years the application of rewriting logic and Maude to the speci?cation of real systems has started,mainly for applications of distributed architectures and communication protocols[DMT98].A formal methodology for specifying and analyzing communication protocols is presented in[DMT00].It is arranged as a sequence of increasingly stronger methods,including:
1.Formal speci?cation,in order to obtain a formal model of the system,in which ambiguities are clari?ed.
2.Execution of the speci?cation,for simulation and debugging purposes,leading to better versions of the
speci?cation.
2 A.Verdejo,I.Pita,and N.Mart′?-Oliet
3.Formal model-checking analysis,in order to?nd errors by considering all possible behaviors of highly
distributed and nondeterministic systems.
4.Narrowing analysis,in which all behaviors from the possibly in?nite set of states described by a symbolic
expression are analyzed.
5.Formal proof,where the correctness of critical properties is veri?ed by using a formal technique.
In this paper we use methods1–3to specify and analyze three descriptions of the tree identify protocol of the IEEE1394serial multimedia bus standard(the“FireWire”),and we use method5to verify them.We have not been able to perform any narrowing analysis because the current Maude system does not support it yet.
As this volume shows,this example is becoming something of a benchmark for formal methods[MS00, SMR01].We show how Maude,a high-level language and high-performance system supporting both equa-tional and rewriting logic computation,can also be used as a formal speci?cation language.We use the object-oriented speci?cation style of Maude[CDE+02],which allows formalization of both synchronous and asynchronous concurrent object systems.We add time aspects(quite important for this protocol)to these object-oriented speci?cations following ideas presented in[¨OM02].
Most of the works presented in[SMR01]use abstract formalisms and tools which are not well suited for directly executing the protocol itself,although,of course,all those tools have di?erent important strengths of their own.The point is that executable speci?cation methods and tools can complement those strengths in new ways.As pointed out in[¨Olv00],one can think of rewriting logic(and Maude)as covering an intermediate operational level,that can substantially help in bridging the gap between more abstract,property-oriented, speci?cations and actual implementations by providing support for executable speci?cations,support for useful techniques of automated or semi-automated formal reasoning(such as strategy-based formal analysis, see Section5)and a precise mathematical model of the system.
This paper does not provide an introduction nor explanation of the protocol,because the volume contains a common introduction with this material[MRS02].In Section2Maude and its object-oriented speci?cations are presented.In Section3we present a simple description of the protocol(without time aspects)that clari?es the ideas used in this kind of speci?cations.Section4shows how time aspects can be added to a rewrite theory and specially to an object-oriented speci?cation,and presents two more descriptions of the protocol handling with all its time aspects.In Section5it is shown how the re?ective features of rewriting logic and Maude can be used to perform a model-checking analysis of all possible behaviors of the protocol starting with the initial con?guration of any concrete network.In Section6we present a detailed proof by induction showing that the desirable properties of the protocol are always ful?lled by any network,provided that it is connected and acyclic.Finally,in Section7we present an evaluation of our approach as suggested in [MRS02]and we draw some conclusions in Section8.
2.Object-oriented speci?cation in Maude
Maude is a high level,general purpose language and high performance system(93–319K AC rewrites per second on a highend Linux PC)based on rewriting logic[Mes92],a logic of change in which deduction directly corresponds to the change.In rewriting logic the state of a system is formally speci?ed as an algebraic data type(by means of an equational speci?cation).In this kind of speci?cations we can de?ne new types(by means of keyword sort(s));subtype relations between types(subsort);operators(op(s))for building values of these types,giving the types of their arguments and result,and which may have attributes as being associative(assoc)or commutative(comm),for example;and equations(eq)that identify terms built with these operators.This data types are speci?ed in functional modules(with syntax fmod...endfm) whose equations are supposed to be con?uent and terminating.
The dynamic behavior of such a distributed system is then speci?ed by rewrite rules of the form t?→t , that describe the local,concurrent transitions of the system.That is,when a part of a system matches the pattern t this part can be transformed into the corresponding pattern t .Labelled rewrite rules(rl[label]) are included in system modules(with syntax mod...endm).
Regarding object-oriented speci?cations,an object is represented as a term
The Tree Identify Protocol of IEEE 1394in Rewriting Logic 3
In a concurrent object-oriented system the concurrent state,which is called a con?guration ,has the structure of a multiset made up of objects and messages that evolves by concurrent rewriting (modulo the multiset structural axioms of associativity,commutativity,and identity)using rules that describe the e?ects of communication events between some objects and messages.The rewrite rules in the module specify in a declarative way the behavior associated with the messages.The general form of such rules is
M 1...M n O 1:F 1|atts 1 ... O m :F m |atts m
?→ O i 1:F
i 1|atts i 1 ... O i k :F i k |atts i k Q 1:D 1|atts 1 ... Q p :D p |atts p M 1...M q if C
where k,p,q ≥0,the M s are message expressions,i 1,...,i k are di?erent numbers among the original 1,...,m ,and C is a rule condition.The result of applying a rewrite rule is that the messages M 1,...,M n disappear;the state and possibly the class of the objects O i 1,...,O i k may change;all the other objects O j vanish;new objects Q 1,...,Q p are created;and new messages M 1,...,M q are sent.Since the above rule involves several objects and messages in its lefthand side,we say that it is a synchronous rule .It is conceptually important to distinguish the special case of rules involving at most one object and one message in their lefthand side.These rules are called asynchronous and have the form
(M ) O :F |atts ?→( O :F |atts ) Q 1:D 1|atts 1 ... Q p :D p |atts p M 1...M q if C
By convention,the only object attributes made explicit in a rule are those relevant for that rule.In particular,the attributes mentioned only in the lefthand side of the rule are preserved unchanged,the original values of attributes mentioned only in the righthand side of the rule do not matter,and all attributes not explicitly mentioned are left unchanged.Object-oriented modules are introduced by means of keywords omod...endom .
3.First description of the protocol (with synchronous communication)
We begin with a simple description of the protocol,without time considerations,where communication between nodes is assumed to be synchronous,i.e.,a message is sent and received simultaneously;therefore,there is no need for acknowledgements,and contention cannot arise.In the IEEE 1394standard we have nodes and communications between nodes,that relate naturally to objects and messages.Nodes are represented by objects of class Node with the following attributes:
?neig :SetIden ,the set of identi?ers of the neighbor nodes with whom this node has not yet communi-cated.This is initialized to the set of all nodes (object identi?ers)connected to this node and decreases with every “be my parent”request until it is either empty (and this node is the root)or it has one element (which is the parent of this node);and
?done :Bool ,a ?ag which is set when the tree identify phase of the protocol has ?nished for this node,because it has been elected as the root node or because it already knows which node is its parent.
Since communication is synchronous in this description,we do not need messages to represent the “be my parent”requests or the acknowledgements.However,we add a “leader”message which is sent by the elected leader to indicate that a leader has been chosen.This provides us with a means of checking the requirement that a single leader is eventually elected (see Section 5).The following module introduces identi?ers (a supersort of the prede?ned quoted identi?ers)and multisets of identi?ers.An identi?er is a singleton set and bigger multisets are built by juxtaposition.This union operator is de?ned as being associative,commutative,and with the empty set as identity element.Pattern matching will be performed modulo these attributes in such a way that a pattern like J NEs (see below)represents any multiset with an element J and rest NEs .
(fmod IDENTIFIERS is protecting QID .
sorts Iden SetIden .subsorts Qid op empty :->SetIden . op __:SetIden SetIden ->SetIden [assoc comm id:empty]. endfm) The object-oriented module describing the protocol starts declaring the node identi?ers as valid object identi?ers,the class Node with its attributes,and the message leader : 4 A.Verdejo,I.Pita,and N.Mart′?-Oliet (omod FIREWIRE-SYNC is protecting IDENTIFIERS. subsort Iden class Node|neig:SetIden,done:Bool. msg leader_:Iden->Msg. Now we have to describe the node’s behavior by means of rewrite rules.The?rst rule describes how a node J,which has only one identi?er I in its attribute neig,sends a“be my parent”request to the node I, and how node I receives the request and removes J from its set of communications still to make;node J also ?nishes the identify phase by setting the attribute done. vars I J:Iden.var NEs:SetIden. rl[rec]: => Note that nondeterminism arises when there are two connected nodes with only one identi?er in their attribute neig.Any one of them can act as the sender. The other rule states when a node is elected as the leader. rl[leader]: endom) 4.Timed,asynchronous communication description The previous description is very simple,but is not an accurate depiction of events in the real protocol,where messages are sent along wires of variable length,and therefore message passing is asynchronous and subject to delay.Since the communication is asynchronous,acknowledgement messages are needed,and a particular problem arises when two nodes might simultaneously request each other to be its parent,leading to root contention[MRS02].Using only the asynchronous explicit communication via messages of Maude leads us to a description of the protocol which does not work as expected,in the sense that there is the possibility that the root contention phase and the receive“be my parent”requests phase alternate forever.Hence the timing aspects of the protocol cannot be ignored,and in the root contention phase nodes have to wait a short or long(randomly chosen)time period before resending the“be my parent”requests.Other time aspects like the detection of cycles and the force root parameter are handled in our third description(Section4.3). We have to say that we do not represent some of the concrete details of the protocol as described in [IEE95],giving more abstract descriptions.In particular,we represent communication between nodes by means of(discrete)messages,instead of the continuous assertion and deassertion of signals on wires used in the standard.The reason is the level of abstraction we want to keep,and not the incapability of our approach to formalize these aspects.We could have used objects to represent wires with attributes having the current signal values.Then,the nodes could detect the wire state by examining the corresponding attribute. Before showing this new,timed description,we brie?y summarize the ideas in[¨Olv00,¨OM02]about how to introduce time in rewriting logic and Maude,and particularly in an object-oriented speci?cation.We think that this introduction of time aspects in a speci?cation is quite natural and modular. 4.1.Time in rewriting logic and Maude A real-time rewrite theory is a rewrite theory with a sort Time that represents the time values,and which ful?lls several properties,like being a commutative monoid(Time,+,0)with additional operations≤,<,and ?.(“monus”).We use the module TIMEDOMAIN to represent the time values,with a sort Time whose values are the natural numbers,and which is a subsort of the sort TimeInf,which in addition contains the constant INF representing∞(see[¨Olv00]). Rules are divided into tick rules,that model the elapse of time on a system,and instantaneous rules, that model changes in(part of)the system and are assumed to take zero time.To ensure that time ad-vances uniformly in all the parts of a state,we need a new sort ClockedSystem,with a free constructor {_|_}:State Time->ClockedSystem.In the term{s|t},s denotes the global state and t denotes the total time elapsed in a computation if in the initial state the clock had value0.Uniform time elapse is then ensured if every tick rule is of the form{s|t}?→{s |t+τ},whereτdenotes the duration of the rule. The Tree Identify Protocol of IEEE1394in Rewriting Logic5 These ideas can also be applied to object-oriented systems[¨OM02].In this case,the global state will be a term of sort Configuration,and since it has a rich structure,it is both natural and necessary to have an explicit operationδdenoting the e?ect of time elapse on the whole state.In this way,the operationδwill be de?ned for each possible element in a con?guration of objects and messages,describing the e?ect of time on this particular element,and there will be equations which distribute the e?ect of time to the whole system. In this case,tick rules should be of the form{s|t}?→{δ(s,τ)|t+τ}. An operation mte giving the maximum time elapse permissible to ensure timeliness of time-critical actions, and de?ned separately for each object and message,is also useful,as we will see below.The general module TIMEDOOSYSTEM declares these operations,and how they distribute over the elements(see Appendix A). 4.2.Second description of the protocol In this second description each node passes through di?erent phases.When a node is in the rec phase,it is receiving“be my parent”requests from its neighbors.In the ack phase,the node sends acknowledgements “you are my child”to all the nodes which sent“be my parent”in the previous phase.In the waitParent phase,the node waits for the acknowledgement from its parent.In the contention phase,the node waits a long or short time before resending the“be my parent”request.A node is in the self phase when either it has been elected as the leader,or it has received the acknowledgement from its parent. The attributes of the class Node,de?ned in a module extending TIMEDOOSYSTEM,are now the following: class Node|neig:SetIden,children:SetIden,phase:Phase,rootConDelay:DefTime. The children attribute represents the set of children to be acknowledged;phase represents the phase in which the node is;and rootConDelay is an alarm used in the root contention phase.The sort DefTime extends Time with a new constant noTimeValue used when the clock is disabled. In addition to the leader message,we introduce two new messages which have as arguments the sender, the receiver,and the time needed to reach the receiver: msg from_to_be‘my‘parent‘with‘delay_:Iden Iden Time->Msg. msg from_to_acknowledgement‘with‘delay_:Iden Iden Time->Msg. For example,the message from I to J be my parent with delay T denotes that a“be my parent”request has been sent from node I to node J,and it will reach J in T units of time.A message with delay0 is urgent,in the sense that it has to be attended by the receiver before time elapses.The mte operation will ensure that this requirement is ful?lled,as we will see below. The?rst rule1states that a node I in the rec phase,and with more than one neighbor,can receive a“be my parent”request with delay0from its neighbor J.The identi?er J is stored in the children attribute: crl[rec]:(from J to I be my parent with delay0) => When a node is in the rec phase and there is only one connection unused,either it may move to the next phase,ack,or it can receive the last request before going into this phase: rl[recN-1]: => rl[recLeader]:(from J to I be my parent with delay0) => In the acknowledgement phase the node sends acknowledgements“you are my child”to all the nodes which previously sent“be my parent”requests: rl[ack]: => 6 A.Verdejo,I.Pita,and N.Mart′?-Oliet The operation timeLink:Iden Iden->Time represents a table with the time values denoting the delays between nodes. When all acknowledgements have been sent,either the node has the set neig empty and therefore is the root node,or it sends a“be my parent”request on the so far unused connection and awaits an acknowledgement from the parent.Note that leaf nodes skip the initial receive requests phase and move straight to this point. rl[ackLeader]: => rl[wait1]: => (from I to J be my parent with delay timeLink(I,J)). rl[ackParent]:(from J to I acknowledgement with delay0) Having modeled the communication by means of messages,and considering a fault-free medium,the con?rmation from the acknowledged children is not necessary.This disagrees with the IEEE1394standard, where the parent waits for con?rmations from all its children before sending its own“be my parent”request. If a parent request has been sent,then the node waits for an acknowledgement.If a parent request arrives instead,then the node and the originating node of the parent request are in contention for leader. In the IEEE1394standard,contention is resolved by choosing a random Boolean b and waiting for a short or long time depending on b before sampling the relevant port to check for a“be my parent”request from the other node.If the request is there then this node should agree to be the root and send an acknowledgement to the other;if the message is not present,then this node will resend its own“be my parent”request. In our representation,a random Boolean is chosen(by means of the value N in the random number generator RAN)and a wait time selected.If a“be my parent”request arrives during that time then the wait aborts and the request is dealt with;if the wait time expires then the node resends“be my parent.”Objects of class RandomNGen are pseudorandom number generators. rl[wait2]:(from J to I be my parent with delay0) => rootConDelay:if(N%2==0)then ROOT-CONT-FAST else ROOT-CONT-SLOW fi> rl[contenReceive]:(from J to I be my parent with delay0) rl[contenSend]: => (from I to J be my parent with delay timeLink(I,J)). The correctness of this random selection is addressed in[SV99]where it is proved that the root contention resolution algorithm is guaranteed to terminate successfully eventually(with probability one).This result is extended in[FS02]where a relationship between the number of attempts to resolve contention and the probability of a successful outcome is derived. We have to de?ne how time a?ects objects and messages,that is,we have to de?ne the delta operation denoting the e?ect of time elapse on objects and messages,and also which is the maximum time elapse mte allowed(to ensure timeliness of time-critical actions)by an object or message.In Appendix A the complete de?nition of these operations for the third description of the protocol(see Section4.3)is given.See[VPMO01] for the full details of this description. The tick rule that lets time pass if there is no rule that can be applied immediately is as follows: crl[tick]:{C|T}=>{delta(C,mte(C))|T plus mte(C)}if mte(C)=/=INF and mte(C)=/=0. Due to our de?nition of the operation mte,this rule can only be applied when no other rules are enabled. We could have modeled the nondeterministic elapsing of time by means of a tick rule like this one: rl[tick’]:{C|T}=>{delta(C,T’)|T plus T’}. with a new variable T’in the right-hand side representing the time increment.This kind of rules with new The Tree Identify Protocol of IEEE1394in Rewriting Logic7 variables cannot be directly used by the default Maude interpreter,but they can be used at the metalevel (see Section5)by a strategy that instantiates the variable T’with di?erent time values,ensuring timeliness of time-critical actions.However,we are not interested in the intermediate states between the result state of an instantaneous rule and the next state where another time-critical action has to be performed.That is, ?→s n where s j(0≤j pass and s n is the?rst state from s0where an action has to occur,we model them by means of a unique transition s0t?→s n,with t= n i=1t i.Of course,this a?ects the set of observable states,as commented in Section5.1. We consider only networks with more than one node,where every node has the possibility to ask another node to be its parent.If networks with only one node were considered,we should add a rule that declares the only node as the leader. 4.3.Third description of the protocol There are two timing considerations that we have not dealt with in the second description.The?rst one is whether or not the CONFIG-TIMEOUT has been exceeded.This indicates that the network has been set up incorrectly(i.e.,it includes a loop)and an error has to be reported.The second timing consideration concerns the force root parameter,fr.Normally it is possible for a node to move to the ack phase when n?1 communications have been made(where n is the number of neighbors of the node).Setting fr forces the node to wait a bit longer,in the hope that all n communications will be made(and the node becomes then the leader).These two considerations a?ect only the?rst phase of the protocol,the receive“be my parent”requests phase. The class Node is modi?ed by adding three new attributes: class Node|neig:SetIden,children:SetIden,phase:Phase,rootConDelay:DefTime, CONFIG-TIMEOUTalarm:DefTime,fr:Bool,FORCE-ROOTalarm:DefTime. The attribute CONFIG-TIMEOUTalarm is an alarm initialized with the time constant CONFIG-TIMEOUT, and it is decreased when time elapses.If it reaches the value0,the node realizes that the network has a loop; an error is reported via the message error;and the node’s attribute phase is set to the new Phase value error. The fr Boolean attribute is set to true when the node is intended to be the leader.In this case,the FORCE-ROOTalarm attribute is initialized to the time constant FRTIME,which determines how long a node delays going into the next phase although it has already received“be my parent”requests from all but one of its neighbors.This alarm is also decreased when time elapses,and when it reaches the value0,it is turned o?,setting its value to noTimeValue and the fr attribute to false.If the fr attribute is initially false,the FORCE-ROOTalarm is initialized to noTimeValue. Let us now see how the rewrite rules are modi?ed.The rec rule is not modi?ed because it is not a?ected by the new considerations.Two rules are added,controlling when the alarms notify that the value0has been reached,and showing what has to be done in each case: rl[error]: => rl[stopAlarm]: => The recN-1rule is modi?ed because now a node in the rec phase moves to the next phase only if its fr attribute has the value false.In this case the CONFIG-TIMEOUT alarm is turned o?: rl[recN-1]: => Both alarms are also turned o?if the last“be my parent”request is received while the node is in the rec phase: rl[recLeader]:(from J to I be my parent with delay0) => FORCE-ROOTalarm:noTimeValue,CONFIG-TIMEOUTalarm:noTimeValue>. 8 A.Verdejo,I.Pita,and N.Mart′?-Oliet (omod EXAMPLE is protecting FIREWIRE-ASYNC. op network7:->Configuration. op dftATTRS:->AttributeSet. eq dftATTRS=children:empty,phase:rec, rootConDelay:noTimeValue. eq network7=<’a:Node|neig:’c,dftATTRS> <’b:Node|neig:’c’d,dftATTRS> <’c:Node|neig:’a’b’e,dftATTRS> <’d:Node|neig:’b,dftATTRS> <’e:Node|neig:’c’f’g,dftATTRS> <’f:Node|neig:’e,dftATTRS> <’g:Node|neig:’e,dftATTRS> <’Random:RandomNGen|seed:13>. eq timeLink(’a,’c)=7.eq timeLink(’b,’c)=7. eq timeLink(’b,’d)=10.eq timeLink(’c,’e)=20. eq timeLink(’e,’f)=8.eq timeLink(’e,’g)=10. var I J:Qid.ceq timeLink(J,I)=timeLink(I,J)if I b e g f c d a 7 10 20 10 8 7 Fig.1.Maude description of a network with seven nodes The rest of the rules,describing the next phases,are kept unmodi?ed,which shows the modularity obtained by having the di?erent protocol phases handled by di?erent rewrite rules.However,the operations delta and mte are rede?ned because they have to deal with objects with more time-dependent attributes (see Appendix A). 4.4.Executing the speci?cation with an example in Maude The descriptions of the protocol are directly executable on the Maude system.We can take advantage of this fact in order to get con?dence on the correctness of the protocol.First,we de?ne a con?guration denoting the initial state of the network we want to check,using the timed description.We want to point out that the protocol descriptions are completely general,and the rewrite rules describing them can be applied to any network.In order to illustrate the execution of the protocol,we need to start with a concrete network (de?ned in an extension of the module with the protocol description),and we have chosen the network shown in Figure1. We can ask the Maude system to rewrite the initial con?guration by using its default strategy: Maude>(rew{network7|0}.) result ClockedSystem:{leader’c <’e:Node|neig:’c,restATTRS><’d:Node|neig:’b,restATTRS><’a:Node|neig:’c,restATTRS> <’f:Node|neig:’e,restATTRS><’b:Node|neig:’c,restATTRS><’g:Node|neig:’e,restATTRS> <’c:Node|neig:empty,restATTRS><’Random:RandomNGen|seed:9655>|920} where,in order to make the term presentation more readable,we have substituted by hand the attributes which are the same for all nodes,as follows: restATTRS=children:empty,phase:self,rootConDelay:noTimeValue 5.Model-checking analysis There are two desirable properties that this protocol has to ful?ll:A single leader is chosen(safety),and a leader is eventually chosen(liveness).The execution provided by the default interpreter is not enough to ensure that these properties are always ful?lled.We may go further in our analysis by means of an exhaustive exploration of all possible behaviors of the protocol.We show in this section how the re?ective capabilities of rewriting logic and Maude[Cla00,CM02,CDE+02]can be used to show that the speci?cations of the protocols work in the expected way when applied to an arbitrary concrete network.This is done by checking that these two properties are ful?lled at the end of the protocol in all possible behaviors of the protocol starting with the initial con?guration representing the concrete network. Rewriting logic is re?ective[Cla00,CM02],that is,there is a?nitely presented rewrite theory U that is The Tree Identify Protocol of IEEE1394in Rewriting Logic9 universal in the sense that we can represent any?nitely presented rewrite theory R(including U itself)and any terms t,t in R as terms t, R,R, 10 A.Verdejo,I.Pita,and N.Mart ′?-Oliet c b a e f g 7 77 740Fig.2.A symmetric network it can be seen how the metarepresentation of module EXAMPLE is obtained and used to instantiate the generic module SEARCH .Next,we can test this example.The Maude result is as follows: Maude> (down EXAMPLE :red allSol(up(EXAMPLE,{network7|0})).)result ClockedSystem :{leader ’c <’e : Node |neig :’c,restATTRS ><’d :Node |neig :’b,restATTRS ><’a : Node |neig :’c,restATTRS ><’f :Node |neig :’e,restATTRS ><’b : Node |neig :’c,restATTRS ><’g :Node |neig :’e,restATTRS ><’c :Node |neig :empty,restATTRS ><’Random :RandomNGen |seed :9655>|920} We observe that only one leader has been elected in the only irreducible,reachable con?guration.It is not surprising that only one con?guration is reachable although all possible behaviors are checked,because the protocol is not so nondeterministic when time is added.Time constraints put severe restrictions on the allowed behaviors.However,the search strategy can be applied starting with a network where several di?erent irreducible states can be reachek.For example,from the network shown in Figure 2(de?ned in a module EXAMPLE2similar to the module EXAMPLE above)several con?gurations can be reached,but all of them have only one leader chosen,as expected. Maude>(down EXAMPLE2:red allSol(up(EXAMPLE2,{network6|0})).) result ClockedSystem :{leader ’c <’e :Node |neig :’c,restATTRS ><’a :Node |neig :’c,restATTRS ><’b :Node |neig :’c,restATTRS ><’f :Node |neig :’e,restATTRS ><’g :Node |neig :’e,restATTRS ><’c :Node |neig :empty,restATTRS ><’Random :RandomNGen |seed : 9655>|997}&{leader ’e <’a :Node |neig :’c,restATTRS ><’c :Node |neig :’e,restATTRS ><’b :Node |neig :’c,restATTRS ><’f :Node |neig :’e,restATTRS ><’g :Node |neig :’e,restATTRS ><’e :Node |neig :empty,restATTRS ><’Random :RandomNGen |seed :9655>|997} The presence of only one leader message does not exclude (on its own)the possibility of a sequence of leaders being declared and undeclared.But a simple examination of the rewrite rules shows that no leader message appears in the left-hand side of rewrite rules and there is no operation that removes this kind of messages.Thus,once a leader message appears in a con?guration,it never disappears.The model checking strategy has to be executed on a concrete network.So we should run it with many di?erent networks to be sure that the protocol works in all possible cases.That is the reason why we propose a third kind of analysis in the following section,where the necessity of starting with a concrete network is not present. 6.Detailed proof by induction The desirable properties for this protocol are that a single leader is chosen,and that this leader is eventually chosen,as stated in Section 5.To prove them,we de?ne observations that allow us to state properties of a con?guration of the system.Then we observe the changes made by the rewrite rules in the con?gurations until the leader is chosen.Currently we are working on a speci?cation logic and tools to automatically generate these proofs [FMMO +00]. 6.1.Veri?cation of synchronous description For the synchronous case,we de?ne the following observation: ?nodes is a set of pairs A ;S where A is a network node identi?er and S is the set of nodes such that The Tree Identify Protocol of IEEE1394in Rewriting Logic11 B∈S i?both If we take the second component of each pair A;S to be the adjacency list of the node represented in the?rst component,then nodes represents the network(directed graph)with the nodes in the initial con?guration for which the protocol has not?nished yet. We assume that the network is initially correct,in the sense that the set nodes represents a symmetric (that is,the links are bidirectional),connected,and acyclic network.We have checked that if these conditions are ful?lled initially,then they are always ful?lled. The desirable properties of the protocol are derived by induction from the following: 1.If there are at least two pairs in nodes then the rule rec can be applied.We know that if|nodes|≥2, then there exist A and B such that 2.The cardinality of nodes always decreases in one unit when a rule is applied.The proof is straightforward from the rules that model the system. 3.Since nodes is symmetric,if there is only one pair 4.Since nodes is connected and symmetric,there may be at most one element in nodes such that its set of neighbors is empty. 6.2.Veri?cation of second description The method above is extended in order to prove the correctness of the timed descriptions.Remember that in this description we are not considering cycles or networks with only one node.The main idea is to have di?erent observations for the sets of nodes in each phase and look for sets of nodes that represent symmetric, connected,and acyclic networks.We will prove that if the sets are not empty then some actions can take place,and the number of elements in the sets decreases until all sets are empty.Given a con?guration of objects and messages,we consider the following observations de?ned by sets of pairs: Rec N: Ack C: where C is the number of node identi?ers in the node’s attribute children. Ack0: and there is no message from B to A acknowledgement with delay T in the system. Contention T: All the sets are pairwise disjoint,since a node cannot be in two phases at the same time. https://www.doczj.com/doc/9518369716.html,work properties Now,the set Nodes is de?ned by Nodes= N Rec N∪ C Ack C∪ T Contention T∪Wait. There are not two pairs in Nodes with the same?rst component;then,if we take the second component of each pair to be the adjacency list of the node represented in the?rst component,Nodes represents a network(directed graph),and initially Nodes= N Rec N,because all the other subsets are empty.Notice that the set containing only the pair If N Rec N represents,at the beginning,a symmetric,connected and acyclic network,then Nodes repre-sents always a symmetric,connected and acyclic network.We have checked that this is true by(structural) induction on our rewrite rules(see[VPMO01]). 12 A.Verdejo,I.Pita,and N.Mart′?-Oliet 6.2.2.Safety properties Informally speaking,we prove that a single leader is chosen by proving that if a rewrite rule is applied in the system,at most one node is removed from the network represented by the set Nodes.Then if the algorithm ?nishes,that is,if the set Nodes becomes empty,at the end the network represented by Nodes will have only one node that will be represented by a pair of the form If the set Nodes becomes empty,there should be a leader.Two rules remove pairs from Nodes:?ack.If we observe the state reached when we apply this rule,we have removed a node identi?er B from the second component of a pair ?ackLeader.If we observe the state reached when we apply this rule,we have removed a pair of the form There is only one leader.Since the network represented by Nodes is always connected,there can only be a pair of the form 6.2.3.Liveness properties Informally speaking,we prove that if there are pairs in Nodes then we can apply some rewrite rule in the system,and if we apply a rule,some positive number that depends on the pairs in Nodes decreases,and becomes zero when there are no more pairs in Nodes.Then Nodes should become empty,which means that the algorithm has?nished.The contention phase presents some problems,since the function does not decrease sometimes when the rules that treat the contention are applied.In this part we prove termination using the assumption that we are in a fair system and contention cannot occur forever. Property1:If there are pairs in Nodes,then there is at least one rule that can be applied in the system.Since the network represented by the pairs in Nodes is acyclic,then either the network has only one node,or the network has at least one leaf,that is,there is a pair of the form Property2:A node can only come into the contention phase a?nite number of times.We have proved(see[VPMO01]for the full details)that in a fair system,and assuming that ROOT-CONT-FAST max{I,J}(timeLink(I,J))(1) ROOT-CONT-SLOW max{I,J}(timeLink(I,J))(2) ROOT-CONT-SLOW?ROOT-CONT-FAST max{I,J}(timeLink(I,J))(3) a node cannot be forever changing between the contention and waitParent phases by applying rules wait2 and contenSend;equivalently,the rewrite rule contenReceive will be applied. We mean by fairness that all the rewrite rules that can be applied will be applied,and that the random number generator produces even and odd numbers and therefore the rootConDelay attribute of a node in the contention phase can be either ROOT-CONT-FAST or ROOT-CONT-SLOW.Equations1,2,and3express that both constants are much greater than the maximum link delay between the nodes,and that their di?erence is also much greater[IEE95]. If a node goes out of the contention phase by means of the contenReceive rule,it will not go back to the contention phase since it will be in the ack phase with no neighbors.Then,the only rules that can be applied to it are?rst ack,and then ackLeader. Property3:Application of rules decreases f(Con?guration).Let N be the total number of nodes in the network and T the maximum delay of the timeLink table.We de?ne: The Tree Identify Protocol of IEEE1394in Rewriting Logic13 rec(I)= 5?N?T?n if 0otherwise ack(I)= 4?T?(n+1)if wait(I)= 1if 0otherwise nm(C)=number of messages with time in C times(C)=sum of times in messages in C Consider the function f(C)= I∈Node rec(I)+ack(I)+wait(I) +nm(C)+times(C). For each rewrite rule di?erent from contenReceive and contenSend we have checked that the value of the function decreases after applying the rule(see[VPMO01]). Rules contenReceive and contenSend do not decrease the value of the function,but on the contrary, they increase it.This does not matter since we have proved that these rules cannot be applied forever for a pair of nodes,and that if two nodes solve their contention they will not have another contention. Since f(C)≥0and it decreases when we apply the rewrite rules,then,although it can be increased by a?nite quantity,we conclude that we cannot apply rewrite rules forever in the system. 6.2.4.Total correctness Since we cannot apply rules forever in the system(Property3),the set Nodes should become empty(Prop-erty1),and if this set becomes empty there should be one and only one leader(Section6.2.2). 6.3.Veri?cation of third description First we will prove that by using this description of the protocol cycles are detected.Then we will show how the new rules a?ect the proof of correctness given for the timed asynchronous description with no cycle detection in Section6.2. 6.3.1.If there is a cycle in the network,an error message is generated. Property1:If a node is in a cycle,then it does not change from the rec phase until an error message is generated.If the node is in a cycle it has at least two neighbors.The rules that change a node from the rec phase are recN-1and recLeader,which cannot be applied since the node has more than one neighbor,and error,which generates the error message. Property2:If the network has a cycle,then the CONFIG-TIMEOUTalarm attribute of some node that is in the cycle is set to0.We divide the set of nodes in two subsets:one with the nodes that are in a cycle,and the other with the nodes that are not in a cycle.If a node is not in a cycle,there are a?nite number of rewrites that can take place before it reaches the self phase.If a node is in a cycle,rule rec can be applied at most as many times as the number of nodes in the network that are connected to this node but are not in the cycle.Once there is no rewrite rule di?erent from tick that can be applied to the nodes, only time can pass changing the CONFIG-TIMEOUTalarm attribute.This attribute will decrease in the nodes of the cycle until some of them become0. Property3:If the CONFIG-TIMEOUTalarm attribute of a node is set to0and the node does not change from the rec phase,the value of the CONFIG-TIMEOUTalarm attribute does not change any more.The rules that change the value of the CONFIG-TIMEOUTalarm attribute are: ?recN-1and recLeader,that change the phase of the node to the ack phase. ?tick,that decreases the value of the attribute.But this rule cannot be applied if CONFIG-TIMEOUTalarm is0,since in this case the mte operation is evaluated to0. ?error,that changes the phase of the node to the error phase. Property4:If there is a cycle in the network then an error is generated.By Properties2and 3,there is a node whose CONFIG-TIMEOUTalarm attribute is set to0,and this value cannot change,and by Property1,the node should be in the rec phase.Looking at the lefthand side of the error rewrite rule we check that it can be applied,and since we assume that we are in a fair system the error message will be generated. 14 A.Verdejo,I.Pita,and N.Mart′?-Oliet 6.3.2.Total correctness We prove that,if there is no error,a single leader is chosen and that the leader is eventually chosen.We can extend the method used in the previous proofs in order to deal with the new rules and the rules that have changed.We consider the same observations as in the case with no cycle detection,since although we have introduced a new phase,error,this is a?nal phase in the sense that once a node is in that phase there is no rewrite rule in the system that can be applied to it. Since we suppose that there is no error,we also have that the network represented by the set Nodes is symmetric,connected,and acyclic. The proof of the safety properties does not change,since we suppose that there is no error,and then we do not introduce any rewrite rule that removes pairs from the set Nodes. The proof of the liveness properties is slightly changed.First,Property1of Section6.2.3needs to take into account the new de?nition of the recN-1rewrite rule,in particular the value of the fr and FORCE-ROOTalarm attributes(see[VPMO01]).The proof of Property2does not change,since the new rules do not a?ect the contention phase.For Property3,we change the function de?nition of nm(C)and times(C)to take into account also objects with time values,and we check that the new rules decrease the function’s value. Since the three properties are veri?ed,the liveness property is ful?lled and therefore we have total correctness,as before. 7.Evaluation We have speci?ed all the parts of this protocol in a formal way,by using rewriting logic as implemented in the Maude system.We consider that the timed object-oriented approach followed is particularly expressive for this kind of protocols.We have also analysed the whole protocol in two di?erent ways.One is fully automated and consists in the exhaustive exploration of all the states reachable from the initial state of a concrete network(arbitrarily choosen).The other one is manual and provides a mathematical proof of the safety and liveness requirements for any network. We think that our solution is easy to change or extend.Indeed,we have presented three speci?cations at di?erent levels of abstraction.However,the formal proofs are quite sensible to changes,although they are also modular,which lets us reuse and extend the second proof when we are verifying the third description. The speci?cations were produced in two weeks by someone with great experience in the use of Maude, but with less knowledge on the introduction of time in rewriting logic,which was learnt during this period. The formal proofs were developed in three more weeks. All the concepts involved in this speci?cation framework are easy to understand by an average engineer, so we think that the understanding of our solution would be quickly undertaken by someone with little knowledge of rewriting and algebraic speci?cations. 8.Conclusion We have shown how rewriting logic and Maude can be used to specify and analyze at di?erent abstract levels a communication protocol such as the FireWire tree identify protocol.We have also shown how the timing aspects of the protocol can be modeled in an easy and structured way in rewriting logic,by means of operations that de?ne the e?ect of time elapse and rewrite rules that let time pass. We see this work as another contribution to the research area of speci?cation and analysis of several kinds of communication protocols in Maude,as described in[DMT98,DMT00],as well as to the development of the formal methodology that we have summarized in the introduction.As far as we know,this paper describes the?rst examples where the strongest method of formal proof has been applied to a protocol in the context of Maude programs.In our opinion,it is necessary to have more examples in order to consolidate this methodology,and to develop tools that can help in the simulation and analysis of such examples. Acknowledgements.We thank Carron Shankland for discussions about the tree identify protocol and its time aspects,and Peter¨Olveczky for suggestions about how to introduce time in our speci?cations.We would also like to thank the anonymous referees and editors for their remarks,which have improved very much the presentation. The Tree Identify Protocol of IEEE1394in Rewriting Logic15 References [BMM98]R.Bruni,J.Meseguer,and U.Montanari.Internal strategies in a rewriting implementation of tile systems.In C.Kirchner and H.Kirchner,editors,Proceedings Second International Workshop on Rewriting Logic and its Applications,WRLA’98,ENTCS15.Elsevier,1998.http://www.elsevier.nl/locate/entcs/volume15.html. [CDE+00a]M.Clavel,F.Dur′a n,S.Eker,P.Lincoln,N.Mart′?-Oliet,J.Meseguer,and https://www.doczj.com/doc/9518369716.html,ing Maude.In T.Maibaum,editor,Proc.Third Int.Conf.Fundamental Approaches to Software Engineering,FASE2000,Berlin, Germany,March/April2000,LNCS1783,pages371–374.Springer-Verlag,2000. [CDE+00b]M.Clavel,F.Dur′a n,S.Eker,P.Lincoln,N.Mart′?-Oliet,J.Meseguer,and J.Quesada.A Maude Tutorial. Computer Science Laboratory,SRI International,March2000.https://www.doczj.com/doc/9518369716.html,. [CDE+00c]M.Clavel,F.Dur′a n,S.Eker,P.Lincoln,N.Mart′?-Oliet,J.Meseguer,and J.Quesada.Towards Maude2.0.In K.Futatsugi,editor,Proceedings Third International Workshop on Rewriting Logic and its Applications,WRLA 2000,ENTCS36,pages297–318.Elsevier,2000.http://www.elsevier.nl/locate/entcs/volume36.html. [CDE+02]M.Clavel,F.Dur′a n,S.Eker,P.Lincoln,N.Mart′?-Oliet,J.Meseguer,and J.Quesada.Maude:speci?cation and programming in rewriting logic.Theoretical Computer Science,285(2):187–243,2002. [Cla00]M.Clavel.Re?ection in Rewriting Logic:Metalogical Foundations and Metaprogramming Applications.CSLI Publications,2000. [CM02]M.Clavel and J.Meseguer.Re?ection in conditional rewriting logic.Theoretical Computer Science,285(2):245–288, 2002. [DMT98]G.Denker,J.Meseguer,and C.Talcott.Protocol speci?cation and analysis in Maude.In N.Heintze and J.Wing, editors,Proc.of Workshop on Formal Methods and Security Protocols,25June1998,Indianapolis,Indiana,1998. https://www.doczj.com/doc/9518369716.html,/who/nch/fmsp/index.html. [DMT00]G.Denker,J.Meseguer,and C.Talcott.Formal speci?cation and analysis of active networks and communication protocols:The Maude experience.In Proc.DARPA Information Survivability Conference and Exposition DICEX 2000,Vol.1,Hilton Head,South Carolina,January2000,pages251–265.IEEE,2000. [FMMO+00]J.Fiadeiro,T.Maibaum,N.Mart′?-Oliet,J.Meseguer,and I.Pita.Towards a veri?cation logic for rewriting logic.In D.Bert and C.Choppy,editors,Recent Trends in Algebraic Development Techniques,WADT’99,France, Selected Papers,LNCS1827.Springer-Verlag,2000. [FS02] C.Fidge and C.Shankland.But what if I don’t want to wait forever?In J.Cooke,S.Maharaj,J.Romijn,and C.Shankland,editors,Formal Aspects of Computing X(Y):UU–VV,2002. [IEE95]Institute of Electrical and Electronics Engineers.IEEE Standard for a High Performance Serial Bus.Std1394-1995,August1995. [Mes92]J.Meseguer.Conditional rewriting logic as a uni?ed model of concurrency.Theoretical Computer Science,96(1):73–155,1992. [Mes98]J.Meseguer.Research directions in rewriting logic.In U.Berger and H.Schwichtenberg,editors,Computational Logic,NATO Advanced Study Institute,Marktoberdorf,Germany,July29–August6,1997,NATO ASI Series F: Computer and Systems Sciences165,pages347–398.Springer-Verlag,1998. [MOM93]N.Mart′?-Oliet and J.Meseguer.Rewriting logic as a logical and semantic framework.Technical Report SRI-CSL-93-05,SRI International,Computer Science Laboratory,August1993.To appear in D.Gabbay,ed.,Handbook of Philosophical Logic,Second Edition,Volume9.Kluwer Academic Publishers,2002.https://www.doczj.com/doc/9518369716.html,/ papers. [MRS02]S.Maharaj,J.Romijn,and C.Shankland.The IEEE1394tree identify protocol:Problem speci?cation.In J.Cooke, S.Maharaj,J.Romijn,and C.Shankland,editors,Formal Aspects of Computing X(Y):AA–BB,2002. [MS00]S.Maharaj and C.Shankland.A Survey of Formal Methods Applied to Leader Election in IEEE1394.Journal of Universal Computer Science,6(11):1145–1163,November2000. [¨Olv00]P.¨Olveczky.Speci?cation and Analysis of Real-Time and Hybrid Systems in Rewriting Logic.PhD thesis,Uni-versity of Bergen,Norway,2000.https://www.doczj.com/doc/9518369716.html,/papers. [¨OM02]P.¨Olveczky and J.Meseguer.Speci?cation of real-time and hybrid systems in rewriting logic.Theoretical Computer Science,285(2):359–405,2002. [SMR01] C.Shankland,S.Maharaj,and J.Romijn.International workshop on application of formal methods to IEEE1394 standard,March2001.https://www.doczj.com/doc/9518369716.html,/firewire-workshop. [SV99]M.I.A.Stoelinga and F.W.Vaandrager.Root contention in IEEE1394.In J.-P.Katoen,editor,Proceedings5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems,LNCS1601,pages 53–74.Springer-Verlag,1999. [VPMO01] A.Verdejo,I.Pita,and N.Mart′?-Oliet.The leader election protocol of IEEE1394in Maude.Technical Report 118.01,Dpto.Sistemas Inform′a ticos y Programaci′o n,Universidad Complutense de Madrid,2001. https://www.doczj.com/doc/9518369716.html,plete Maude code(for third description) (omod TIMEDOOSYSTEM is protecting TIMEDOMAIN.protecting QID. sorts State ClockedSystem. subsort Configuration op‘{_|_‘}:State Time->ClockedSystem. op delta:Configuration Time->Configuration. vars CF CF’:Configuration.var T:Time. 16 A.Verdejo,I.Pita,and N.Mart′?-Oliet eq delta(none,T)=none. ceq delta(CF CF’,T)=delta(CF,T)delta(CF’,T)if CF=/=none and CF’=/=none. op mte:Configuration->TimeInf. eq mte(none)=INF. ceq mte(CF CF’)=min(mte(CF),mte(CF’))if CF=/=none and CF’=/=none. endom) (fmod IDENTIFIERS is protecting QID. sorts Iden SetIden.subsorts Qid op empty:->SetIden. op__:SetIden SetIden->SetIden[assoc comm id:empty]. endfm) (fmod TIMEDPHASES is sort Phase. ops rec ack waitParent contention self error:->Phase. endfm) (omod RANDOM is protecting TIMEDOOSYSTEM. class RandomNGen|seed:MachineInt. op random:MachineInt->MachineInt.***random(x)generates the next random number var N:MachineInt.var T:Time.var RAN:Oid. eq random(N)=((104*N)+7921)%10609. eq delta( eq mte( endom) (omod FIREWIRE-ASYNC is protecting IDENTIFIERS.protecting TIMEDPHASES.protecting RANDOM. class Node|neig:SetIden,children:SetIden,phase:Phase,rootConDelay:DefTime, CONFIG-TIMEOUTalarm:DefTime,fr:Bool,FORCE-ROOTalarm:DefTime. msg from_to_be‘my‘parent‘with‘delay_:Iden Iden Time->Msg. msg from_to_acknowledgement‘with‘delay_:Iden Iden Time->Msg. msg leader_:Iden->Msg. msg error:->Msg. ***Time constants ops ROOT-CONTEND-FAST ROOT-CONTEND-SLOW CONFIG-TIMEOUT FRTIME:->Time. eq ROOT-CONTEND-FAST=250.eq ROOT-CONTEND-SLOW=580.eq CONFIG-TIMEOUT=166600.eq FRTIME=84000. op timeLink:Iden Iden->Time. var RAN:Oid.var PH:Phase.vars I J K:Iden.var N:Nat. vars NEs CHs:SetIden.var C:Configuration.vars T T’:Time.vars DT DT’:DefTime. crl[rec]:{(from J to I be my parent with delay0) =>{ rl[error]:{ =>{ rl[stopAlarm]:{ =>{ rl[recN-1]:{ =>{ rl[recLeader]:{(from J to I be my parent with delay0) =>{ FORCE-ROOTalarm:noTimeValue,CONFIG-TIMEOUTalarm:noTimeValue>C|T}. rl[ack]:{ =>{(from I to J acknowledgement with delay timeLink(I,J)) rl[ackLeader]:{ =>{ rl[ackParent]:{ =>{ (from I to J be my parent with delay timeLink(I,J))C|T}. rl[wait1]:{(from J to I acknowledgement with delay0) =>{ rl[wait2]:{(from J to I be my parent with delay0) The Tree Identify Protocol of IEEE1394in Rewriting Logic17 =>{ rootConDelay:if(N%2==0)then ROOT-CONTEND-FAST else ROOT-CONTEND-SLOW fi> rl[contenReceive]:{(from J to I be my parent with delay0) =>{ rootConDelay:noTimeValue>C|T}. rl[contenSend]:{ =>{ (from I to J be my parent with delay timeLink(I,J))C|T}. ***Timed behaviour eq delta( (if DT’==noTimeValue then else else(if DT’==noTimeValue then else eq delta( if DT==noTimeValue then ceq delta( if(PH==ack or PH==waitParent or PH==self or PH==error). eq delta(leader I,T)=leader I. eq delta(error,T)=error. eq delta(from I to J be my parent with delay T,T’)= from I to J be my parent with delay(T monus T’). eq delta(from I to J acknowledgement with delay T,T’)= from I to J acknowledgement with delay(T monus T’). eq mte(from I to J be my parent with delay T)=T. eq mte(from I to J acknowledgement with delay T)=T. eq mte(leader I)=INF. eq mte(error)=INF. eq mte( else(if DT’==noTimeValue then DT else min(DT,DT’)fi)fi. eq mte( eq mte( eq mte( eq mte( eq mte( eq mte( eq mte( crl[tick]:{C|T}=>{delta(C,mte(C))|T plus mte(C)}if mte(C)=/=INF and mte(C)=/=0. endom) ***Search strategy (fth AMODULE is including META-LEVEL. op MOD:->Module.op labels:->QidList. endfth) (fmod SEARCH[M::AMODULE]is sort TermSet.subsort Term vars T T’:Term.var TL:TermList.var TS:TermSet. var N:MachineInt.var L:Qid.var LS:QidList.var SB:Substitution. op~:->TermList. eq~,TL=TL.eq TL,~=TL. op extTerm:ResultPair->Term. eq extTerm({T,SB})=T. op meta-apply’:Term Qid MachineInt->Term. op allRew:Term QidList->TermList. op topRew:Term Qid MachineInt->TermList. eq meta-apply’(T,L,N)=extTerm(meta-apply(MOD,T,L,none,N)). eq allRew(T,nil)=~. eq allRew(T,L LS)=topRew(T,L,0),allRew(T,LS). eq topRew(T,L,N)=if meta-apply’(T,L,N)==error*then~ else(meta-apply’(T,L,N),topRew(T,L,N+1))fi. op‘{‘}:->TermSet. op_U_:TermSet TermSet->TermSet[assoc comm id:{}]. 18 A.Verdejo,I.Pita,and N.Mart′?-Oliet op_isIn_:Term TermSet->Bool. eq T U T=T. eq T isIn{}=false. eq T isIn(T’U TS)=if meta-reduce(MOD,’_==_[T,T’])=={’true}’Bool then true else(T isIn TS)fi. op allSol:Term->TermSet. op allSolDepth:TermList TermSet->TermSet. eq allSol(T)=allSolDepth(meta-reduce(MOD,T),{}). eq allSolDepth(~,TS)={}. eq allSolDepth(T,TS)=if T isIn TS then{} else(if allRew(T,labels)==~then T else allSolDepth(allRew(T,labels),TS U T)fi)fi. eq allSolDepth((T,TL),TS)=if T isIn TS then allSolDepth(TL,TS) else(if allRew(T,labels)==~then(T U allSolDepth(TL,TS)) else allSolDepth((allRew(T,labels),TL),TS U T)fi)fi. endfm) ***Example (omod EXAMPLE is protecting FIREWIRE-ASYNC. op network7:->Configuration. op defaultATTRS:->AttributeSet. eq defaultATTRS=children:empty,phase:rec,fr:false,FORCE-ROOTalarm:noTimeValue, CONFIG-TIMEOUTalarm:CONFIG-TIMEOUT,rootConDelay:noTimeValue. eq network7=<’a:Node|neig:’c,defaultATTRS><’b:Node|neig:’c’d,defaultATTRS> <’c:Node|neig:’a’b’e,defaultATTRS><’d:Node|neig:’b,defaultATTRS> <’e:Node|neig:’c’f’g,defaultATTRS><’f:Node|neig:’e,defaultATTRS> <’g:Node|neig:’e,defaultATTRS><’Random:RandomNGen|seed:13>. eq timeLink(’a,’c)=7.eq timeLink(’b,’c)=7.eq timeLink(’b,’d)=10. eq timeLink(’c,’e)=40.eq timeLink(’e,’f)=7.eq timeLink(’e,’g)=7. var I J:Qid.ceq timeLink(J,I)=timeLink(I,J)if I op_&_:ClockedSystem ClockedSystem->ClockedSystem[assoc comm]. var S:ClockedSystem. eq S&S=S. endom) (mod META-FIREWIRE is including META-LEVEL. op METAFW:->Module. eq METAFW=up(EXAMPLE). op labelsIDs:->QidList. eq labelsIDs=(’rec’error’stopAlarm’recN-1’recLeader’ack’ackLeader ’ackParent’wait’contenReceive’contenSend’tick). endm) (view ModuleFW from AMODULE to META-FIREWIRE is op MOD to METAFW.op labels to labelsIDs. endv) (mod SEARCH-FW is protecting SEARCH[ModuleFW]. op downSol:TermSet->Term. var T:Term.var TS:TermSet. eq downSol({})=error*. eq downSol(T)=T. ceq downSol(T U TS)=’_&_[T,downSol(TS)]if TS=/={}. endm) ***Section 4.4 (select EXAMPLE.) (rew{network7|0}.) ***Section 5.2 (select SEARCH-FW.) (down EXAMPLE:red downSol(allSol(up(EXAMPLE,{network7|0}))).) 慕课、翻转课堂、微课的介绍和特点 所谓“慕课”(MOOC)，顾名思义，“M”代表Massive(大规模)，与传统课程只有几十个或几百个学生不同，一门MOOCs课程动辄上万人，最多达16万人；第二个字母“O”代表Open(开放)，以兴趣导向，凡是想学习的，都可以进来学，不分国籍，只需一个邮箱，就可注册参与；第三个字母“O”代表Online(在线)，学习在网上完成，无需旅行，不受时空限制；第四个字母“C”代表Course，就是课程的意思。[1] MOOC是新近涌现出来的一种在线课程开发模式，它发端于过去的那种发布资源、学习管理系统以及将学习管理系统与更多的开放网络资源综合起来的旧的课程开发模式。通俗地说，慕课是大规模的网络开放课程，它是为了增强知识传播而由具有分享和协作精神的个人组织发布的、散布于互联网上的开放课程。 这一大规模在线课程掀起的风暴始于2011年秋天，被誉为“印刷术发明以来教育最大的革新”，呈现“未来教育”的曙光。2012年，被《纽约时报》称为“慕课元年”。[2]多家专门提供慕课平台的供应商纷起竞争，Coursera、edX和Udacity是其中最有影响力的“三巨头”，前两个均进入中国。 主要特点: 1)、大规模的：不是个人发布的一两门课程：“大规模网络开放课程”(MOOC)是指那些由参与者发布的课程，只有这些课程是大型的或者叫大规模的，它才是典型的的MOOC。 2)、开放课程：尊崇创用共享（CC）协议；只有当课程是开放的，它才可以成之为MOOC。 3)、网络课程：不是面对面的课程；这些课程材料散布于互联网上。人们上课地点不受局限。无论你身在何处，都可以花最少的钱享受美国大学的一流课程，只需要一台电脑和网络联接即可。 ★鞋子尺码对照表大全(标准通用)★美国码★日本码★国际码★英国码★鞋子尺码对照表 标准通用尺码对照表 男鞋尺码对照表（标准通用） 尺码39 40 41 42 43 44 45 46 47 脚长(mm) 23."6-24 24."1-245 24."6-250 25."1-255 25."6-260 26."1- 26526."6-270 27."1-275 27."6-280 美国码 6."5 7 7."5 8 8."5 9 9."5 10 10."5 24."5 25."0 25."5 26."0 26."5 27."0 27."5 28."0 28."5 国际码245 250 255 260 265 270 275 280 285 女鞋尺码对照表（标准通用） 尺码35 36 37 38 39 40 41 42 脚长（mm） 22."1-225 22."6-230 23."1-235 23."6-240 24."1-245 24."6- 25025."1-255 美国码5 5."5 6 6."5 7 7."5 8 8."5 日本码 22."5 23."0 23."5 24."0 24."5 25."0 25."5 26."0 国际码225 230 235 240 245 250 255 260 Adidas尺码对照表 Adidas男鞋尺码对照表 中国码38 2/3 39 1/3 40 40 2/3 41 1/3 42 42 2/3 43 1/3 44 44 2/3 451/3 46 美国码6 6."5 7 8."5 9 9."5 10 10."5 11 11."5 英国码 5."5 6 6."5 7 7."5 8 8."5 9 9."5 10 10."5 11 标准尺码（mm）240 245 250 255 260 265 270 275 280 285 290 295Nike尺码对照表 Nike男鞋尺码对照表 中国码 38."5 39 40 40."5 41 42 42."5 43 44 44."5 45 美国码6 6."5 7 Women's Size Conversions US Sizes Euro Sizes UK Sizes Inches CM 4 3 5 2 8.1875" 20.8 4.5 35 2.5 8.375" 21.3 5 35-3 6 3 8.5" 21.6 5.5 36 3.5 8.75" 22.2 6 36-3 7 4 8.875" 22.5 6.5 37 4.5 9.0625" 23 7 37-38 5 9.25" 23.5 7.5 38 5.5 9.375" 23.8 8 38-39 6 9.5" 24.1 8.5 39 6.5 9.6875" 24.6 9 39-40 7 9.875" 25.1 9.5 40 7.5 10" 25.4 10 40-41 8 10.1875" 25.9 10.5 41 8.5 10.3125" 26.2 11 41-42 9 10.5" 26.7 11.5 42 9.5 10.6875" 27.1 12 42-43 10 10.875" 27.6 Men's Size Conversions US Sizes Euro Sizes UK Sizes Inches CM 6 39 5.5 9.25" 23.5 6.5 39 6 9.5" 24.1 7 40 6.5 9.625" 24.4 7.5 40-41 7 9.75" 24.8 8 41 7.5 9.9375" 25.4 8.5 41-42 8 10.125" 25.7 9 42 8.5 10.25" 26 9.5 42-43 9 10.4375" 26.7 10 43 9.5 10.5625" 27 10.5 43-44 10 10.75" 27.3 11 44 10.5 10.9375" 27.9 11.5 44-45 11 11.125" 28.3 12 45 11.5 11.25" 28.6 13 46 12.5 11.5625" 29.4 14 47 13.5 11.875" 30.2 15 48 14.5 12.1875" 31 16 49 15.5 12.5" 31.8 Youth Size Conversions (6 – 10 years) 鞋 类 英 文 包装用字汇…………………………………………………………………4 (四)颜色 字汇..............................................................................4 (五)材料字汇..............................................................................5 二、鞋子构造名称(一)鞋子各部位名称及图解............................................................12 (二)鞋类各种鞋型名称及图解.........................................................22 三、制鞋工具及机械设备..............................................................29 四、制鞋过程之术语应用(一)制鞋过程暨品管检验应用术语...................................................33 (二)鞋类制作流程........................................................................38 五、鞋类一般缺点........................................................................43 六、规格表之应用........................................................................44 七、订单之应用...........................................................................46 八、简易英语会话........................................................................47 九、一般贸易常识 (51) 十、国际贸易暨交易上用语 (52) 作品简介 本微课视频的教学内容为牛津小学英语5B Unit8 At the weekends (B)部分的单词教学。本部分的教学内容和教学重点是掌握6个昆虫类单词及insects的发音。教学目标是让学生通过微视频的学习，能够正确、流利地朗读6种昆虫类的单词以及单词insects，并能够熟练运用。教学难点是让学生读准单词发音，掌握发音规律，掌握以字母y结尾的可数名词变为复数时的变化规则。情感态度方面，需要学生具有通过微视频学习知识的兴趣，能够积极、主动的参与到教学活动中来，通过微视频学习的方式，掌握语言技能；能够根据自己对知识的掌握程度和实际需要借助视频学习的优势，反复观看，解决自己的难点问题，积极参与到视频教学中的操练项目，巩固和运用知识。 作品的创作说明： 教学设计 教学内容：牛津小学英语5B Unit8 At the weekends (B) 教学目标：让学生通过微视频学习，能够正确、流利地朗读6种昆虫类的单词以及单词insects，并能够熟练运用。 教学重点：熟练掌握6个昆虫类单词及insects的发音 教学难点：让学生读准6个昆虫类单词及insects的发音，掌握发音规律，知道以y结尾的可数名词变为复数时的变化规律。 教学过程： Step 1借助情境图，激发兴趣，揭示课题 1.出示情境图，公园的一角 T: Here’s a picture. Is it nice? What can you see in the picture? T: Today, let’s learn some words about insects. 2.揭示课题，读2遍 Step2利用猜谜的游戏，呈现新单词，学习新单词 1.边听边猜，激发兴趣，学习新单词a grasshopper , a bee 教师讲两个昆虫的特点，让学生猜他们是什么？学生猜对后，教师呈现昆虫的图和单词，带领学生跟读，并指导单词grasshopper中a 和o的发音以及字母组合ee的发音。利用已知的单词学习新单词的发音。 2.自主阅读，猜一猜，他们是哪些昆虫 （1）学生自己读文本，猜文本中所指的是哪些昆虫。学生抓住昆虫的特点，思考。 （2）核对答案，并学习他们的发音，同时学习他们的复数形式及发音。 （3）引导学生观察发现，掌握以辅音字母+y 结尾的可数名词复数形式的变化规律。 3．整体呈现单词，齐读 整体呈现新单词，播放录音让学生整体跟读一遍，加以巩固。Step3 巩固操练 1.仔细阅读，根据歌谣内容，选择正确的图，填空。 鞋舌上标注说明：CM即厘米，为鞋的内部长度;EUR即欧洲码，为中国人平时购鞋时所说的鞋码;US即美国码，UK即英国码也都是选购运动鞋时的一个参照。脚板窄者选鞋不会有太大影响，脚板宽或厚者需穿大一号甚至大二号的鞋! 鞋子尺码对照表 标准通用尺码对照表 男鞋尺码对照表(标准通用) 女鞋尺码对照表(标准通用) Adidas 尺码对照表Adidas 男鞋尺码对照表 欧洲码/EUR 3 9 40 40. 5 41 4 2 42. 5 43 44 44. 5 45 4 6 46. 5 4 7 厘米/CM 2 4 24. 5 25 25. 5 2 6 26. 5 26. 5 27 27. 5 27. 5 2 8 28. 5 2 9 英国码/UK 6 6.5 7 7.5 8 8.5 9 9. 5 10 10. 5 1 1 11. 5 1 2 标准尺码(mm) 240 245 250 255 260 265 270 275 280 285 290 295 女式 欧洲码 /EUR 36 36. 5 37 38 38. 5 3 9 40 40. 5 41 4 2 42. 5 厘米/CM 22 22. 5 23 23. 5 23. 5 2 4 24. 5 24. 5 25 2 6 26. 5 英国码/UK 3. 5 4 4. 5 5 5.5 6 6.5 7 7. 5 8 8.5 中性欧洲码 /EUR 36 36. 5 37 38 38. 5 3 9 40 40. 5 41 4 2 42. 5 43 44 44. 5 45 4 6 厘米/CM 22 22. 5 23 23. 5 23. 5 2 4 24. 5 24. 5 25. 5 2 6 26. 5 26. 5 27 27. 5 27. 5 2 8 英国码/UK 3. 5 4 4. 5 5 5.5 6 6.5 7 7.5 8 8.5 9 9. 5 10 10. 5 1 1 Nike 尺码对照表Nike 男鞋尺码对照表 欧洲码/EUR 38. 5 39 4 40. 5 4 1 42 42. 5 43 4 4 44. 5 4 5 45. 5 4 6 47 47. 5 厘米/CM 24. 5 24. 5 2 5 25. 5 2 6 26. 5 27 27. 5 2 8 28. 5 2 9 29. 5 3 30. 5 31 美国码/US 6 6.5 7 7.5 8 8.5 9 9.5 1 0 10. 5 1 1 11. 5 1 2 12. 5 13 标准尺码(mm) 240 245 250 255 260 265 270 275 280 285 290 Nike 女鞋尺码对照表 欧洲码 /EUR 35 35. 5 36 36. 5 37. 5 3 8 38. 5 3 9 40 40. 5 41 4 2 43 创作编号：BG7531400019813488897SX 创作者：别如克* 微课的类型介绍 按照不同的划分方法，微课可以被分为许多种类型，其中按照教学方法来分类，微课大致可以划分为分别为五类，分别为：讲授类、讨论类、启发类、演示类、练习类等。那么今天我们就为大家介绍几种常见的微课类型，以便于大家在今后的微课制作中有更好设计思路和创意。 一、讲授类 讲授类微课适用于教师运用口头语言向学生传授知识,如描绘情境、叙述事实、解释概念、论证原理和阐明规律。这是中小学最常见、最主要的一种微课类型。 1.课堂实录微缩版 这种类型的微课中有教师、有学生、有活动、有交互……然而学生不是教研员，也不是评课专家。他不需要观看师生活动过程，学生需要的仅仅是学习内容本身。 2.画中画版 这种方式的优点在于，老师的头像出现在视频局部，仿佛老师就在自己身边一对一讲解，亲切而自然，更易于被学生接受从而愿意去学习。 二、讨论类 讨论类微课适用于在教师指导下，由全班或小组围绕某一种中心问题通过发表各自意见和看法，共同研讨，相互启发，集思广益地进行学习。 三、演示类 1.幻灯片动画式 演示类微课适用于教师在课堂教学时，把实物或直观教具展示给学生看，或者作示范性的实验，或通过现代教学手段，通过实际观察获得感性知识以说明和印证所传授知识。 PPT类微课是指教师借助PPT的视频录制功能将嵌入有课程讲解配音的PPT直接录制成流媒体视频。这类微课视频的制作门槛低，要求老师必须具备一定的动画设计制作能力。 2.手机+白纸 工具随手可得，技术难度低，操作快捷方便，画面真实亲切，并且易于分享 结语： 但在实际微课的设计与拍摄时，老师还得根据课程的性质、教学的要求、学校的实际硬件条件及自身的技术能力来选择微课的类型，只有这样，微课才能真正与课堂教学相结合，并能通过翻转课堂教学来提升课程教学的质量。 创作编号：BG7531400019813488897SX 创作者：别如克* 鞋子各部位中英文对照 帮面-UPPER 后帮-BACK COUNTER 内里-LINING 大底-OUTSOLE 中底-INSOLE 中底标-INSOLE LABEL 鞋眼-EYELET 鞋眼片-EYELET STAY 鞋带-LACE 魔术扣-VELCRO 鞋舌-TONGUE 鞋跟-HEEL 靴帮-CUT 高帮-HIGHT CUT 低帮-LOW CUT 边墙-SIDE SHOE 沿条-WELT 刺绣-EMBROIDERY 扣子-BUCKLE 拉练-ZIPPER 松紧带-ELASTIC LACE（GROE） 饰片-ORNAMENT 铁心-SHANK 加强带-REINFORCE TAPE 泡棉-FOAM 飞机板-INSERTER 跟皮-HEEL COVER 鞋鞍-SADDLE 满帮-WHOLE VAMP 鞋垫（中底垫皮）-SOCK LINING 鞋面前端-VAMP 鞋头-TOE CAP 套头-TOE BOX 鞋领-COLLAR 鞋腰QUARTER 滴塑片-PLASTIC PIECE 鞋统-SHAFT 滚边-BINDING 鞋后开口-OPEN BACK 2、品名（ITEM） 运动鞋-SPORT SHOES 反绒皮-SWEDE SHOES 休闲鞋-CASUAL SHOES 皮鞋-LEATHER SHOES 注塑鞋-INJECTION SHOES 时装鞋-FASHION SHOES 靴子-BOOT 拖鞋-SLIPPER 毛绒鞋-ANIMAL SHOES（PLUSH） 沙滩鞋-BEACH SANDAL 室内鞋-INDOOR SHOES 布鞋-CANVAS SHOES 凉鞋-SANDAL 3、颜色（COLOUR） 深色-DARK/D. 浅色-LIGHT/L. 银色-SILVER 本微课视频有以下几个优点： 1、通过本节课的教学，让学生进一步体会，数学来源于生活，又用于生活，提供学生生活中熟悉的材料作背景，学生学习兴趣很高。 2、教学设施中，我非常重视开头的引入教学，激发学生学习的兴趣。注意鼓励学生大胆发言，注意从生活中的两幅图片出发，展现知识的形成过程，使学生能够利用已有的生活知识和数学知识，通过知识迁移、类比的方法归纳得出同类项的概念以及合并同类项的法则。使他们不会觉得数学概念学习的单调乏味，逐步提高学生抽象概括的能力。 3、教学的设计主要是体现以“学生为主体，教师为主导”的教学理念。整个教学过程都是学生在思考、交流，相互比赛，并解决问题，老师只是进行适当的点拨，从而真正体现了以学生为主体，教师为主导的教学理念。学生通过自学，再小组讨论，把不懂的问题都在组内消化完成。全班交流展示时，所举同类项的例子，能检验该学生是否真正掌握了同类项的概念，突出了合作交流的重要性。 4、通过议一议，汇报学习成果，培养了学生的数学语言表达能力，促使学生对合并同类项的法则理解记忆。通过比一比，看谁反应快；填一填，看谁写得最快；全班分为两组进行比赛能检验学生对同类项的概念及合并同类项的法则是否掌握，学生通过两组比赛活动，也能发扬学生合作学习的精神，进一步培养学生团结协助、严谨求实的学习精神。从而激发了学生探究数学的兴趣，更能发挥学生解决问题的主动性，使每个学生在比赛活动中都有收获。 5、通过学生谈收获，教师做补充，培养学生的数学语言表达能力和自我整理的学习习惯。因此整堂课主要突出了以下三个方面：贯穿了一个原则——以学生为主体的原则；培养了一种意识——合作交流的意识；锻炼了一种能力——数学语言表达能力。 鞋类专业术语中英文对照 目录： 鞋子种类 (2) 部位名称 (3) 材料名称 (4) 问题点描述 (6) Sports shoes运动鞋 Casual shoes便鞋 Hiking shoes/Traveling shoes旅游鞋Slipper拖鞋 Sandals凉鞋 Boots马靴 Work shoes工作鞋 Beach Shoes沙滩鞋 Canvas shoes帆布鞋 Pumps单鞋/跟鞋 Climbing shoes登山鞋 Football shoes足球鞋 Jogging shoes慢跑鞋 Basketball shoes篮球鞋 Leisure shoes休闲鞋 Tennis shoes网球鞋 Baseball shoes棒球鞋 Aerobic shoes舞蹈鞋 Leather shoes皮鞋 Sandal凉鞋 flip-flops 夹脚/人字拖 Slippers拖鞋 Sneakers平板鞋/旅游鞋 ballet shoes芭蕾舞鞋 Moccasin 鹿皮鞋 Patent leather shoes 漆皮皮鞋 Boot 靴子 Bootie短靴 Clog 木拖鞋 galosh, overshoe 套鞋 Walking Shoes步行鞋 Artificial leather/PU人造皮革 healthy shoes, healthcare shoes保键鞋，健康鞋 Safety shoes 安全鞋 High heel高跟鞋 Skateboard滑板鞋 Skating shoes滑冰鞋 Grass-sliding shoes 滑草鞋 Skiing shoes 滑雪鞋 Orthopedic shoe矫正鞋 Cotton shoes棉鞋Racing shoes 跑鞋 dress shoes 时装鞋 fashion shoes 精致鞋（装饰鞋，盛装鞋）plastic shoes塑料，塑胶鞋 children shoes童鞋 Cement shoes冷粘鞋 Injection shoes注塑鞋 Vulcanized shoes硫化鞋 Snow boots 雪地靴 Cork slipper 软木拖 Croco shoes 花园鞋 鞋子种类(shoes variety) 鞋子尺寸测量方法及尺码对照表 鞋子尺寸测量 为购买到最适合自己的尺码，建议您先认真参考非常重要的有关尺码测量的介绍内容: 注： 1、"抬脚测量是大家最容易犯的错误!如果抬脚测量，由于脚没有受力的缘故，测量出来的数据会偏小而不准确。所以测量时要求身体直立，体重均分于双脚，这样才能测出准确的尺码。 2、人由于行走习惯和用力不一的原因，基本上每个人的两只脚都不一样大小，购买鞋子的时候应按照最大那只脚来选择尺码。(差之毫厘，失之千里哦) 3、你平时都穿多大尺码的鞋?请勿提供球鞋尺码。 4、脚板是肉肉的?还是瘦而没肉? 5、请您按前面介绍的测量方法核准尺码，该方法是中华人民共和国国家质量监督局对我国制鞋行业的规范标准。注意测量出来的数据一定要和平时自己穿的码数基本协调才对噢。 鞋子尺码对照表 我们常用的两种鞋码一种是英美制的，就是一般比较大的那个，一种是我国制定的，就是较小的。 换算公式： 中国制/2-10=英美制 写的尺码大概分四种： 美国、英国、欧洲和毫米数。比如说： US UK EUR MIM 9 8 42 270 我们中国一般用欧洲号。 女鞋 脚长(cm) 22."5 23 23."5 24 24."5 25 25."5 26 中国35 36 37 38 39 39 40 40 美国5 5."5 6 6."5 7 7."5 8 8."5 英国4 4."5 5 5."5 6 6."5 7 7."5 欧洲35 36 37 38 39 39 40 40 .男鞋 脚长(cm) 24." 525." 526."5 27 27."5 28 中国43 44 45 46 美国 77." 588."59 9."5 10 10."5 英国 66." 577."58 8."5 9 9."5 欧洲43 44 45 46 希望以上信息对网购族们有一定的帮助作用。 海淘鞋类尺码对照表 + 经验分享 一、长度 中国尺码和欧码一致，计算公式为：脚长值（mm）/5-10。例如225/5-10=35码。 美码和英码每0.5为一档，同一尺寸英码比美码小1-2号。 美码没有完美的计算公式，大致可以用0.75*欧码-23来计算。 附男女鞋、童鞋国际尺码对照表： 童鞋（婴儿、学步儿、小童、大童） 注意：不同品牌的尺码差异可能较大，购买前最好上品牌官网查询其尺码说明（对 照表）。 二、宽度 一般在美国网站买鞋子，同一个鞋子尺码下，有五种不同的女鞋宽度、四种不同的男鞋和童鞋宽度： 1、特窄（X-Narrow）：女鞋S号或AA号 2、窄（Narrow）：男鞋N号或C号，女鞋N号或A号，童鞋N号 3、正常中等宽度（Medium）：男鞋M号或D号，女鞋M号或B号，童鞋M 号 4、宽（Wide）：男鞋W号或EE（2E）号，女鞋W号或C/D号，童鞋W号 5、特宽（X-Wide）：男鞋XW号或EEEE（4E）号，女鞋XW号或EE（2E）号，童鞋XW号 Medium（中等）表示脚宽=脚长的3/8，相邻的鞋宽等级表示的脚宽相差3/16英寸（0.476厘米）； 即Narrow比Medium窄0.476厘米，Wide比Medium宽0.476厘米，X-Wide 比Wide宽0.476厘米…… 以脚长25厘米为例，此脚长对应的中等宽度（Medium）为25*3/8=9.375厘米； 如果此人的脚宽很接近9.375厘米，那么就应该选择Medium这档； 如果他的脚宽是9.8厘米，很接近9.375+0.476，那么就应该选择Wide这档。 亚洲人的脚一般比欧美人要宽，脚背宽或者高的朋友可以适当考虑买加宽甚至特宽。 （这是一般建议，不同品牌请具体斟酌，当然最好是去专柜试穿了）。 三、测量方法 （一）量脚的原则 1、请人协助：不能自己量，因为自然站立让脚来承担重力，量出的尺寸才准确； 2、双脚都要测量：按照较大的那只脚的脚长进行鞋码选择； 3、最佳测量时机：下午或您适当运动后，这时脚比较大，同时穿上您打算要穿的袜子，结果会更准确。 （二）量脚的执行要点 1、脚形线：被测量者正常站立在白纸上，测量者用笔绕其脚形粗略的绘制一条边缘线； "微课"简介 "微课"是指按照新课程标准及教学实践要求，以视频为主要载体，记录教师在课堂内外教育教学过程中围绕某个知识点(重点难点疑点)或教学环节而开展的精彩教与学活动全过程。 一、"微课"的组成 学设计、素材课件、教学反思、练习测试及学生反馈、教 师点评等辅助性教学资源，它们以一定的组织关系和呈现方式共同"营造"了一个半结构化、主题式的资源单元应用"小环境"。因此，"微课"既有别于传统单一资源类型的教学课例、教学课件、教学设计、教学反思等教学资源，又是在其基础上继承和发展起来的一种新型教学资源。 二、"微课"的主要特点 理念以小见大，用微课堂带动学生的学习积极性适当的让学生动手做 宗旨关注孩子每一个微变化，从小处着手，创建一个真正属于学生自己的课堂 (1)教学时间较短:教学视频是微课的核心组成内容。根据中小学生的认知特点和学习规律，"微课"的时长一般为5-8分钟左右，最长不宜超过10分钟。因此，相对于传统的40或45分钟的一节课的教学课例来说，"微课"可以称之为"课例片段"或"微课例"。 (2)教学内容较少:相对于较宽泛的传统课堂，"微课"的问题聚集，主题突出，更适合教师的需要:"微课"主要是为了突出课堂教学中某个学科知识点(如教学中重点、难点、疑点内容)的教学，或是反映课堂中某个教学环节、教学主题的教与学活动，相对于传统一节课要完成的复杂众多的教学内容，"微课"的内容更加精简，因此又可以称为"微课堂"。 (3)资源容量较小:从大小上来说，"微课"视频及配套辅助资源的总容量一般在几十兆左右，视频格式须是支持网络在线播放的流媒体格式(如rm,wmv,flv等)，师生可流畅地在线观摩课例，查看教案、课件等辅助资源;也可灵活方便地将其下载保存到终端设备(如笔记本电脑、手机、MP4等)上实现移动学习、"泛在学习"，非常适合于教师的观摩、评课、反思和研究。 (4)资源组成/结构/构成"情景化":资源使用方便。"微课"选取的教学内容一般要求主题突出、指向明确、相对完整。它以教学视频片段为主线"统整"教学设计(包括教案或学案)、课 ★鞋子尺码对照表大全(标准通用)★美国码★日本 码★国际码★英国码★ 鞋子尺码对照表 标准通用尺码对照表 男鞋尺码对照表（标准通用） 尺码 39 40 41 42 43 44 45 46 47 脚长(mm)23.6-24 24.1-245 24.6-250 25.1-255 25.6-260 26.1-265 26.6-270 27.1-275 27.6-280 美国码 6.5 7 7.5 8 8.5 9 9.5 10 10.5 日本码 24.5 25.0 25.5 26.0 26.5 27.0 27.5 28.0 28.5 国际码 245 250 255 260 265 270 275 280 285 女鞋尺码对照表（标准通用） 尺码 35 36 37 38 39 40 41 42 脚长（mm） 22.1-225 22.6-230 23.1-235 23.6-240 24.1-245 24.6-250 25.1-255 25.6-260 美国码 5 5.5 6 6.5 7 7.5 8 8.5 日本码 22.5 23.0 23.5 24.0 24.5 25.0 25.5 26.0 国际码 225 230 235 240 245 250 255 260 Adidas 尺码对照表 Adidas 男鞋尺码对照表 中国码 38 2/3 39 1/3 40 40 2/3 41 1/3 42 42 2/3 43 1/3 44 44 2/3 45 1/3 46 美国码 6 6.5 7 7.5 8 8.5 9 9.5 10 10.5 11 11.5 英国码 5.5 6 6.5 7 7.5 8 8.5 9 9.5 10 10.5 11 标准尺码（mm） 240 245 250 255 260 265 270 275 280 285 290 295 Nike 尺码对照表 Nike 男鞋尺码对照表 中国码 38.5 39 40 40.5 41 42 42.5 43 44 44.5 45 美国码 6 6.5 7 7.5 8 8.5 9 9.5 10 10.5 11 英国码 5 5.5 6 6.5 7 7.5 8 8.5 9 9.5 10 标准尺码（mm） 240 245 250 255 260 265 270 275 280 285 290 Nike 女鞋尺码对照表 中国码 35 35.5 36 36.5 37.5 38 38.5 39 40 40.5 41 美国码 4.5 5 5.5 6 6.5 7 7.5 8 8.5 9 9.5 英国码 2 2.5 3 3.5 4 4.5 5 5.5 6 6.5 7 标准尺码（mm） 220 220 225 230 235 240 245 250 255 260 265 1、结构(construction) 帮面、鞋帮-UPPER 鞋身面/鞋腰- Quarter后帮-BACK COUNTER 内里-LINING 大底-OUTSOLE 中底-INSOLE 中底标-INSOLE LABEL 鞋眼-EYELET 鞋眼片-EYELET STAY 鞋带-LACE 圆带 ROUND半圆带 SEMI-CIRCLE扁带 FLAT 单色双色多色 魔术扣-VELCRO 鞋舌-TONGUE 鞋跟-HEEL 鞋帮-CUT 高帮-HIGHT CUT 低帮-LOW CUT 边墙、大底沿条-SIDE SHOE 沿条-WELT 鞋口- top line 刺绣-EMBROIDERY 扣子-BUCKLE 拉练-ZIPPER 松紧带-ELASTIC LACE（gore）魔术扣-VELCRO 魔术扣毛-VELCRO LOOP 魔术扣丁-VELCRO HOOK 饰片-ORNAMENT 铁心-SHANK 加强带/补强带-REINFORCE TAPE 泡棉-FOAM 海绵-SPONGE飞机板-INSERTER 跟皮-HEEL COVER 鞋鞍-SADDLE 满帮-WHOLE VAMP 鞋垫（中底垫皮）-SOCK LINING 鞋头面-VAMP 鞋头-TOE CAP 前港宝- toe box 后港宝- heel/counter box 鞋领、领口-COLLAR 鞋腰QUARTER 滴塑片-PLASTIC PIECE 靴统-SHAFT 滚边-BINDING 鞋后开口-OPEN BACK 鞋头开口-OPEN TOE 2、品名（ITEM） 运动鞋-SPORT SHOES 反绒皮-SUEDE SHOES 休闲鞋-CASUAL SHOES 皮鞋-LEATHER SHOES 注塑鞋-INJECTION SHOES 时装鞋-FASHION SHOES 靴子-BOOTS 拖鞋-SLIPPERS 毛绒鞋-ANIMAL SHOES（PLUSH） 沙滩鞋-BEACH SANDALS 室内鞋-INDOOR SHOES 布鞋-CANVAS SHOES/VULCANIZED SHOES 凉鞋-SANDALS 3、颜色（COLOUR） 深色-DARK/D. 浅色-LIGHT/L. 银色-SILVER 灰色-GREY 黑色-BLACK水晶色-CRYSTALLINE 白色-WHITE 米白色 OFF-WHITE 嫩绿色-SPRING MINT深绿色-AUGUST GREEN 浅绿色-CITRUS GREEN 草绿色GREEN 05（LIT GREEN）鲜绿色-DESERT WEED 青绿色-SUBLE MOSS 鞋码，通常也称鞋号，是用来衡量人类脚的形状以便配鞋的标准单位系统。目前世界各国采用的鞋码并不一致，但一般都包含长、宽两个测量。长度是指穿者脚的长度，也可以是制造者的鞋楦长。即使在同一个国家/地区，不同人群和不同用途的鞋，例如儿童、运动鞋，也有不同的鞋码定义。下面是尺码对照表，可以帮你解决如何挑选正确的码数；经过量度脚长与脚宽，让你能够挑选到合适的鞋子。 国际标准鞋号表示的是脚长的毫米数。 中国标准采用毫米数或厘米数。如：245是毫米数，24 1/2是厘米数，表示一样的尺码。 换算公式： 厘米数×2－10=欧制（欧制+10）÷2=厘米数 厘米数－18+0.5=美制美制+18－0.5=厘米数 厘米数－18－0.5=英制英制+18+0.5=厘米数 （欧码+10）×5=中国鞋号，如欧码35的鞋，对应的中国鞋号为225；欧码37对应的中国鞋号为235。 鞋号换算表（单位：毫米）34号——22035号——22536号——23037号——23538号——24039号——24540号——25041号——25542号——26043号——26544号——27045号——275。 男人鞋尺码对照表： 厘米24.5 24.5 25 25.5 26 26.5 27 27.5 28 28.5 29 29.5 30 30.5 31 中国码38.5 39 40 40.5 41 42 42.5 43 44 44.5 45 45.5 46 47 47.5 英国码 5 5.5 6 6.5 7 7.5 8 8.5 9 9.5 10 10.5 11 11.5 12 美国码 6 6.5 7 7.5 8 8.5 9 9.5 10 10.5 11 11.5 12 12.5 13 女人鞋尺码对照表： 厘米22 22 22.5 23 23.5 24 24.5 25 25.5 26 26.5 27 27.5 28 28.5 29 30 30.5 中国码35 35.5 36 36.5 37.5 38 38.5 39 40 40.5 41 42 42.5 43 44 44.5 45.5 46 英国码 2 2.5 3 3.5 4 4.5 5 5.5 6 6.5 7 7.5 8 8.5 9 9.5 10.5 11 美国码 4.5 5 5.5 6 6.5 7 7.5 8 8.5 9 9.5 10 10.5 11 11.5 12 13 13.5 微课的类型介绍 按照不同的划分方法，微课可以被分为许多种类型，其中按照教学方法来分类，微课大致可以划分为分别为五类，分别为：讲授类、讨论类、启发类、演示类、 练习类等。那么今天我们就为大家介绍几种常见的微课类型，以便于大家在今后 的微课制作中有更好设计思路和创意。 一、讲授类 讲授类微课适用于教师运用口头语言向学生传授知识,如描绘情境、叙述事 实、解释概念、论证原理和阐明规律。这是中小学最常见、最主要的一种微课类 型。 1.课堂实录微缩版 这种类型的微课中有教师、有学生、有活动、有交互??然而学生不是教研员，也不是评课专家。他不需要观看师生活动过程，学生需要的仅仅是学习内 容本身。 2.画中画版 这种方式的优点在于，老师的头像出现在视频局部，仿佛老师就在自己身边 一对一讲解，亲切而自然，更易于被学生接受从而愿意去学习。 二、讨论类 讨论类微课适用于在教师指导下，由全班或小组围绕某一种中心问题通过发 表各自意见和看法，共同研讨，相互启发，集思广益地进行学习。 三、演示类 1.幻灯片动画式 演示类微课适用于教师在课堂教学时，把实物或直观教具展示给学生看，或者作示范性的实验，或通过现代教学手段，通过实际观察获得感性知识以说明和 印证所传授知识。 PPT类微课是指教师借助PPT的视频录制功能将嵌入有课程讲解配音的 PPT直接录制成流媒体视频。这类微课视频的制作门槛低，要求老师必须具备一 定的动画设计制作能力。 2.手机+白纸 工具随手可得，技术难度低，操作快捷方便，画面真实亲切，并且易于分享 结语： 但在实际微课的设计与拍摄时，老师还得根据课程的性质、教学的要求、学 校的实际硬件条件及自身的技术能力来选择微课的类型，只有这样，微课才能真 正与课堂教学相结合，并能通过翻转课堂教学来提升课程教学的质量。 美国鞋码对照表 Nike,Adidas,Puma,Converse,Kappa,Reebok,New balance尺码查询对照表 NIKE 耐克运动鞋尺码对照表 男鞋尺码对照表 美国码/US6 6.577.588.599.51010.51111.512131415US 欧码/EUR38.5394040.5414242.5434444.54545.54647.548.549.5EUR 厘米/CM24.024.525.025.526.026.527.027.528.028.529.029.530.031.032.033CM 阿迪39 1/34040 2/341 1/34242 2/343 1/34444 2/345 1/34646 2/347 1/34849 1/350 2/3中国码260 265 270 李宁新41 2/3 42 1/3 43 李宁旧42 43 女鞋尺码对照表 美国码/US5 5.56 6.577.588.599.51010.51111.512欧码/EUR35.53636.537.53838.5394040.5414242.5434444.5厘米/CM22.022.523.023.524.024.525.025.526.026.527.027.528.028.529.5 NIKE 耐克服装尺码对照表 男子服装（单位CM） 尺码XS S M L XL XXL 身高160165170175180185胸围（上装）8084889296100腰围（下装）687276808488裤子282930313233 数字165/72A170/74A170/76A175/78A175/78A180/84A 女子服装（单位CM） 尺码XS S M L XL 身高150155160165170 微课创作说明及作品 简介 作品简介 本微课视频的教学内容为牛津小学英语5B Unit8 At the weekends (B)部分的单词教学。本部分的教学内容和教学重点是掌握6个昆虫类单词及insects的发音。教学目标是让学生通过微视频的学习，能够正确、流利地朗读6种昆虫类的单词以及单词insects，并能够熟练运用。教学难点是让学生读准单词发音，掌握发音规律，掌握以字母y结尾的可数名词变为复数时的变化规则。情感态度方面，需要学生具有通过微视频学习知识的兴趣，能够积极、主动的参与到教学活动中来，通过微视频学习的方式，掌握语言技能；能够根据自己对知识的掌握程度和实际需要借助视频学习的优势，反复观看，解决自己的难点问题，积极参与到视频教学中的操练项目，巩固和运用知识。 作品的创作说明： 教学设计 教学内容：牛津小学英语5B Unit8 At the weekends (B) 教学目标：让学生通过微视频学习，能够正确、流利地朗读6种昆虫类的单词以及单词insects，并能够熟练运用。 教学重点：熟练掌握6个昆虫类单词及insects的发音 教学难点：让学生读准6个昆虫类单词及insects的发音，掌握发音规律，知道以y结尾的可数名词变为复数时的变化规律。 教学过程： Step 1借助情境图，激发兴趣，揭示课题 1.出示情境图，公园的一角 T: Here’s a picture. Is it nice? What can you see in the picture? T: Today, let’s learn some words about insects. 2.揭示课题，读2遍 Step2利用猜谜的游戏，呈现新单词，学习新单词 1.边听边猜，激发兴趣，学习新单词a grasshopper , a bee 教师讲两个昆虫的特点，让学生猜他们是什么？学生猜对后，教师呈现昆虫的图和单词，带领学生跟读，并指导单词grasshopper 中a和o的发音以及字母组合ee的发音。利用已知的单词学习新单词的发音。 2.自主阅读，猜一猜，他们是哪些昆虫 （1）学生自己读文本，猜文本中所指的是哪些昆虫。学生抓住昆虫的特点，思考。 （2）核对答案，并学习他们的发音，同时学习他们的复数形式及发音。 （3）引导学生观察发现，掌握以辅音字母+y 结尾的可数名词复数形式的变化规律。 3．整体呈现单词，齐读 整体呈现新单词，播放录音让学生整体跟读一遍，加以巩固。Step3 巩固操练 1.仔细阅读，根据歌谣内容，选择正确的图，填空。 海外购常见尺码对照表 海外购经常会遇到尺码问题，海外购不像国内的B2C商城可以货到付款，无理由退货，买错尺码的话基本上只能送人了。本文整理了相关资料，以帮助网友们下单时尽量正确的选择自己的尺码。需要注意：1、同国内情况类似，国外的尺码也比较混乱，各个品牌的尺码换算不尽相同，本文选取的是互联网上较为流行的版本。2、无论是参与国内的抢购还是参与海外购，熟知自己的身高（衣码）、腰围（裤码）、脚长（鞋码）是必须的。 1、牛仔裤尺码 牛仔裤尺码通常会标识W**L**字样，前者表示腰围，后者表示裤长，例如W29L30，通常可以按腰围选购。有一个简单的计算方法：女性的腰围两字+6，例如1尺9，即19+7=26码。男性的腰围两字+7~9，例如2尺6，即26+8=34码，腰围越大加的数字越大。注：还有个精确的算法，用你的腰围*13.1再四舍五入即可得到准确的尺码。例如2尺2的腰，2.2*13.1=28.8=29码。具体的换算见下表： 2、衣服尺码 美版的衣服尺码使用了和国内相同的S（Small）、M（Medium）、L（Large）+X（eXtreme）的标识方法，但其代表的衣服大小与国内的惯例不同，通常会大一个甚至几个号。不同类型的服装尺码会有所不同，不同品牌的尺码也有较大差异，下面是较为通用的尺码表，网友们可以根据自己的胸围或者腰围选取最接近的尺码： 3、鞋子尺码 鞋子尺码是最为混乱的。中国尺码和欧码是一致的，可以使用公式计算出来，具体为脚长值（mm）/5-10。例如230/5-10=36码。美码没有一个完美的公式可以计算，各个品牌均有自己的转换表，不同品牌的差异可能非常大。基本的规律是，美码和英码每0.5为一档，同一尺寸英码比美码小1-2号，美码大致上可以用0.75*欧码-23来计算。 名鞋库网站上有部分品牌的尺码转换表，可以对号入座试试看。但此表不完全与其他鞋类B2C网站提供的尺码表完全一致，因此还是仅供参考。表格较大，点击后可在新页面查看大图。 男款慕课、翻转课堂、微课的介绍和特点
鞋子尺码对照表大全
海淘鞋子尺码对照表
鞋类中英文对照
微课创作说明及作品简介
国际的鞋尺码对照表
微课的类型介绍
鞋子各部位中英文对照
(完整版)微课亮点介绍
鞋类专业术语中英文对照
鞋子尺寸测量方法及尺码对照表
海淘鞋类尺码对照表
微课简介
鞋子尺码对照表大全
鞋类术语英文对照
美国-中国-国际鞋码对照表
微课的类型介绍
美国鞋码对照表
微课创作说明及作品简介培训资料
海外购常见尺码对照表
相关主题
文本预览