The specification and analysis of network embedded system  

作　　者：张冠华 张连华 白英彩 

机构地区：[1]Dept. of Computer Science and Technology, Shanghai Jiaotong University, Shanghai 200030, China

出　　处：《Journal of Harbin Institute of Technology(New Series)》2005年第4期434-439,共6页哈尔滨工业大学学报（英文版）

摘　　要：This paper proposes a formal method which is used to model and analyze network devices such as touters. It 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 synchronization. Therefore, although there 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 system. This paper extends ACSR-VP to EACSR-VP, which is more adaptive to the features of network devices and specializes in analyzing this kind of embedded system. EACSR-VP adds the notion of n-way communication which allows more than two processes to participate in synchronization. It also enhances value-passing capabilities which make for more flexible specifications. Finally, specifications, verification and analysis methods with EACSR-VP are introduced by a case study of router with multiple input queues.This paper proposes a formal method which is used to model and analyze network devices such as routers. It 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 synchronization. Therefore, although there 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 system. This paper extends ACSR-VP to EACSR-VP, which is more adaptive to the features of network devices and specializes in analyzing this kind of embedded system. EACSR-VP adds the notion of n-way communication which allows more than two processes to participate in synchronization. It also enhances value-passing capabilities which make for more flexible specifications. Finally, specifications, verification and analysis methods with EACSR-VP are introduced by a case study of router with multiple input queues.

关 键 词：Formal method process algebra network devices MODELING 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]