Abstract
We present a framework of specification design and proof of processes networks. The design aspect is directed or aided by rules based on temporal specifications and grammar oriented specifications. A network is a set of processes communicating by using channels. The semantics of the network is defined with the help of histories of channel communications. But, more generally, a process is considered to be a set of possible operations on a set of channels. A channel is characterized by communication rules. These communication rules are in fact written as production rules of a communication grammar. We assume the existence of a global clock used to sort communications. Our semantics is based on the abstract data type approach and the temporal logics extended by specific operators (induced by the production rules). Inference rules are derived and allow to take into account communications.
Supported by GRECO C3 and MRES grant
Supported by GRECO C 3
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
C. A. R. Hoare. An axiomatic basis for computer programming. Communication of ACM, 12:576–580, 1969.
N. Francez, K.R. APT and V.P. De Roever. A proof system for communicating sequential processes. ACM TOPLAS, 2(3):359–385, 1980.
S. Kaplan and A. Pnueli. Specification and implementation of concurrently accessed data structures: an abstract data type approach. LNCS, (247):220–244, 1987.
F. Kroger. Abstract modules: combining algebraic and temporal logic specification means. Technique et Science Informatiques, 6(6):559–573, 1987.
N. Levy, A. Piganiol, and J. Souquieres. Specifying in sacso. In Fourth International Workshop On Software Engineering and Design, 1987.
D. Mery. A proof system to derive eventuality properties under justice hypothesis. LNCS, (233), 1986. Bratislava, Tchecoslovaquie.
D. Mery. Méthode axiomatique pour les propriétés de fatalité des programmes parallèles. RAIRO Informatique Théorique et Application, 21(3):287–322, 1987.
R. Milner. A Calculus of Communicating Systems. Technical Report ECSLFCS-87–7, Laboratory for Foundations of Computer Science, August 1986. First published by SPRINGER VERLAG as Vol 92 of LNCS
Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM TOPLAS, 6:68–93, 1984.
Van N’Guyen, A. Demers, D. Gries, and S. Owicki. A model and temporal proof system for networks of processes. Distributing Computing, 1:7–25, 1986.
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs i. Acta Inforrnatica, 6:319–340, 1976.
E.R Olderog and C.A.R Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23:9–66, 1986.
G. R. Perrin. La Communication: Un Outil pour la Specification, la Construction et la Verification de Systemes Paralleles. PhD thesis, Universite de Nancy I, 1985. FRANCE.
A. Szalas. Towards the temporal approach to abstract data type. Fundamenta Informaticae, XI(1):49–64. March 1988.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer-Verlag London
About this paper
Cite this paper
Carrez, F.D., Mery, D. (1990). Temporal Specifications Directed by Grammar and Design of Process Networks. In: Rattray, C. (eds) Specification and Verification of Concurrent Systems. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3534-0_20
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3534-0_20
Publisher Name: Springer, London
Print ISBN: 978-3-540-19581-8
Online ISBN: 978-1-4471-3534-0
eBook Packages: Springer Book Archive