Advertisement

A Practice-Oriented Course on the Principles of Computation, Programming, and System Design and Analysis

  • Egon Börger
Conference paper
  • 275 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)

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.

Keywords

Virtual Machine Turing Machine Recursive Function Business Process Execution Language Abstract State Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  3. 3.
    Anlauff, M., Kutter, P.: Xasm Open Source. Web pages (2001), at http://www.xasm.org/
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)zbMATHCrossRefGoogle Scholar
  7. 7.
    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)zbMATHCrossRefGoogle Scholar
  8. 8.
    Blass, A., Gurevich, Y.: Abstract State Machines capture parallel algorithms. ACM Trans. Computational Logic (2002)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Börger, E.: The ASM refinement method. Formal Aspects of Computing 15, 237–257 (2003)zbMATHCrossRefGoogle Scholar
  13. 13.
    Börger, E.: Teaching ASMs to practice-oriented students. In: Teaching Formal Methods Workshop, pp. 5–12. Oxford Brookes University (2003)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Börger, E., Durdanović, I.: Correctness of compiling Occam to Transputer code. Computer Journal 39(1), 52–92 (1996)CrossRefGoogle Scholar
  21. 21.
    Börger, E., Fruja, G., Gervasi, V., Stärk, R.: A high-level modular definition of the semantics of C#. Theoretical Computer Science (2004)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
    Börger, E., Rosenzweig, D.: A mathematical definition of full Prolog. Science of Computer Programming 24, 249–286 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    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)Google Scholar
  28. 28.
    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)Google Scholar
  29. 29.
    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)CrossRefGoogle Scholar
  30. 30.
    Börger, E., Stärk, R.F.: Abstract State Machines. In: A Method for High-Level System Design and Analysis, Springer, Heidelberg (2003)Google Scholar
  31. 31.
    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)CrossRefGoogle Scholar
  32. 32.
    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)Google Scholar
  33. 33.
    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)Google Scholar
  34. 34.
    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)Google Scholar
  35. 35.
    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)CrossRefGoogle Scholar
  36. 36.
    Dold, A.: A formal representation of Abstract State Machines using PVS. Verifix Technical Report Ulm/6.2, Universität Ulm, Germany (July 1998)Google Scholar
  37. 37.
    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)Google Scholar
  38. 38.
    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)Google Scholar
  39. 39.
    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)CrossRefGoogle Scholar
  40. 40.
    Foundations of Software Engineering Group, Microsoft Research. AsmL (2001), pages at http://research.microsoft.com/foundations/AsmL/
  41. 41.
    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)CrossRefGoogle Scholar
  42. 42.
    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)CrossRefGoogle Scholar
  43. 43.
    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)CrossRefGoogle Scholar
  44. 44.
    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)CrossRefGoogle Scholar
  45. 45.
    Glässer, U., Gotzhein, R., Prinz, A.: Formal semantics of SDL-2000: Status perspectives. Computer Networks 42(3), 343–358 (2003)zbMATHCrossRefGoogle Scholar
  46. 46.
    Gurevich, Y.: Sequential Abstract State Machines capture sequential algorithms. ACM Trans. Computational Logic 1(1), 77–111 (2000)CrossRefMathSciNetGoogle Scholar
  47. 47.
    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)Google Scholar
  48. 48.
    Heitmeyer, C.: Software cost reduction. In: Marciniak, J.J. (ed.) Enc. of Software Engineering, 2nd edn. (2002)Google Scholar
  49. 49.
    ITU-T. SDL formal semantics definition. ITU-T Recommendation Z.100 Annex F, International Telecommunication Union (November 2000) Google Scholar
  50. 50.
    Johnson, D.E., Moss, L.S.: Grammar formalisms viewed as Evolving Algebras. Linguistics and Philosophy 17, 537–560 (1994)CrossRefGoogle Scholar
  51. 51.
    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)CrossRefGoogle Scholar
  52. 52.
    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)CrossRefGoogle Scholar
  53. 53.
    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)CrossRefGoogle Scholar
  54. 54.
    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)Google Scholar
  55. 55.
    Reisig, W.: On Gurevich’s theorem on sequential algorithms. Acta Informatica 39(5), 273–305 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  56. 56.
    Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM case study. J. Universal Computer Science 3(4), 377–413 (1997)zbMATHMathSciNetGoogle Scholar
  57. 57.
    Schmid, J.: Executing ASM specifications with AsmGofer. Web, pages at http://www.tydo.de/AsmGofer
  58. 58.
    Schmid, J.: Refinement and Implementation Techniques for Abstract State Machines. PhD thesis, University of Ulm, Germany (2002)Google Scholar
  59. 59.
    Scott, D.: Definitional suggestions for automata theory. J. Computer and System Sciences 1, 187–212 (1967)zbMATHCrossRefGoogle Scholar
  60. 60.
    Stärk, R.F.: Formal verification of the C# thread model. Department of Computer Science, ETH Zürich (2004)Google Scholar
  61. 61.
    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)CrossRefGoogle Scholar
  62. 62.
    Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  63. 63.
    Teich, J.: Project Buildabong at University of Paderborn (2001), http://www-date.upb.de/RESEARCH/BUILDABONG/buildabong.html
  64. 64.
    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)CrossRefGoogle Scholar
  65. 65.
    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)Google Scholar
  66. 66.
    Wegner, P.: Why interaction is more powerful than algorithms. Commun. ACM 40, 80–91 (1997)CrossRefGoogle Scholar
  67. 67.
    Winter, K.: Model checking for Abstract State Machines. J. Universal Computer Science 3(5), 689–701 (1997)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Egon Börger
    • 1
  1. 1.Dipartimento di InformaticaUniversità di PisaPisaItaly

Personalised recommendations