|
|
|
@inproceedings{DBLP:conf/adbis/EhikioyaB97,
author = {Sylvanus A. Ehikioya and
Ken Barker},
title = {CSP with Record Data Type for Supporting Transaction Systems
Specification},
booktitle = {Proceedings of the First East-European Symposium on Advances
in Databases and Information Systems (ADBIS'97), St.-Petersburg,
September 2-5, 1997. Volume 1: Regular Papers},
publisher = {Nevsky Dialect},
year = {1997},
pages = {64-71},
ee = {db/conf/adbis/EhikioyaB97.html},
crossref = {DBLP:conf/adbis/97},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX
The need to support concurrency in recent advanced transaction systems that use highly structured and complex data types means synchronization is necessary to guarantee data/ operations dependencies are maintained, thereby ensuring the correctness of results. To correctly and adequately capture a system's intended behaviour requires a specification language that provides elegant means to concisely specify operations on structured data in addition to capturing communications among the system's subcomponents. Although CSP has been found most suitable for the specification and design of distributed systems, it is restricted to simple data types. The inability of CSP to provide structured and complex data types undermines its expressive power and usefulness as a specification language for advanced database transaction applications where there is need to examine data fields of a data item. Clearly, the types of data objects available in a language have a profound impact on its suitability for a particular application since these data object types provide a meaningful representation of the problem being solved.
This paper presents mechanisms for supporting structured data types in the CSP specification language and to perform semantic transformations that enhances CSP's expressive power beyond primitive atomic data types. The extension proves beneficial in producing more natural abstract manipulations in system specifications required by database systems. The extensions are amenable to formal mathematical reasoning because they contain regular and simple structure. Moreover, as the field selectors are fixed at declaration time, the components of a record may be accessed as efficiently as scalar data objects so no efficiency is sacrificed. Also, defining the semantics of a data type formally facilitates proofs of correctness for implementations and in proving properties about data.
Copyright © 1997 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.