Executable formal specifications of complex distributed systems with CoreASM

Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be. With increasing complexity of software-intensive computer-based systems and the challenges of validation and verification of abstract software models prior to coding, the need for interactive software tools supporting executable formal specifications is even more evident. In this paper, we discuss how CoreASM, an environment for writing and running executable specifications according to the ASM method, provides flexibility and manages the complexity by using an innovative extensible language architecture.

► We present CoreASM, a toolset for the design and analysis of high-level system models. ► The toolset supports authoring, running, and validation of formal specifications. ► Its novel extensible architecture allows extension of the language and interpreter. ►CoreASM has been deployed extensively in various scientific and industrial projects.