《网络嵌入式系统的描述与分析》由会员分享，可在线阅读，更多相关《网络嵌入式系统的描述与分析（25页珍藏版）》请在金锄头文库上搜索。
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 paper enhances value-passing capabilities which make values pass through more than two possible processes It also adds subscri
