Abstract
We propose a simple foundation for a practice-oriented undergraduate course that links seamlessly computation theory to principles and methods for high-level computer-based system development and analysis. Starting from the fundamental notion of virtual machine computations, which is phrased for both synchronous and asynchronous systems in terms of Abstract State Machines, the course covers in a uniform way the basics of algorithms (sequential and distributed computations) and formal languages (grammars and automata) as well as the computational content of the major programming paradigms and high-level system design principles. The course constitutes a basis for advanced courses on algorithms and their complexity as well as on rigorous methods for requirements capture and for practical hardware/software design and analysis.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abiteboul, S., Vianu, V., Fordham, B., Yesha, Y.: Relational transducers for electronic commerce. In: Proc. 17th ACM Sympos. Principles of Database Systems (PODS 1998), pp. 179–187. ACM Press, New York (1998)
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Anlauff, M., Kutter, P.: Xasm Open Source. Web pages (2001), at http://www.xasm.org/
Barnett, M., Börger, E., Gurevich, Y., Schulte, W., Veanes, M.: Using Abstract State Machines at Microsoft: A case study. In: Gurevich, Y., Kutter, P., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 367–380. Springer, Heidelberg (2000)
Barnett, M., Schulte, W.: Contracts, components and their runtime verification on the .NET platform. J. Systems and Software, Special Issue on Component-Based Software Engineering (2002) (to appear)
Beierle, C., Börger, E.: Refinement of a typed WAM extension by polymorphic order-sorted types. Formal Aspects of Computing 8(5), 539–564 (1996)
Beierle, C., Börger, E.: Specification and correctness proof of a WAM extension with abstract type constraints. Formal Aspects of Computing 8(4), 428–462 (1996)
Blass, A., Gurevich, Y.: Abstract State Machines capture parallel algorithms. ACM Trans. Computational Logic (2002)
Börger, E.: Computability, Complexity, Logic (English translation of ”Berechenbarkeit, Komplexität, Logik”). Studies in Logic and the Foundations of Mathematics, vol. 128. North-Holland, Amsterdam (1989)
Börger, E.: High-level system design and analysis using Abstract State Machines. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 1–43. Springer, Heidelberg (1999)
Börger, E.: The ASM ground model method as a foundation of requirements engineering. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 145–160. Springer, Heidelberg (2004)
Börger, E.: The ASM refinement method. Formal Aspects of Computing 15, 237–257 (2003)
Börger, E.: Teaching ASMs to practice-oriented students. In: Teaching Formal Methods Workshop, pp. 5–12. Oxford Brookes University (2003)
Börger, E.: Linking architectural and component level system views by abstract state machines. In: Grimm, C. (ed.) Languages for System Specification and Verification, CHDL, pp. 247–269. Kluwer, Dordrecht (2004)
Börger, E.: Modeling with Abstract State Machines: A support for accurate system design and analysis. In: Rumpe, B., Hesse, W. (eds.) Modellierung 2004. GI-Edition Lecture Notes in Informatics, vol. P-45, pp. 235–239. Springer, Heidelberg (2004)
Börger, E.: Abstract State Machines: A unifying view of models of computation and of system design frameworks. Annals of Pure and Applied Logic (2004) (to appear)
Börger, E., Bolognesi, T.: Remarks on turbo ASMs for computing functional equations and recursion schemes. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 218–228. Springer, Heidelberg (2003)
Börger, E., Busch, H., Cuellar, J., Päppinghaus, P., Tiden, E., Wildgruber, I.: Konzept einer hierarchischen Erweiterung von EURIS. Siemens ZFE T SE 1 Internal Report BBCPTW91-1, pp. 1–43 (Summer 1996)
Börger, E., Dässler, K.: Prolog: DIN papers for discussion. ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory, Middlesex, England (1990)
Börger, E., Durdanović, I.: Correctness of compiling Occam to Transputer code. Computer Journal 39(1), 52–92 (1996)
Börger, E., Fruja, G., Gervasi, V., Stärk, R.: A high-level modular definition of the semantics of C#. Theoretical Computer Science (2004)
Börger, E., Glässer, U., Müller, W.: The semantics of behavioral VHDL 1993 descriptions. In: EURO-DAC 1994. European Design Automation Conference with EURO-VHDL 1994, pp. 500–505. IEEE Computer Society Press, Los Alamitos (1994)
Börger, E., López-Fraguas, F.J., Rodríguez-Artalejo, M.: A model for mathematical analysis of functional logic programs and their implementations. In: Pehrson, B., Simon, I. (eds.) IFIP 13th World Computer Congress. Technology/Foundations, vol. I, pp. 410–415. Elsevier, Amsterdam (1994)
Börger, E., Mazzanti, S.: A practical method for rigorously controllable hardware design. In: Bowen, J.P., Hinchey, M.B., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 151–187. Springer, Heidelberg (1997)
Börger, E., Päppinghaus, P., Schmid, J.: Report on a practical application of ASMs in software design. In: Gurevich, Y., Kutter, P., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 361–366. Springer, Heidelberg (2000)
Börger, E., Rosenzweig, D.: A mathematical definition of full Prolog. Science of Computer Programming 24, 249–286 (1995)
Börger, E., Rosenzweig, D.: The WAM – definition and compiler correctness. In: Beierle, C., Plümer, L. (eds.) Logic Programming: Formal Methods and Practical Applications. ch. 2, Studies in Computer Science and Artificial Intelligence, vol. 11, pp. 20–90. North-Holland, Amsterdam (1995)
Börger, E., Salamone, R.: CLAM specification for provably correct compilation of CLP(R) programs. In: Börger, E. (ed.) Specification and Validation Methods, pp. 97–130. Oxford University Press, Oxford (1995)
Börger, E., Schmid, J.: Composition and submachine concepts for sequential ASMs. In: Clote, P., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 41–60. Springer, Heidelberg (2000)
Börger, E., Stärk, R.F.: Abstract State Machines. In: A Method for High-Level System Design and Analysis, Springer, Heidelberg (2003)
Börger, E., Stärk, R.F.: Exploiting abstraction for specification reuse. The Java/C# case study. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 42–76. Springer, Heidelberg (2004)
Burgard, W., Cremers, A.B., Fox, D., Heidelbach, M., Kappel, A.M., Lüttringhaus-Kappel, S.: Knowledge-enhanced CO-monitoring in coal mines. In: Proc. Int. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA-AIE), Fukuoka, Japan, June 4-7, pp. 511–521 (1996)
Castillo, G.D., Päppinghaus, P.: Designing software for internet telephony: experiences in an industrial development process. In: Blass, A., Börger, E., Gurevich, Y. (eds.) Theory and Applications of Abstract State Machines, Schloss Dagstuhl, Int. Conf. and Research Center for Computer Science (2002)
Burgard, W., Cremers, A.B., Fox, D., Heidelbach, M., Kappel, A.M., Lüttringhaus-Kappel, S.: Knowledge-enhanced CO-monitoring in coal mines. In: Proc. Int. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA-AIE), Fukuoka, Japan, June 4-7, pp. 511–521 (1996)
Del Castillo, G., Winter, K.: Model checking support for the ASM high-language. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 331–346. Springer, Heidelberg (2000)
Dold, A.: A formal representation of Abstract State Machines using PVS. Verifix Technical Report Ulm/6.2, Universität Ulm, Germany (July 1998)
Dold, A., Gaul, T., Vialard, V., Zimmermann, W.: ASM-based mechanized verification of compiler back-ends. In: Glässer, U., Schmitt, P. (eds.) Proc. Int. Workshop on Abstract State Machines, pp. 50–67. Magdeburg University (1998)
Fahland, D.: Ein Ansatz einer Formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines. Master’s thesis, Humboldt-Universität zu Berlin (June 2004)
Farahbod, R., Glässer, U., Vajihollahi, M.: Specification and validation of business process execution language for web services. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 78–94. Springer, Heidelberg (2004)
Foundations of Software Engineering Group, Microsoft Research. AsmL (2001), pages at http://research.microsoft.com/foundations/AsmL/
Fruja, N.G., Stärk, R.F.: The hidden computation steps of turbo Abstract State Machines. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 244–262. Springer, Heidelberg (2003)
Gargantini, A., Riccobene, E.: Encoding Abstract State Machines in PVS. In: Gurevich, Y., Kutter, P., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 303–322. Springer, Heidelberg (2000)
Gargantini, A., Riccobene, E.: Using Spin to generate tests from ASM specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263–277. Springer, Heidelberg (2003)
Gawanmeh, A., Tahar, S., Winter, K.: Interfacing ASMs with the MDG tool. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 278–292. Springer, Heidelberg (2003)
Glässer, U., Gotzhein, R., Prinz, A.: Formal semantics of SDL-2000: Status perspectives. Computer Networks 42(3), 343–358 (2003)
Gurevich, Y.: Sequential Abstract State Machines capture sequential algorithms. ACM Trans. Computational Logic 1(1), 77–111 (2000)
Heitmeyer, C.: Using SCR methods to capture, document, and verify computer system requirements. In: Börger, E., Hörger, B., Parnas, D.L., Rombach, D. (eds.) Requirements Capture, Documentation, and Validation. Dagstuhl Seminar No. 99241, Schloss Dagstuhl, Int. Conf. and Research Center for Computer Science (1999)
Heitmeyer, C.: Software cost reduction. In: Marciniak, J.J. (ed.) Enc. of Software Engineering, 2nd edn. (2002)
ITU-T. SDL formal semantics definition. ITU-T Recommendation Z.100 Annex F, International Telecommunication Union (November 2000)
Johnson, D.E., Moss, L.S.: Grammar formalisms viewed as Evolving Algebras. Linguistics and Philosophy 17, 537–560 (1994)
Kalinov, A., Kossatchev, A., Petrenko, A., Posypkin, M., Shishkov, V.: Using ASM specifications for compiler testing. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, p. 415. Springer, Heidelberg (2003)
Kutter, P., Schweizer, D., Thiele, L.: Integrating domain specific language design in the software life cycle. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 196–212. Springer, Heidelberg (1998)
Langmaack, H.: An ALGLO-view on TURBO ASM. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 20–37. Springer, Heidelberg (2004)
Mueller, W., Ruf, J., Rosenstiel, W.: An ASM-based semantics of systemC simulation. In: Mueller, W., Ruf, J., Rosenstiel, W. (eds.) SystemC - Methodologies and Applications, pp. 97–126. Kluwer Academic Publishers, Dordrecht (2003)
Reisig, W.: On Gurevich’s theorem on sequential algorithms. Acta Informatica 39(5), 273–305 (2003)
Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM case study. J. Universal Computer Science 3(4), 377–413 (1997)
Schmid, J.: Executing ASM specifications with AsmGofer. Web, pages at http://www.tydo.de/AsmGofer
Schmid, J.: Refinement and Implementation Techniques for Abstract State Machines. PhD thesis, University of Ulm, Germany (2002)
Scott, D.: Definitional suggestions for automata theory. J. Computer and System Sciences 1, 187–212 (1967)
Stärk, R.F.: Formal verification of the C# thread model. Department of Computer Science, ETH Zürich (2004)
Stärk, R.F., Börger, E.: An ASM specification of C# threads and the.NET memory model. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 38–60. Springer, Heidelberg (2004)
Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)
Teich, J.: Project Buildabong at University of Paderborn (2001), http://www-date.upb.de/RESEARCH/BUILDABONG/buildabong.html
Teich, J., Weper, R., Fischer, D., Trinkert, S.: A joint architecture/compiler design environment for ASIPs. In: Proc. Int. Conf. on Compilers, Architectures and Synthesis for Embedded Systems (CASES2000), San Jose, CA, USA, November 2000, pp. 26–33. ACM Press, New York (2000)
Vajihollahi, M.: High level specification and validation of the business process execution language for web services. Master’s thesis, School of Computing Science at Simon Fraser University (March 2004)
Wegner, P.: Why interaction is more powerful than algorithms. Commun. ACM 40, 80–91 (1997)
Winter, K.: Model checking for Abstract State Machines. J. Universal Computer Science 3(5), 689–701 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Börger, E. (2004). A Practice-Oriented Course on the Principles of Computation, Programming, and System Design and Analysis. In: Dean, C.N., Boute, R.T. (eds) Teaching Formal Methods. TFM 2004. Lecture Notes in Computer Science, vol 3294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30472-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-30472-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23611-5
Online ISBN: 978-3-540-30472-2
eBook Packages: Springer Book Archive