Database of Case Studies Achieved Using CADP

Atomicity Maintenance in EPCReport of ALE

Organisation: North China University of Technology, Beijing (CHINA)
Central Michigan University (USA)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Trading.

Period: 2011

Size: n/a

Description: EPCglobal published a framework for developing applications of Electronic Product Code (EPC) network in 2005. In order to leave flexibility to it user, it only gives a series of interfaces for implementation. The Application Layer Event (ALE) is one of the interfaces through which clients may obtain filtered consolidated EPC data from a variety of Radio Frequency Identification (RFID) readers. The objective of ALE is to reduce the volume of EPC data that comes directly from RFID readers into applications. The processing done at this layer typically involves: (1) receiving EPCs from one or more RFID readers; (2) accumulating data over intervals of time, filtering to eliminate duplicate EPCs and EPCs that are not of interest, and counting and grouping EPCs to reduce the volume of data; and (3) reporting in various forms.

EPCglobal provides an API to facilitate development of ALE applications. The API specifies the atomicity property constraint by a case study while leaving the flexibility of implementation up to the developers. An important issue the developer has to deal with is the atomicity property of event cycle. That is, an event cycle is treated as a single atomic unit and proper handling failure of a read cycle (as part of an event cycle) is critical. If a read cycle failed the EPC data will be lost according to EPCglobal standards. So there is no way to undo a completed operation and reverting the system back to its previous state. To remedy this problem, a fault tolerant strategy is proposed, based on a new architecture for ALE with respect to fault tolerance and design several algorithms implementing the poll method of the API.

Two polling modes (synchronous and asynchronous) and three algorithms for the poll method were proposed and described formally in LOTOS. Successful termination of transactions in the two polling modes was expressed as a temporal property in regular alternation-free mu-calculus, and was checked on the LOTOS specifications using the EVALUATOR model checker of CADP.

Conclusions: As a key component of EPC framework, ALE plays an important role for the reliability and performance of EPC applied systems. The new ALE architecture proposed increases its reliability, and the separation between fine-grained cycle and coarse-grained event cycle, EPC network channels can be released to prevent traffic block. The formal analysis using LOTOS and CADP has shown the effectiveness of the proposed architecture.

Publications: [Sun-Zhao-Wang-Hu-11] Jing Sun, Huiqun Zhao, Wenwen Wang, and Gongzhu Hu. "Atomicity Maintenance in EPCreport of ALE". Proceedings of the 10th IEEE/ACIS International Conference on Computer and Information Science ICIS'2011, pages 224-229, IEEE Computer Society Press, 2011.
Available on-line at:
Prof. Gongzhu Hu
Computer Science Department
Central Michigan University
Office: 115 Pearce Hall
Mount Pleasant, Michigan 48859
Tel: 989-774-2848
Fax: 989-774-3728

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page