Design exploration and experimental validation of abstract requirements

How can one cope with the notorious problem of establishing the correctness and completeness of abstract functional requirements in the design of control-intensive software systems prior to actually building the system? The answer given here explores the abstract state machine (ASM) paradigm: a versatile semantic framework for computational modeling of virtually all kinds of discrete dynamic systems. Combining common abstraction principles from computational logic and discrete mathematics, abstract state machines provide a universal model of computation and an effective instrument for analyzing and reasoning about complex semantic properties of real-world systems. In this paper we introduce a novel ASM tool environment for making ASM ground models executable on real machines. We present the CoreASM language and the general architecture of the CoreASM engine together with a high-level description of its extensibility mechanisms.