Abstract
We formulate some research and development challenges that relate what a verifying compiler can verify to the definition and analysis of the application-content of programs, where the analysis comprises both experimental validation and mathematical verification. We also point to a practical framework to deal with theses challenges, namely the Abstract State Machines (ASM) method for high-level system design and analysis. We explain how it allows one to bridge the gap between informal requirements and detailed code by combining application-centric experimentally validatable system modeling with mathematically verifiable refinements of abstract models to compiler-verifiable code.
Chapter PDF
References
Abrial, J.-R.: Event based sequential program development: application to constructing a pointer program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 51–74. Springer, Heidelberg (2003)
Abrial, J.-R.: Event driven distributed program construction. Version 6 (August 2004)
Abrial, J.-R.: On constructing large computerized systems (a position paper). In: Proc. VSTTE, ETH Zürich (October 2005)
Anlauff, M., Kutter, P.: Xasm Open Source (2001), http://www.xasm.org/
Betarte, G., Gimenez, E., Loiseaux, C., Chetali, B.: Formavie: Formal modelling and verification of the java card 2.1.1 security architecture. In: Proc. eSmart (2002)
Börger, E.: A logical operational semantics for full Prolog. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 36–64. Springer, Heidelberg (1990)
Börger, E.: A logical operational semantics of full Prolog. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol. 452, pp. 1–14. Springer, Heidelberg (1990)
Börger, E.: A logical operational semantics for full Prolog. In: Moschovakis, Y.N. (ed.) Part III: Built-in predicates for files, terms, arithmetic and input-output, Berkeley Mathematical Sciences Research Institute Publications. Logic From Computer Science, vol. 21, pp. 17–50. Springer, Heidelberg (1992)
Börger, E.: Logic programming: The Evolving Algebra approach. In: Pehrson, B., Simon, I. (eds.) IFIP 13th World Computer Congress. Technology/Foundations, vol. I, pp. 391–395. Elsevier, Amsterdam (1994)
Börger, E.: The origins and the development of the ASM method for high-level system design and analysis. J. Universal Computer Science 8(1), 2–74 (2002)
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.: The ASM method for system design and analysis. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, Springer, Heidelberg (2005)
Börger, E.: From Finite State Machines to Virtual Machines (Illustrating design patterns and event-B models). In: Cohors-Fresenborg, E., Schwank, I. (eds.) Präzisionswerkzeug Logik–Gedenkschrift zu Ehren von Dieter Rödding, Forschungsinstitut für Mathematikdidaktik Osnabr(̈2006) ISBN 3-925386-56-4
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 336(2–3), 235–284 (2005)
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., Päppinghaus, P., Schmid, J.: Report on a practical application of ASMs in software design. In: Gurevich, Y., Kutter, P.W., 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. Studies in Computer Science and Artificial Intelligence, vol. 11, ch. 2, pp. 20–90. North-Holland, Amsterdam (1995)
Börger, E., Stärk, R.F.: Abstract State Machines. In: A Method for High-Level System Design and Analysis, Springer, Heidelberg (2003)
Brooks, F.P.J.: No silver bullet. Computer 20(4), 10–19 (1987)
Carnap, R.: The methodological character of theoretical concepts. In: Feigl, H., Scriven, M. (eds.) Minnesota Studies in the Philosophy of Science, vol. 2, pp. 33–76. University of Minnesota Press (1956)
Del Castillo, G.: The ASM Workbench. A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models. PhD thesis, Universität Paderborn, Germany (2001)
Del Castillo, G., Winter, K.: Model checking support for the ASM high-level language. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 331–346. Springer, Heidelberg (2000)
Dijkstra, E.W.: Notes on structured programming. In: Dahl, O.-J., Dijkstra, E.W., Hoare, C.A.R. (eds.) Structured Programming, pp. 1–82. Academic Press, London (1972)
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. 5th Int. Workshop on ASMs, Magdeburg University, pp. 50–67 (1998)
Farahbod, R., et al.: The CoreASM Project, http://www.coreasm.org
Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: An Extensible ASM Execution Engine. Fundamenta Informaticae XXI (2006)
Foundations of Software Engineering Group, Microsoft Research. AsmL (2001), http://research.microsoft.com/foundations/AsmL/
Fruja, N.G.: The Correctness of the Definite Assignment Analysis in C#. J. Object Technology 3(9), 29–52 (2004)
Fruja, N.G.: A Modular Design for the.NET CLR Architecture. In: Beauquier, A.S.D., Börger, E. (eds.) 12th International Workshop on Abstract State Machines, ASM 2005, Paris, France, pp. 175–199 (March 2005)
Fruja, N.G.: Type Safety of Generics for the.NET Common Language Runtime. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 325–341. Springer, Heidelberg (2006)
Fruja, N.G., Börger, E.: Analysis of the.NET CLR Exception Handling. In: Skala, V., Nienaltowski, P. (eds.) 3rd International Conference on .NET Technologies, NET 2005, Pilsen, Czech Republic, pp. 65–75 (May–June 2005)
Fruja, N.G., Börger, E.: Modeling the.NET CLR Exception Handling Mechanism for a Mathematical Analysis. Journal of Object Technology 5(3), 5–34 (2006)
Gargantini, A., Riccobene, E.: Encoding Abstract State Machines in PVS. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 303–322. Springer, Heidelberg (2000)
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 and perspectives. Computer Networks 42(3), 343–358 (2003)
Goerigk, W., Dold, A., Gaul, T., Goos, G., Heberle, A., von Henke, F.W., Hoffmann, U., Langmaack, H., Pfeifer, H., Ruess, H., Zimmermann, W.: Compiler correctness and implementation verification: The verifix approach. In: Fritzson, P. (ed.) Int. Conf. on Compiler Construction, Proc. Poster Session of CC 1996, Linköping, Sweden (1996); IDA Technical Report LiTH-IDA-R-96-12
Habibi, A.: Framework for System Level Verification: The SystemC Case. PhD thesis, Concordia University, Montreal (July 2005)
Haeberer, A.M., Maibaum, T.S.E.: Scientific rigour, an answer to a pragmatic question: a linguistic framework for software engineering. In: International Conference on Software Engineering, Toronto, vol. 23 (2001)
Haeberer, A.M., Maibaum, T.S.E., Cengarle, M.V.: Knowing what requirements specifications specify (typoscript 2001)
Heimdahl, M.P.E.: Let’s not forget validation. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE 2005). LNCS, vol. 4171. Springer, Heidelberg (2008) (this volume)
Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. J. ACM 50(1), 63–69 (2003)
Jones, C.B.: What can we do (technically) to get the right specification. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE 2005). LNCS, vol. 4171, pp. 64–69. Springer, Heidelberg (2008) (this volume)
Jula, H.V., Fruja, N.G.: An Executable Specification of C#. In: Beauquier, A.S.D., Börger, E. (eds.) 12th International Workshop on Abstract State Machines, ASM 2005, Paris, France, pp. 275–287 (March 2005); University Paris 12
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)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Prog. Lang. Syst. (2006)
Nanchen, S., Stärk, R.F.: A security logic for Abstract State Machines. TR 423 CS Dept., ETH Zürich (2003)
Popper, K.: Logik der Forschung. Zur Erkenntnishtoeire der modernen Naturwissenschaft. Wien (1935)
Glass, R.L.: Facts and Fallacies of Software Engineering. Addison-Wesley, Reading (2003)
Schellhorn, G.: Verifikation abstrakter Zustandsmaschinen. PhD thesis, Universität Ulm, Germany (1999)
Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. Universal Computer Science 7(11), 952–979 (2001)
Schellhorn, G.: ASM refinement and generalizations of forward simulation in data refinement: A comparison. Theoretical Computer Science 336(2-3), 403–436 (2005)
Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM case study. J. Universal Computer Science 3(4), 377–413 (1997)
Schellhorn, G., Ahrendt, W.: The WAM case study: Verifying compiler correctness for Prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction – A Basis for Applications, volume III: Applications, pp. 165–194. Kluwer Academic Publishers, Dordrecht (1998)
Schmid, J.: Executing ASM specifications with AsmGofer, http://www.tydo.de/AsmGofer
Schmid, J.: Compiling Abstract State Machines to C++. J. Universal Computer Science 7(11), 1069–1088 (2001)
Schmid, J.: Refinement and Implementation Techniques for Abstract State Machines. PhD thesis, University of Ulm, Germany (2002)
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, Springer, Heidelberg (2004)
Stärk, R.F., Nanchen, S.: A logic for Abstract State Machines. J. Universal Computer Science 7(11), 981–1006 (2001)
Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)
Teich, J., Kutter, P., Weper, R.: Description and simulation of microprocessor instruction sets using ASMs. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 266–286. Springer, Heidelberg (2000)
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 (CASES 2000), November 2000, pp. 26–33. ACM Press, San Jose (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)
Winter, K.: Model checking for Abstract State Machines. J. Universal Computer Science 3(5), 689–701 (1997)
Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4) (1971)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Börger, E. (2008). Linking the Meaning of Programs to What the Compiler Can Verify. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)