网络嵌入式系统的描述与分析

1、Journal of Harbin Institute of Technology (New Series) Vo1.12, No.4, 2005The specification and analysis of network embedded systemZHANG Guan-hua ZHANG Lian-hua BAI ying-cai(Deptof Computer Science and Technology，Shanghai Jiao tong University，Shanghai 200030，China)Abstract：This paper proposes a forma

2、l method which is used to model and analyze network devices such as routersIt is based on an algebraic process called “ACSR-VP”，which enhances the original CCS algebraic process by incorporating the notions of time，resource requirements，dynamic prioritization，and synchronizationTherefore，although th

3、ere are many formal methods to analyze the timed concurrency system ，ACSR-VP，due to its prominent features，is best fit for analysis of a resource bounded real-time systemThis paper extends ACSR-VP to EACSR-VP，which is more adaptive to the features of network devices and specializes in analyzing this

4、 kind of embedded systemEACSR-VP adds the notion of n-way communication which allows more than two processes to participate in synchronizationIt also enhances value-passing capabilities which make for more flexible specificationsFinally，specifications，verification and analysis methods with EACSR-VP

5、are introduced by a case study of router with multiple input queuesKey words：Formal method；process algebra；network devices；modelingCLC number：TP393 Document code：A Article ID：1005-91l3(2005)O4-0434-06The rapid growth of the Internet has demonstrated the large demand for network devices such as route

6、rs and switches. With widely used applications such as multimedia，the functions of the router becomes more and more complicated and the implementation and design of routers becomes increasingly difficult Therefore，even a trivial error may lead to the redesign of the whole systemTo mitigate this risk

7、，an iterative process of design-implementation-design is required Consequently，the development cost is very expensive The formal method can be used to specify the system before its implementation and analysis to validate and test itAs a resultall errors can be corrected during the design process and

8、 subsequently development cost is greatly reducedResearch on formal methods for rea1-time embedded systems is very active Most of the work falls into four main categories： timed logics， automata theory ，Petri nets and process algebra In methods based on timed logics， systems are described by a set o

9、f assertions and properties are represented as theoremsA property holds for a system if it can be logically reasoned from the assertions Such methods can process strict reasoning but they do not have an execution model and therefore they cannot lead to an implementation directlyIn timed automata met

10、hods，computation models are represented using finite state automata and a set of clock data associated with itThe state transition can be expressed as a consequent occurrence of a set of events with their time constraints Such a method does not support synchronous communicationPetri nets can describ

11、e many concurrency features， but it only is a mode1 It has no calculiMethods based on Process algebra use interleaving models to specify concurrencyTypical examples are ， andSuch methods can represent detailed behavior of systems and both CCS and CSP have good algebraic properties They not only can

12、model behavior of systems，but also have a reasoning calculi system To use such methods under real-time environments， many extensions have been introduced by many researchers Some examples are timed CCS(TCCS)，CCS with ，CSP with delay and，etcIn ，Lee proposed an ACSR framework，which is a kind of timed

13、process algebra based on the CCS mode1 This method incorporates synchronous，time，resource requirements and priorities into CCSIt supports modular specification and validation of the system It is very adaptive to analyze resource bound systems such as routers. is an extension of ACSR with dynamic pri

14、orities and a value-passing mechanism as follows：1)priorities could be value expressions containing variables；2)an instantaneous event is added with a value expression to represent value-passing The network embedded system belongs to a real-time embedded system with bounded resources Its main task i

15、s to process input packets and a certain packet forwarding rate must be satisfied Although much research of formal methods for embedded systems has been done，there is no special focuses on network devices This paper extends ACSR-VP to EACSR-VP, which is more adaptive to features of network devices a

16、nd presents specifics in analyzing this kind of embedded system This method inherits many of the best characteristics of ACSR-VP and adds several novel concepts Firstly the notion of n-way communication is added，which allows more than two processes to participate in synchronizationSecondly，this pape

17、r enhances value-passing capabilities which make values pass through more than two possible processes It also adds subscripting to the label of instantaneous event to make value-passing more flexible Value-passing also can then be used to record the state of execution At last，dynamic priorities are

18、used to implement algorithmic scheduling input queues and synchronization among input queue processes and routing process This paper is organized as follows：in Section 1，the syntax of EACSR-VP is defined and its semantics is explained；Section 2 introduces specification，validation and specification m

19、ethod by the case study of router with multiple input queues；finally，Section 3 presents the papers conclusions1 EACSR-VP1.1 SyntaxDefinition 1 The domain of time is the set N of natural numbers Denoted by tN . The domain of priorities is the set Z of integers、denoted by pZLet I denotes resources set

20、Definition 2 The behavior of process is shown as a label transition system It is a subset of ProcActProcLet P1 be a process. It may have the following behavior: That is， first executes and evolves into， which executes ，etcHere，(，P2)，(，)， LDefinition 3 The set of primitive actions broken into the sub

21、set of timed action and the subset of instantaneous eventsDefinition 4 Timed action takes one time unit to execute and is represent -ed as a list of resources and associated priorities as follows： A distinguished timed action ，or O/，stands for idling of one time unitLet denotes the set of resources

22、used， and denotes the priority of on resource .Definition 5 Instantaneous action is also called an instantaneous event，which takes no time to execute It is used, primarily， for communication among proce -sses It is represented as a pair，consisting of label and an associated priority Let denote an ev

23、ent labeled denotes an event labeled with a subscript and denotes subscript， and denotes expressions， and denotes vectorsInstant -aneous events of ACSR-VP can be defined as follows： And where denotes a synchronous event between two processes， and denotes the receiving event of a process， and denotes

24、 a sending event of a process， denotes a synchronous event among more than two processes， denotes a receiving event of a process from a broadcasting process，and denotes a broadcasting event of a processLet denote the label of and denotes priority of label Definition 6 Processes and actions are basic

25、 units in algebraic description and calculi and they use operators to process algebraic calculiLet and denote processes， denotes labels denotes expre -ssion， denotes vector， denotes resource and denotes the set of free value variables in The syntax of an EACSR-VP process term is as follows： represen

26、ts a deadlock process that does nothingand are event and action prefix process terms, respectively represents a non-deterministic choice between and represents the parallel composition of and in which the events from and are interleaved while the timed actions from and ，if not conflicting，are merged

27、The close operator，produces a process that monopolizes the resources in The Restriction operator，restricts events with labels in from being executed is used to represent the behavior of whereby the identities of resources in are concealedEach process constant is associated with a process definition

28、of form where，. Conditional process term is introduced to incorporate conditions on value variablesIf the Boolean expression is evaluated to be true，process will be executed.1.2 Semantics Interpretation1.2.1 CommunicationCommunication is an essential method to achieve the synchronization of concurre

29、nt processes The common communication primitives are either 2-way synchronous communication between two processes or n-way synchronous communication among more than two processes In EACSR-VP, n-way synchronous communication among one sending process and several receiving processes is introduced main

30、lyDeftnition 7 The 2-way synchronous communication allows only two processes to synchronize at a moment，which is implemented by a sending event“!”and a receiving event“?”To prevent further synchronization with an already established communication，the effect of communication between two events “-” an

31、d “?” is to convert the simultaneous occurrence of the two events into the internal event“”In EACSR-VPtwo kinds of event labels are definedOne is ，and the other is ，where denotes the subscript of event label For example， denotes synchronization between the processes and ；and if denotes synchronizati

32、on between the processes and Definition 8 The point-to-multipoint communication allows one sending process and several receiving processes to participate in simultaneous synchronizationSuch synchronization is implemented by a sending event“”and several receiving events“”The effect of communication b

33、etween them is to convert the simultaneous occurence of those events into the internal event“”The point-to-multipoint communication allows more than two processes to participate in synchronizationFor example， denotes synchronization among the processes， and 1.2.2 Unprioritized operational semanticsJ

34、ust like ACSR-VPthe operational semantics of EACSR-VP is defined in two stepsFirst, an unprioritized transition system is used to express operational semantics in the standard style Subsequently，a prioritized transition system is defined to prune executions with priority informationThe unprioritized

35、 transition rules in Fig.1 constitute the unconstrained operational semantics of EACSRVP processesThe domain of value variables is the set of integers Let denote variables or constants and let denote vectors A vector can have several elementsFor example, has two variables and Let denote the value of

36、 in and denote the Boolean va1ue of Fig.1 A model of router with multiple input queuesIn the following，we only highlight the modified or the newly introduced transition rules of which we use bold fonts for the titles in Tab.1 For other rules，we refer to Rule ActI2 states the use of prefix operator w

37、hen more than two processes are synchronizedCompared with rules ActI3 and ActI4，rule ActI5 and ActI6 deal with instantaneous events with labels with subscript and they are used together with rule ParCom2 which deals with synchronization of two concurrent processesCompared with rules ActI3 and ActI4，

38、rule ActI7 and ActI8 deal with instantaneous events which are used for n-way communication and they are used together with rule ParCom3 which deals with synchronization of more than two concurrent processes，which is described in detail in the section 1.2.1 Tab1 The unprioritized transition rules 1.2

39、.3 Prioritized semanticsPrioritization is an important property which is combined with resources and processes tightly It is used to constrain competition between concurrent processes to the same resourcesA process may require several resources and every resource has different priorities To the same

40、 resourcethe process with highest priority will succeed in controlling the resourceThe router has two main prioritiesOne is the priority of the task which is used to compete for CPU and the other is the priority of the input queue which is used to compete for routing bandwidth The first priority is

41、assigned through the operating systems scheduler and the later priority is assigned through the scheduler of queuesTo define the operational semantics of EACSR-VP which accounts for preemption，we define the preemption relation between actions， based on priorities，as follows：Definition 9 For two acti

42、ons，, say preempts ，if one of the following cases holds：1Both and are timed actions in ，where 2Both and are events in ，where 3 and ，with EACSR-VP supports dynamic priorities and both their assignment and adjustment are implemented through value-passing among processesCorresponding to two kinds of sy

43、nchronization among processes which are described in the section 1.2.1， there are two methods to implementation of dynamic priorities through value-passing between processes A process can receive information of priorities， and change them For example，in ，the initial priority of is When it receives i

44、nformation through , its priority is changed to be ,In the initial priority of and is When they receives information through ，the priority of is changed to be and the priority of is changed to be .Therefore，prioritization synchronization among processes is implemented2 Case Study：Model of Router wit

45、h Multiple Input QueuesIn this section，the specification and analysis by EACSR-VP is introduced by the case study of model of router with multiple input queues based on value-passing of rate of packet2.1 SpecificationThis router model is composed of three parts including the packet preprocessing mod

46、el， the queuing model and the routing scheduling mode1 which is shown in Fig.1The system in its initial state is represented by process Where,denote the initial priority of and denotes the initial priority of denotes the routing capability within a time unit2.1.1 Packet preprocessing modelThe packet

47、 preprocessing process is responsible for preprocessing work such as receiving packets，classifying packets，etc After that，packets are put into appropriate input buffersChannel is used to receive packets and is used to send packets to buffersThe model is specified as follows： where is the polling per

48、iod of and is the capability of process within a time unit Value-passing of is input packet number and packet class2.1.2 Queuing modelThe input buffer of the router is implemented through the queue with limited length When a packet is put into a full queue, the overflow event will happen，which is ca

49、lled packet-lost If a queue named and its length is ,then this queue would have different states, which can be denoted as ， and overflowThey can be transited to each other according to input or output of packetsDifferent queues can have different priorities，but their priorities are changed dynamical

50、ly Routing scheduling process schedules queues by their current related prioritiesThe specification of queues can be divided into five probable operations including packets input， idle operation， priority change， queue state transmission and packets output They are connected by operator“ ”and the mo

51、del can be specified as follows： Instantaneous event is used to transmit the current states of queues to routing module Process deals with the input of packets of queues as follows： Process deals with the output of packets of queues as follows： Process deals with the change of priorities of queuesMa

52、ny methods can be used to implement it according to different scheduling algorithm of queues In this example，an iterative priority is implemented as follows： where， denotes the maximum number of priorityDuring the execution of the system ，the state can be recorded through the free variables of the p

53、rocesses and value-passing For example，the process can record the overflowed packets number of the queue through event as follows： Process does not use any resources，and it is only responsible for receiving the event of overflow of queues and recording it in the variable count2.1.3 Routing schedulin

54、g modelRouting module is the core of routerIt schedules the input queue to receive a packet，and then searches the routing table for it Finally，it puts the packet to the corresponding interfaceIn the model with multiple input queues，routing bandwidth is the main resource that they compete for Current

55、ly，there are many scheduling algorithms，such as Weight Fair Queueing (WFQ) algorithm，Hierarchical Link Shared Service Queueing algorithm, etcAll of them can be implemented through dynamic priorities and specified using EACSR-VPIn this case，WFQ algorithm is implemented as follows： where， denotes the

56、total number of routing packets within a routing scheduling period Routing module can receive the current state of the input queue that is ready to be scheduled through the event ，where denotes the index of the input queue， denotes the current number of packets of the input queue and denotes the cur

57、rent priority of the input queueThrough the event ，routing module broadcast the information of changing priorities and at the same time, all input queues receive the information through and then change their priorities accordinglyThrough the event ，the routing module inform the related queue of the routed packetsFor example，let ，then the input queue would synchronize with the routing m