Abstract
As part of a comprehensive design concept for complex reactive systems we investigate the derivation of formal requirements and design specifications at systems level. We discuss the meaning of correctness with respect to the embedding of mathematical models into the physical world. A crucial aspect in our attempt to make the logic link between the application domain specific view and the formal view explicit is the concept of evolving algebra [13, 14]; it provides the formal basis of a specification methodology which has successfully been applied to a variety of specification and verification problems. We introduce an evolving algebra abstract machine as a conceptual framework for the development of tools for machine based analysis and execution of evolving algebra specifications.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ch. Beierle, E. Börger, I. đurđanović U. Glässer, and E. Riccobene. An evolving algebra solution to the steam-boiler control specification problem. Seminar on Methods for Specification and Semantics (Dagstuhl, June 1995), Report, 1995.
E. Börger. Annotated bibliography on evolving algebras. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.
E. Börger, U. Glässer, and W. Mueller. Formal definition of an abstract VHDL'93 simulator by EA-machines. In C. Delgado Kloos and Peter T. Breuer, editors, Semantics of VHDL, volume 307 of The Kluwer International Series in Engineering and Computer Science. Kluwer Academic Publishers, 1995.
E. Börger and D. Rosenzweig. A mathematical definition of full Prolog. Science of Computer Programming, 1994.
E. Börger and D. Rosenzweig. The WAM — definition and compiler correctness. In L. C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, Series in Computer Science and Artificial Intelligence. El-sevier Science B.V./North-Holland, 1995.
E. Börger, I. đurđanović, and D. Rosenzweig. Occam: Specification and compiler correctness. Part I: The primary model. In E.-R. Olderog, editor, Proc. of PROCOMET'94 (IFIP Working Conference on Programming Concepts, Methods and Calculi), pages 489–508. North-Holland, 1994.
Egon Börger. Three pragmatic suggestions for making formal methods practical. Dipartimento di Informatica, Università di Pisa, Report, 1995.
Egon Börger, Giuseppe Del Castillo, Paola Glavan, and Dean Rosenzweig. Towards a mathematical specification of the APE100 architecture: The apese model. In B. Pehrson and I. Simon, editors, Proc. of the IFIP 13th World Computer Congress 1994, Volume I: Technology and Foundations, pages 396–401. Elsevier Science Publishers B. V., 1994.
Egon Börger and Uwe Glässer. A formal specification of the PVM architecture. In B. Pehrson and I. Simon, editors, Proc. of the IFIP 13th World Computer Congress 1994, Volume I: Technology and Foundations, pages 402–409. Elsevier Science Publishers B. V., 1994.
Manfred Broy, Frank Dederichs, Claus Dendorfer, Max Fuchs, Thomas F. Gritzner, and Rainer Weber. The design of distributed systems — an introduction to FOCUS. Technical Report TUM-19202-2 (SFB-Bericht Nr. 342/2-2/92/A), Institut für Informatik, Technische Universität München, January 1993.
Igor đurđanović and Uwe Glässer. An evolving algebra abstract machine. FB Mathematik & Informatik, Universität-GH Paderborn, Report, May 1995.
George Grätzer. Universal Algebra. Van Nostrand, 1968.
Yuri Gurevich. Evolving algebras — a tutorial introduction. Bulletin of the EATCS, (43):264–284, February 1991.
Yuri Gurevich. Evolving Algebra 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.
Yuri Gurevich, Jim Huggins, and Raghu Mani. The generalized railroad crossing problem: An evolving algebra based solution. CSE Technical Report CSE-TR-230-95, EECS Department, University of Michigan-Ann Arbor, 1995.
D. Harel and A. Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, pages 477–498. Springer-Verlag, 1985.
Gerald J. Holzman. The theory and practice of a formal method: NewCoRe. In B. Pehrson and I. Simon, editors, Proc. of the IFIP 13th World Computer Congress 1994, Volume I: Technology and Foundations, pages 35–44. Elsevier Science Publishers B. V., 1994.
Jim Huggins. Kermit: Specification and verification. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.
The Institute of Electrical and Electronics Engineering. IEEE Standard VHDL Language Reference Manual—IEEE Std 1076-1993, New York, NY, USA, 1994. Order Code SH16840.
T. Lindner C. Lewerentz, editor. Formal Development of Reactive Systems, volume 891 of Lecture Notes in Computer Science. Springer-Verlag, 1995.
Franz Pichler, Heinz Schwärtzel, and Roberto Moreno-Diaz. System Science and Systems Technology: From conceptual frameworks to applicable solutions. In Proceedings of the Fourth International Workshop on Computer Aided Systems Technology (Ottawa, Ont., May 16–20), 1994.
A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Current Trends in Concurrency—Overviews and Tutorials, volume 224 of Lecture Notes in Computer Science, pages 510–584. Springer-Verlag, 1986.
Christoph Schaffer and Herbert Prähofer. On requirements for a CAST-tool for complex, reactive system analysis, design and evaluation. In F. Pichler and R. Moreno-Diaz, editors, Computer Aided Systems Theory-EUROCAST'93, volume 763 of Lecture Notes in Computer Science, pages 137–159. Springer-Verlag, 1994.
A. Wayne Wymore, editor. Model-Based Systems Engineering: An Introduction to the Mathematical Theory of System Design, chapter 1. Systems Engineering Series. CRC Press, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Glässer, U. (1996). Systems level specification and modelling of reactive systems: Concepts, methods, and tools. In: Pichler, F., Díaz, R.M., Albrecht, R. (eds) Computer Aided Systems Theory — EUROCAST '95. EUROCAST 1995. Lecture Notes in Computer Science, vol 1030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0034774
Download citation
DOI: https://doi.org/10.1007/BFb0034774
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60748-9
Online ISBN: 978-3-540-49358-7
eBook Packages: Springer Book Archive