Formal verification of activity based specification of protocols

Anand, K. C. ; Shyamasundar, R. K. (2000) Formal verification of activity based specification of protocols Journal of Parallel and Distributed Computing, 60 (5). pp. 639-676. ISSN 0743-7315

Full text not available from this repository.

Official URL:

Related URL:


In this paper, we describe a method to formally verify activity-based specifications such as EBSDL. Starting from EBSDL-like specifications that specify engineering activities in terms of input and output behaviors, we derive programs in an asynchronous language CSP-R. CSP-R programs are then verified by the Maxpar method by composing them with the programs abstracting their environment. EBSDL-like specification and its verification using our method, is illustrated through the example of a fragment of LAPD protocol. The derivation of programs from the specification of activities of the underlying protocols through EBSDL-like specifications provides an important useful tool for formal verification of real-time protocols. We shall also discuss a translation of EBSDL-like specifications to synchronous languages such as Esterel. In the method proposed, it is possible for the user to choose asynchronous or synchronous formalisms depending upon the requirements of verification vis-a-vis logical specification.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
ID Code:56594
Deposited On:24 Aug 2011 11:01
Last Modified:24 Aug 2011 11:01

Repository Staff Only: item control page