Concurrency model and its application to formal protocol specifications

Author

Kim, M.C. ; Chanson, Samuel T. ; Vuong, Son T.

Author_Institution

Dept. of Comput. Sci., British Columbia Univ., Vancouver, BC, Canada

fYear

1993

fDate

1993

Firstpage

766

Abstract

A concurrency model is presented, and concurrent events, concurrency blocks, global states, concurrency measures, communication deadlocks, and data races are defined based on the model. The model allows high-level abstractions to be used for understanding concurrent behaviors. Using the concept of concurrency blocks, it is shown how to compute concurrency measures efficiently. The results are applied to the formal description techniques Estelle and LOTOS to reason about and classify their concurrency behaviors

Keywords

concurrency control; formal specification; protocols; specification languages; Estelle; LOTOS; communication deadlocks; concurrency blocks; concurrency measures; concurrency model; concurrent events; data races; formal description techniques; formal protocol specifications; global states; high-level abstractions; Application software; Clocks; Communication system control; Computer science; Concurrent computing; Debugging; ISO standards; Open systems; Protocols; System recovery;

fLanguage

English

Publisher

ieee

Conference_Titel

INFOCOM '93. Proceedings.Twelfth Annual Joint Conference of the IEEE Computer and Communications Societies. Networking: Foundation for the Future, IEEE

Conference_Location

San Francisco, CA

Print_ISBN

0-8186-3580-0

Type

conf

DOI

10.1109/INFCOM.1993.253293

Filename

253293