Formal Specification and Simulation of a Real-Time Concurrency Control Protocol
The executable specification tool ExSpect is presented. A concurrency algorithm for a real-time distributed system is specified in the language of this tool. Parts of the specification are shown and it is demonstrated how the executable specification can assist in the concurrency control development.
KeywordsExecution Time Concurrency Control Read Request Executable Specification Request Manager
Unable to display preview. Download preview PDF.
- D.K. Hanomer, E.J. Luit, O. van Roosmalen and P.D.V. van der Stok, “The Dependable Distributed Operating System DEDOS: an overview”, TUE computer Note, (in preparation).Google Scholar
- J.C. Laprie, “Dependability: an unifying concept for rehable computing and fault- tolerance”, T Anderson, (ed.), Blackwell Scientific Publications, Oxford, 1989.Google Scholar
- B. Meyer, “From structured programming to object-oriented design: The road to Eiffel”, Structured programming, Springer Verlag, 1989.Google Scholar
- P.D.V. van der Stok and A. Engel, “Shared data concepts for DE- DOS”, Proc. of the 10th IFAC workshop of Dist. Comp. Control Systems, Semmering, Austria, 9–11 Sept. 1991, IFAC Workshop series, Ed. H. Kopetz and M.G. Rodd, No 3, Pergamon Press, 1992.Google Scholar
- P.D.V. van der Stok, O.S. van Roosmalen, E.J. Luit and D.K. Hammer, “An object-oriented approach to edependable responsive systems”, 1st Int. Workshop on Responsive Systems, Golfe-Juan, France, 3–4 Oct. 1991.Google Scholar
- K.M. van Hee, L.J. Somers, M. Voorhoeve, “Executable specifications for distributed information systems”, E.D. Falkenberg, P. Lindgreen (eds.). Information system concepts: an in-depth analysis, North-Holland, 1989.Google Scholar
- K. Jensen, “Colored Petri Nets: A High Level Language for System Design and Analysis”, G. Rozenberg (ed.). Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer Verlag, 1991.Google Scholar
- P.T.A. Thijssen, “Specification of DEDOS Concurrency Control with ExSpect”, EUT master’s thesis, Dec. 1991.Google Scholar
- CCITT, Recommendations Z.100-Z.104, Vol VI, Ease VLIO, 1984.Google Scholar
- ISO, DP8807rev, “LOTOS: A formal descrition tecnique based on temporal ordering of observational behavior”, Geneva, 1988.Google Scholar