Abstract
We explain why for the verified software challenge proposed in Hoare (J ACM 50(1): 63–69, 2003), Hoare and Misra (Verified software: theories, tools, experiments. Vision of a Grand Challenge project. In: [Meyer05]) to gain practical impact, one needs to include rigorous definitions and analysis, prior to code development and comprising both experimental validation and mathematical verification, of ground models, i.e., blueprints that describe the required application-content of programs. This implies the need to link via successive refinements the relevant properties of such high-level models in a traceable and checkable way to code a compiler can verify. We outline the Abstract State Machines (ASM) method, a discipline for reliable system development which allows one to bridge the gap between informal requirements and executable code by combining application-centric experimentally validatable system modelling with mathematically verifiable stepwise detailing of abstract models to compile-time-verifiable code.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Altenhofen M, Börger E, Friesen A, Lemcke J (2006) A high-level specification for virtual providers. Int J Bus Process Integration Management 4(1)
Artho C, Barringer H, Goldberg A, Havelund K, Khurshid S, Lowry M, Pasareanu C, Rosu G, Sen K, Visser W, Wahington R (2005) Combining test case generation and runtime verification. Theoret Comput Sci 336(2–3):209–234
Abrial J-R, Börger E, Langmaack H (1996) The steam boiler case study: competition of formal program specification and development methods. In: Abrial J-R, Börger E, Langmaack H (eds) Formal methods for industrial applications. Specifying and programming the steam-boiler control, Vol. 1165 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 1–12
Abrial J-R On constructing large computerized systems (a position paper). In [Meyer05]
Abrial J-R (1996) The B-book. Cambridge University Press, Cambridge
Abrial J-R (2003) Event based sequential program development: application to constructing a pointer program. In: Proceedings of FME 2003. pp 51–74. Springer, Berlin Heidelberg New York
Abrial J-R (2004) Event driven distributed program construction, Version 6
Anlauff M, Kutter P (2001) Xasm Open Source. http://www.xasm.org/
Alur R Trends and challenges in algorithmic software verification. In [Meyer05]
Ball T The verified software challenge: a call for a holistic approach to reliability. In [Meyer05]
Barnocchi D (1971) L’‘Evidenza’ nell’assiomatica aristotelica (contributo all’interpretazione dell’assiomatica aristotelica alla luce della moderna logica matematica). Proteus 5:133–144
Barros A, Börger E (2005) A compositional framework for service interaction patterns and communication flows. In: Lau K-K, Banach R (eds), Formal methods and software engineering. Proceedings of 7th international conference on formal engineering methods (ICFEM 2005), Vol. 3785 of LNCS, pp 5–35. Springer, Berlin Heidelberg New York
Beierle C, Börger E, Durdanović I, Glässer U, Riccobene E (1996) Refining abstract machine specifications of the steam boiler control to well documented executable code. In: Abrial J-R, Börger E, Langmaack H (eds) Formal methods for industrial applications. Specifying and programming the steam-boiler control, number 1165 in LNCS, pp 62–78. Springer, Berlin Heidelberg New York
Börger E, Dässler K (1990) Prolog: DIN papers for discussion. ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory, Middlesex
Börger E, Durdanović I (1996) Correctness of compiling Occam to Transputer code. Comput J 39(1):52–92
Berry DM (1995) The importance of ignorance in requirements engineering. J Syst Softw 28(2):179–184
Börger E, Fruja G, Gervasi V, Stärk R (2005) A high-level modular definition of the semantics of C#. Theoret Comput Sci 336(2–3):235–284
Betarte G, Gimenez E, Loiseaux C, Chetali B (2002) Formavie: formal modelling and verification of the java card 2.1.1 security architecture. In: Proc. eSmart
Börger E, Glässer U, Müller W (1994) The semantics of behavioral VHDL’93 descriptions. In: EURO-DAC’94. european design automation conference with EURO-VHDL’94. Los Alamitos, California IEEE Computer Society Press, pp 500–505
Börger E, Gargantini A, Riccobene E (2006) Abstract state machines. A method for system specification and analysis. In: Frappier M, Habrias H (eds) Software specification methods: an overview using a case study. HERMES Sc Publ, pp 103–119
Börger E, Mazzanti S (1997) A practical method for rigorously controllable hardware design. In: Bowen JP, Hinchey MB, Till D (eds) ZUM’97: the Z formal specification notation, Vol. 1212 of LNCS. Springer, Heidelberg New York, pp 151– 187
Börger E, Mearelli L (1997) Integrating ASMs into the software development life cycle. J Universal Comput Sci 3(5):603–665
Börger E Linking content definition and analysis to what the compiler can verify. In: [Meyer05]
Börger E (1990) A logical operational semantics for full Prolog. Part I: selection core and control. In: Börger E, Kleine Büning H, Richter MM, Schönfeld W (eds) CSL’89. 3rd workshop on computer science logic, Vol. 440 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 36–64
Börger E (1990) A logical operational semantics of full Prolog. Part II: built-in predicates for database manipulation. In: Rovan B (ed) Mathematical foundations of computer science, Vol. 452 of LNCS. Springer, Berlin Heidelberg New York, pp 1–14
Börger E (1994) Logic programming: the evolving algebra approach. In: Pehrson B, Simon I (eds) IFIP 13th world computer congress, Vol I: Technology/foundations. Elsevier, Amsterdam, pp 39–395
Börger E (1995) Why use evolving algebras for hardware and software engineering? In: Bartosek M, Staudek J, Wiederman J, (eds) Proceedings of SOFSEM’95, 22nd seminar on current trends in theory and practice of informatics, Vol. 1012 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 236–271
Börger E (1999) High-level system design and analysis using Abstract State Machines. In: Hutter D, Stephan W, Traverso P, Ullmann M (eds), Current trends in applied formal methods (FM-Trends 98), Vol. 1641 of LNCS. Springer, Berlin Heidelberg New York, pp 1–43
Börger E (2002) The origins and the development of the ASM method for high-level system design and analysis. J Universal Comput Sci 8(1):2–74
Börger E (2003) The ASM ground model method as a foundation of requirements engineering. In: Dershowitz N (ed) Verification: theory and practice, Vol. 2772 of LNCS. Springer, Berlin Heidelberg New york, pp 145–160
Börger E (2003) The ASM refinement method. Formal Aspects Computing 15:237–257
Börger E (2005) The ASM method for system design and analysis. A tutorial introduction. In: Gramlich B (ed) Proceedings of FroCoS, Vol. 3717 of LNAI, Vienna. Springer, Berlin Heidelberg New York
Börger E (2006) 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. Forschungsinst. für Mathematikdidaktik Osnabrück. ISBN 3-925386-56-4
Börger E, Päppinghaus P, Schmid J (2000) Report on a practical application of ASMs in software design. In: Gurevich Y, Kutter P, Odersky M, Thiele L (eds) Abstract State Machines: theory and applications, Vol. 1912 of LNCS. Springer, Berllin Heidelberg New York, pp 361–366
Börger E, Rosenzweig D (1995) The WAM—definition and compiler correctness. In: Beierle C, Plümer L (eds) Logic programming: formal methods and practical applications, Vol. 11 of studies in computer science and artificial intelligence, chap 2. North-Holland, Amsterdam
Brooks FP Jr (1987) No silver bullet. Computer 20(4):10–19
Börger E, Stärk RF (2003) Abstract State Machines A method for high-level system design and analysis. Springer, Berlin Heidelberg New York
Börger E, Stärk RF (2004) Exploiting abstraction for specification reuse. The Java/C# case study. In: Bonsangue M (ed.) Formal methods for components and objects: 2nd international symposium (FMCO 2003 Leiden), Vol. 3188 of LNCS, pp 42–76. Springer, Berlin Heidelberg New York
Carnap R (1956) The methodological character of theoretical concepts. In: Feigl H, Scriven M (eds), Minnesota studies in the philosophy of science, Vol. 2. University of Minnesota Press, pp 33–76
Del Castillo G (2001) The ASM workbench. A tool environment for computer-aided analysis and validation of abstract state machine models. PhD Thesis, Universität Paderborn
Dold A, Gaul T, Vialard V, Zimmermann W (1998) ASM-based mechanized verification of compiler back-ends. In: Glässer U, Schmitt P (eds) Proceedings of 5th International Workshop on ASMs. Magdeburg University, pp 50–67
Dijkstra EW (1972) Notes on structured programming. In: Dahl O-J, Dijkstra EW, Hoare CAR (eds), Structured Programming, pp 1–82. Academic, New York
de Moura L, Owre S, Ruess H, Rushby J, Shankar N Integrating verification components. In [Meyer05]
Dold A (1998) A formal representation of Abstract State Machines using PVS. Verifix Technical Report Ulm/6.2, Universität Ulm
Del Castillo G, Winter K (2000) Model checking support for the ASM high-level language. In: Graf S, Schwartzbach M (eds) Proceedings of 6th Internatonal Conference TACAS 2000, Vol. 1785 of LNCS. Springer, Berlin Heidelberg New York, pp 331–346
Farahbod R et al. The CoreASM project. http://www.coreasm.org
Fruja NG, Börger E (2005) Analysis of the .NET CLR exception handling. In: Skala V, Nienaltowski P (eds) 3rd international conference on .NET technologies, .NET 2005, Pilsen, pp 65–75
Fruja NG, Börger E (2006) Modeling the .NET CLR exception handling mechanism for a mathematical analysis. J Object Technology 5(3):5–34
Frappier M, Habrias H (2006) Software specification methods: an overview using a case study. HERMES Science Publishing
Foundations of Software Engineering Group, Microsoft Research (2001) AsmL. Web pages at http://research.microsoft.com/foundations/AsmL/
Goerigk W, Dold A, Gaul T, Goos G, Heberle A, von Henke FW, Hoffmann U, Langmaack H, Pfeifer H, Ruess H, Zimmermann W (1996) Compiler correctness and implementation verification: the verifix approach. In: Fritzson P (ed) on compiler construction, proceedings poster session of CC’96, Linköping, Sweden IDA Technical Report LiTH-IDA-R-96-12
Glässer U, Gotzhein R, Prinz A (2003) Formal semantics of sdl-2000: status and perspectives. Comput Netw 42(3):343–358
Gargantini A, Riccobene E (2000) Encoding Abstract State Machines in PVS. In: Gurevich Y, Kutter P, Odersky M, Thiele L (eds) Abstract State Machines: theory and applications, Vol. 1912 of LNCS, pp 303–322. Springer, Berlin Heidelberg New York
Gawanmeh A, Tahar S, Winter K (2003) Interfacing ASMs with the MDG tool. In: Börger E, Gargantini A, Riccobene E (eds), Abstract State Machines 2003–advances in theory and applications, Vol. 2589 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 278–292
Gurevich Y (1991) Evolving algebras. A tutorial introduction. Bull EATCS 43:264–284
Habibi A (2005) Framework for system level verification: the systemC case. PhD Thesis, Concordia University
Hall A (1990) Seven myths of formal methods. IEEE Softw 11–19
Hall JA (1997) Taking Z seriously. In: ZUM’97, Vol. 1212 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 89–91
Heimdahl MPE Let’s not forget validation. In [Meyer05]
Heitmeyer C (1999) Using SCR methods to capture, document, and verify computer system requirements. In: Börger E, Hörger B, Parnas DL, Rombach D (eds) Requirements capture, documentation, and validation. Dagstuhl seminar no. 99241, Schloss Dagstuhl
Havelund K, Goldberg A Verify your runs. In: [Meyer05]
Holzmann GJ, Joshi R Reliable software systems design: Defect prevention, detection, and containment. In: [Meyer05]
Hoare T, Misra J Verified software: theories, tools, experiments. Vision of a Grand Challenge project. In: [Meyer05]
Haeberer AM, Maibaum TSE (2001) Scientific rigour, an answer to a pragmatic question: a linguistic framework for software engineering. Number 21 in Proceedings of international conference on software engineering (ICSE 21), Toronto. IEEE CS Press, pp 463–472
Harel D, Marelly R (2001) Capturing and executing behavioral requirements: the play-in/play-out approach. Technical report MCS01-15, Weizmann Institute of Science, Israel
Haeberer AM, Maibaum TSE, Cengarle MV (2001) Knowing what requirements specifications specify. Typoscript
Hoare CAR (2003) The verifying compiler: a grand challenge for computing research. J ACM 50(1):63–69
Rushby J Automated test generation and verified software. In: [Meyer05]
Kalinov A, Kossatchev A, Petrenko A, Posypkin M, Shishkov V (2003) Using ASM specifications for compiler testing. In: Börger E, Gargantini A, Riccobene E (eds) Abstract State Machines 2003–advances in theory and applications, Vol. 2589 of LNCS. Springer, Berlin Heidelberg New York, p 415
Klein G, Nipkow T (2006) A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans Program Lang Syst
Leroy X (2006) Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In: Proceedings of POPL’06. ACM
Leveson NG (2000) Completeness in formal specification language design for process-control systems. In: Formal methods in software practice, pages 75–87. ACM Press
Methodologies and technologies for industrial strength systems engineering. http://www.matisse.qinetiq.com/, 1999. Project number IST-1999-11435
Strother Moore J A mechanized program verifier. In [Meyer05]
Moore JS (2003) Proving theorems about Java and the JVM with ACL2. In: Broy M, Pizka M (eds) Models, Algebras and Logic of Engineering Software, Vol. 191. IOS Press
Meyer B (2005) Proceedings of IFIP WG conference on verified software: tools, techniques, and experiments, ETH, Zürich, October. http://vstte.ethz.ch/papers.html
Naur P (1985) Programming as theory building. Microprocess Microprogram 15:253–261
Nanchen S, Stärk RF (2003) A security logic for Abstract State Machines. In: TR 423 CS Dept ETH Zürich
Parnas DL (2006) The use of precise documentation in software develpment. Tutorial at FM 2006, see http://fm06.mcmaster.ca/t8.htm
Popper KR, Eccles JC (1977) The self and its brain. Routledge and Kegan Paul, London
Popper KR (1935) Logik der Forschung. Zur Erkenntnistheorie der modernen Naturwissenschaft. (Engl. Translation: The Logic of Scientific Discovery, Hutchinson 1959, Routledge 1992 and 2002), Wien
Glässer U, Farahbod R, Vajihollahi M (2006) An abstract machine architecture for Web service based business process management. Int J Bus Process Integration Manage
Glass RL (2003) Facts and Fallacies of Software Engineering. Addison-Wesley, Reading
Ryle R (1963) The concept of mind. Penguin Books, Harmondworth
Schellhorn G, Ahrendt W (1997) Reasoning about Abstract State Machines: the WAM case study. J Universal Computer Science, 3(4):377–413
Stärk RF, Börger E (2004) An ASM specification of C# threads and the. NET memory model. In: Zimmermann W, Thalheim B (eds) Abstract State Machines 2004, Vol. 3052 of LNCS, pp 38–60. Springer, Berlin Heidelberg New York
Schmid J Executing ASM specifications with AsmGofer. Web pages at http://www.tydo.de/AsmGofer
Schürmann C Meta-logical frameworks and formal digital libraries. In: [Meyer05]
Schellhorn G (2001) Verification of ASM refinements using generalized forward simulation. J Universal Comput Sci 7(11):952–979
Schmid J (2001) Compiling Abstract State Machines to C++. J Universal Comput Sci 7(11):1069–1088
Schmid J (2002) Refinement and implementation techniques for Abstract State Machines. PhD Thesis, University of Ulm
Schellhorn G (2005) ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theoret Comput Sci 336(2-3):403–436
Semiconductor Industry Assoc (2005) International technologoy roadmap for semiconductors. Design. http://www.itrs.net/ Common/2005ITRS/Design2005.pdf
Strichmann O, Godlin B Regression verification–a practical way to verify programs. In [Meyer05]
Smith DR Generating programs plus proofs by refinement. In [Meyer05]
Stärk RF, Nanchen S (2001) A logic for Abstract State Machines. J Universal Comput Sci 7(11):981–1006
Stärk RF, Schmid J, Börger E (2001) Java and the Java Virtual Machine: definition, verification, validation. Springer, Berlin Heidelberg New York
Teich J, Kutter P, Weper R (2000) Description and simulation of microprocessor instruction sets using ASMs. In: Gurevich Y, Kutter P, Odersky M, Thiele L (eds) Abstract State Machines: theory and applications, Vol. 1912 of Lecture Notes in Computer Science, pp 266–286. Springer, Berlin Heidelberg New York
Teich J, Weper R, Fischer D, Trinkert S (2000) A joint architecture/compiler design environment for ASIPs. In: Proceedings of the international conference on compilers, architectures and synthesis for embedded systems (CASES2000), pp 26–33, San Jose, CA, ACM Press
Utting M Model-based testing. In [Meyer05]
Wing JM (1990) A specifier’s introduction to formal methods. Computer, 8–24
Winter K (1997) Model checking for Abstract State Machines. J Universal Computer Science 3(5):689–701
Wirth N (1971) Program development by stepwise refinement. Comm. ACM 14(4)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Börger, E. Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems. Form Asp Comp 19, 225–241 (2007). https://doi.org/10.1007/s00165-006-0019-y
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-006-0019-y