AsmL: Abstract State Machine Language

Established: November 2, 2001

AsmL is an industrial-strength executable specification language. It can be used at any stage of the programming process: design, coding, or testing. It is fully integrated into the Microsoft .NET environment: AsmL models can interoperate with any other .NET assembly, no matter what source language it is written in. AsmL uses XML and Word for literate specifications.

What is AsmL?

AsmL is the Abstract State Machine Language. The FSE group develops AsmL. It is an executable specification language based on the theory of Abstract State Machines, invented by Yuri Gurevich (opens in new tab). The current version, AsmL for Microsoft .NET, is embedded into Microsoft Word. It uses XML and Word for literate specifications. It is fully interoperable with other .NET languages. AsmL generates .NET assemblies which can either be executed from the command line, linked with other .NET assemblies, or packaged as COM components.

What is it good for?

AsmL is useful in any situation where you need a precise, non-ambiguous way to specify a computer system, either software or hardware. AsmL specifications are an ideal way for teams to communicate design decisions. Program managers, developers, and testers can all use an AsmL specification to achieve a single, unified understanding.

One of the greatest benefits of an AsmL specification is that you can execute it. That means it is useful before you commit yourself to coding the entire system. By exploring your design, you can answer the following questions: Does it do everything you intended it to? How do the features interact? Are there any unintended behaviors?

Availability

Binaries: AsmL provides the foundations of the model-based testing tool Spec Explorer. The Spec Explorer distribution includes the latest AsmL compiler for Microsoft .NET . Spec Explorer can also explore models written AsmL. Please go to the Spec Explorer (opens in new tab) website to learn more about Spec Explorer and to obtain a copy.

Sources: The sources of the AsmL compiler are available as part of the AsmL community project on CodePlex (opens in new tab).

People

Portrait of Margus Veanes

Margus Veanes

Principal Researcher

Portrait of Tony Hoare

Tony Hoare

Emeritus Researcher