The Open Automation and Control Systems Journal

2014, 6 : 1958-1961
Published online 2014 December 31. DOI: 10.2174/1874444301406011958
Publisher ID: TOAUTOCJ-6-1958

A New Method for Modeling on Concurrent System

Jing Guo , Zhongwei Xu and Meng Mei
School of Electronics & Information Engineering, Tongji University, Shanghai, 201804, China.

ABSTRACT

Binary decision diagrams (BDDs) are effective means to cope with complex concurrent system. But the size of BDD itself can be relatively large. We study the BDD representation of large synchronous, asynchronous and interleaved processes with communication via shared variables. Due to the features of communication, we introduce a novel representation strategy. Based on the model, we continue to model and map up the synchrony, and detect the deadlock errors.

Keywords:

Formal verification, Model checking, BDD, Concurrent system.