Abstract
Clear mathematical description of large scale digital systems is not possible without extensive use of encapsulation. We argue that standard models of concurrency and composition are too unstructured to support modular composition and verification of systems. We offer an alternative model based on algebraic feedback products of finite state machines. We also describe a technique for concisely specifying complex state machines in terms of state dependent (modal) functions. The product automata model provides a precise interpretation for the formal expressions, and the formal expressions provide an intuitive language for describing multi-layer concurrent digital systems. We develop several examples, showing how specifications of varying levels of abstractness can be composed to specify rather complex systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K. Apt, editor. Logics and Models of Concurrent Systems. Springer-Verlag, 1985.
R. T. Boute. On the shortcomings of the axiomatic approach as presently used in computer science. In Compeuro 88 Systems Design: Concepts Methods, and Tools, 1988.
E. M. Clarke, Emerson A., and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach. In Proceedings of the 10th Annual Symposium on Principles of Programming Languages, pages 117–119, 1983.
J.W. de Bakker, editor. Current Trends in Concurrency. Number 224 in Lecture Notes in Computer Science. Springer-Verlag, 1985.
Ferenc Gecseg. Products of Automata. Monographs in Theoretical Computer Science. Springer Verlag, 1986.
R. L. Goodstein. Recursive Number Theory. North Holland, Amsterdam, 1957.
D. Harel. Logics of programs: Axiomatics and descriptive powers. Technical Report TR-200, MIT/LCS, 1978.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
S. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83–94, 1963.
E.F. Moore, editor. Sequential Machines: Selected Papers. Addison-Welsey, Reading MA, 1964.
J.S. Ostroff and W.M. Wonham. Modelling, specifying, and verifying real-time embedded computer systems. In Symposium on Real-Time Systems, Dec 1987.
Rozsa Peter. Recursive functions. Academic Press, 1967.
K. Voss, H.J. Genrich, and G Rozenberg, editors. Concurrency and Nets: Advances in Petri Nets. Springer-Verlag, 1987.
V. Yodaiken and K. Ramamritham. Axiomatic specification of automata. Technical Report in preparation, University of Massachusetts, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yodaiken, V. (1991). A logic-free method for modular composition of specifications. In: Akl, S.G., Fiala, F., Koczkodaj, W.W. (eds) Advances in Computing and Information — ICCI '90. ICCI 1990. Lecture Notes in Computer Science, vol 468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53504-7_76
Download citation
DOI: https://doi.org/10.1007/3-540-53504-7_76
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53504-1
Online ISBN: 978-3-540-46677-2
eBook Packages: Springer Book Archive