Construction and Analysis of Ground Models and their Refinements as a Foundation for Validating Computer Based Systems

Abstract. We explain why for the verified software challenge proposed in [66, 67] to gain practical impact, one needs to include rigorous defini-tions and analysis, prior to code development and comprising both ex-perimental 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 prop-erties 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 mod-elling with mathematically verifiable stepwise detailing of abstract mod-els to compile-time-verifiable code.