CoreASM

CoreASM is an executable language for writing Abstract State Machines - and, just as importantly, an open, plugin-based engine for running them. Its stated goal is unusual among specification tools: rather than defining a convenient programming notation that happens to have formal semantics, CoreASM tries to keep the executable language as close as possible to the mathematical definition of pure ASMs, so that a specification can stay abstract for as long as the modeller wants it to and only becomes concrete where the modeller chooses.

That priority - abstraction first, execution second - is what distinguishes CoreASM from the other ASM tools of its era. Where earlier systems asked you to encode your model into their host language before it would run, CoreASM aims to run the model you actually wrote, leaving intentionally abstract parts marked as such rather than forcing them to be filled in.

History and Origins

Abstract State Machines began as Yuri Gurevich’s “evolving algebras” in the late 1980s: a foundational claim that any algorithm can be modelled, at its natural level of abstraction, by an ASM. By the early 2000s the theory had a substantial literature and a growing collection of tools - the ASM Workbench, XASM, AsmGofer, and Microsoft Research’s AsmL among them - each of which made different tradeoffs between mathematical faithfulness and practical execution.

CoreASM was the next generation’s answer. Roozbeh Farahbod, then a doctoral student under Uwe Glässer at Simon Fraser University, together with Vincenzo Gervasi at the University of Pisa, presented “CoreASM: An Extensible ASM Execution Engine” at the 12th International Workshop on Abstract State Machines in Paris in 2005. The journal version followed in Fundamenta Informaticae volume 77 in 2007, and Farahbod’s 2009 SFU thesis - CoreASM: An Extensible Modeling Framework & Tool Environment for High-level Design and Analysis of Distributed Systems - gave the framework its full treatment.

The design premise, stated in the project’s own description, is that specification is a creative and evolutionary activity: a model gets written, run, broken, and rewritten many times before it is right, and the tool should support “freedom of experimentation” rather than punishing incompleteness. The practical consequence was a decision to keep the kernel of the language almost empty and push nearly everything - data types, rule forms, scheduling policies - into plugins.

Design Philosophy

Three commitments define CoreASM.

Faithfulness to ASM semantics. The language is built to mirror the mathematical definition of ASMs rather than to look like a programming language. A CoreASM run is a sequence of states; each step evaluates rules in parallel over the current state to produce a set of updates, which are then applied atomically. Inconsistent updates in the same step are a detectable failure, not a last-write-wins accident.

Minimality plus extensibility. The kernel understands almost nothing on its own. Numbers, strings, sets, lists, maps, bags, queues, stacks, trees, conditional rules, forall and choose rules, let, case, turbo-ASM sequencing, I/O, scheduling policies, plotting, and Java interoperation all arrive as engine plugins. The engine’s own source tree carries more than thirty of them, and a specification declares which ones it wants with use clauses - use StandardPlugins pulls in the usual working set.

Distributed models as first-class citizens. The project describes CoreASM as the first ASM tool to explicitly support distributed ASM computation models with custom scheduling policies. Agents are ordinary state elements with an associated program; a scheduling-policy plugin decides which subset of agents moves in a given step. That makes it possible to model a protocol once and then experiment with interleaved, fully parallel, or adversarially scheduled executions of the same model.

Key Features

A CoreASM specification names itself, imports plugins, declares its vocabulary, and names an initial rule. The following is drawn from the Daemon Game sample distributed with the Eclipse plugin, a CoreASM rendering of the classic example from the ASM book:

CoreASM DaemonGame

use  StandardPlugins

enum USER = {user1, user2}
enum COMMAND = {newGame, probe, endGame, showResult}
universe PLAY
function score: PLAY -> NUMBER
function playId: PLAY -> NUMBER
function userPlays: USER -> SET
function lastPlayId: -> NUMBER

init InitRule

rule InitRule =
    par
        lastPlayId := 0
        extend Agents with daemon do
            program(daemon) := @DaemonGame
        Agents(self) := false
        forall u in USER do userPlays(u) := {}
    endpar

rule NewGame(user) =
    if (userInput(user) = newGame) and (user memberof USER) then
        extend PLAY with p do
            Initialize(p, user)

rule Initialize(play, user) =
    par
        score(play) := 0
        add play to userPlays(user)
        playId(play) := lastPlayId
        lastPlayId := lastPlayId + 1
    endpar

The vocabulary is worth reading closely, because most of it comes straight from ASM theory:

Interpretation happens in a pipeline that the papers describe explicitly: a parser (built on a plugin-extensible grammar), an interpreter that produces update sets, an abstract storage layer that holds the state, and a scheduler that decides which agents run. Each stage exposes extension points, which is how a plugin can add not just a library function but new syntax and new rule forms.

Two integration features are worth noting. JASMine lets a specification reach into Java objects, which is how an abstract model gets attached to a concrete implementation or test harness. And Carma, the command-line engine driver, runs specifications outside Eclipse and gives scripted control over the engine - the basis on which the Bârun scripting language was built.

Evolution

CoreASM’s development arc runs roughly from 2005 to the mid-2010s. The core language and engine stabilised in the years around Farahbod’s thesis; the plug-in architecture paper of 2009 and the Software: Practice and Experience article of 2011 mark the point at which the framework was being presented as finished rather than proposed.

Tooling development then shifted centre of gravity from Simon Fraser University to Ulm University. Marcel Dausend and Alexander Raschke built a debugger for ASM specifications on top of CoreASM and merged it into the main project - a genuinely novel contribution, since stepping through a parallel-update semantics is not the same problem as stepping through imperative code. Michael Stegmaier, Dausend, and Raschke went on to publish a universal control construct for ASMs at ABZ 2016, released as a CoreASM plugin, and Ulm contributed to UASM, a unified ASM syntax distilled from the CoreASM and ASMETA languages and accepted as input by both toolchains.

The infrastructure moved with the times: SourceForge to GitHub in 2012, an Eclipse Marketplace listing in November 2013, Maven-based builds, and engine artifacts 1.7.1 through 1.7.3 published to Maven Central during 2016. After that the commit log thins out. The last changes on master, in February 2022, are dependency bumps; the Marketplace entry was last touched in December 2022 and still describes its development status as alpha.

The language also produced a descendant. CASM - the Corinthian Abstract State Machine language - began as a project heavily inspired by CoreASM’s language and has since diverged substantially, adding static type inference and a compiled implementation. Its authors cite the interpretive overhead of CoreASM’s engine as part of the motivation for a compiler-based approach - a qualitative argument in the CASM papers rather than a published head-to-head benchmark of the two implementations. The two languages now appear side by side as distinct executable ASM dialects, as in the 2023 Alternating Bit protocol tutorial.

Current Relevance

CoreASM is dormant rather than abandoned. The GitHub repositories are up, the Academic Free License 3.0 permits reuse, the Eclipse update site hosted at Ulm is still referenced from the Marketplace listing, and the engine is a Java artifact retrievable from Maven Central. Nobody is adding language features, and the last substantive activity is several years old.

Its remaining audience is the formal-methods research community. CoreASM shows up when someone wants to make an ASM model run: in Börger and Raschke’s 2018 modelling book, in comparisons between ASM and TLA+, in the ASM workshop and ABZ conference literature. Within that community it retains a specific reputation - the ASM tool that took extensibility and distributed computation models seriously, reportedly at some cost in execution speed, though no published benchmark quantifies the gap.

For anyone approaching it today, the realistic proposition is a mature, documented, Java-based interpreter for a well-specified formal language, with an Eclipse front end of a certain vintage, and a research literature that explains in unusual detail how the whole thing is put together.

Why It Matters

CoreASM is a good answer to a question formal-methods tooling keeps getting wrong: what should a specification language do about the parts of a design you have not decided yet?

Most executable formalisms answer “make them concrete or you cannot run anything.” CoreASM’s answer is that abstraction should be a first-class, marked, runnable thing - that you should be able to execute a model in which several functions are still deliberately unspecified, watch what it does, and refine downward from there. That is exactly how the ASM method describes design as working, from ground model to refinements, and CoreASM is the tool that tried hardest to make the language match the method rather than the other way round.

The plug-in architecture is the second contribution, and it is the more technically distinctive one. Very few language implementations let an extension add syntax, evaluation rules, data domains, and scheduling policy through the same mechanism. The papers that document it - particularly the 2009 plug-in architecture chapter - remain a readable case study in building an interpreter whose kernel deliberately knows almost nothing.

Its influence is visible chiefly in CASM, which took the language and rebuilt it around a compiler, and in UASM, the attempt to give the ASM community one syntax instead of several. For a research language with no commercial user base, being the thing that later tools defined themselves against is a reasonable measure of impact.