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. 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 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.
2009
- Margus Veanes, Nikolaj Bjorner, Yuri Gurevich, and Wolfram Schulte, Symbolic Bounded Model Checking of Abstract State Machines, in Int J Software Informatics, vol. 3, no. (2-3), pp. 149-170, June 2009
- Margus Veanes and Nikolaj Bjorner, Symbolic Bounded Conformance Checking of Model Programs, no. MSR-TR-2009-28, 14 March 2009
2008
- Margus Veanes and Ando Saabas, On Bounded Reachability of Programs with Set Comprehensions, in LPAR'08, Springer Verlag, November 2008
- Margus Veanes and Ando Saabas, Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract), in ABZ'08, Springer Verlag, September 2008
- Margus Veanes, Nikolaj Bjørner, and Alexander Raschke, An SMT Approach to Bounded Reachability Analysis of Model Programs, in FORTE'08, Springer Verlag, June 2008
- Margus Veanes, Ando Saabas, and Nikolaj Bjorner, Bounded reachability of model programs, no. MSR-TR-2008-81, May 2008
- Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson, Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, in Formal Methods and Testing, vol. 4949, pp. 39-76, Springer Verlag, 2008
2007
- Yuri Gurevich, Margus Veanes, and Charles Wallace, Can Abstract State Machines Be Useful in Language Theory?, in Theoretical Computer Science, vol. 376, no. 1, pp. 17-29, Elsevier , 2007
2005
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to Test, in FATES 2005, Springer Verlag, July 2005
- Yuri Gurevich and Nikolai Tillmann, Partial updates, in Theor. Comput. Sci., vol. 336, no. 2-3, pp. 311-342, Springer Verlag, 2005
- Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Testing Concurrent Object-Oriented Systems with Spec Explorer, in FM, Springer, 2005
- Colin Campbell and Margus Veanes, Exploration with Multiple State Groupings, in Abstract State Machines 2005, 2005
- Yuri Gurevich, Benjamin Rossman, and Wolfram Schulte, Semantic essence of AsmL, in Theor. Comput. Sci., vol. 343, no. 3, pp. 370-412, 2005
2004
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, Abstract Communication Model for Distributed Systems, in IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, vol. 30, no. 7, pp. 1-15, IEEE Computer Society, July 2004
- Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Towards a Tool Environment for Model-Based Testing with AsmL, in FATES 2003, Springer Verlag, 2004
- Wolfgang Grieskamp, Nikolai Tillmann, and Margus Veanes, Instrumenting Scenarios in a Model-Driven Development Environment, in Journal of Information and Software Technology, vol. 46, no. 15, pp. 1027-1036, Elsevier , 2004
2003
- Wolfgang Grieskamp, Lev Nachmanson, Nikolai Tillmann, and Margus Veanes, Test Case Generation from AsmL Specifications, in ASM 2003, Springer Verlag, March 2003
- Margus Veanes and Rostislav Yavorsky, Combined Algorithm for Approximating a Finite State Abstraction of a Large System, in ICSE 2003/Scenarios Workshop, 2003
- Michael Barnett, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Validating Use-Cases with the AsmL Test Tool, in QSIC, IEEE Computer Society, 2003
- Yuri Gurevich and Nikolai Tillmann, Partial Updates Exploration II, in Abstract State Machines, Springer Verlag, 2003
- Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Model-Based Testing with AsmL .NET, in 1st European Conference on Model-Driven Software Engineering, 2003
2002
- Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Generating finite state machines from abstract state machines, in ISSTA 2002, July 2002
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, An Abstract Communication Model, no. MSR-TR-2002-55, May 2002
- Uwe Glässer and Margus Veanes, Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines, in Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002), Kluwer Academic , 2002
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, High-level Executable Specification of the Universal Plug and Play Architecture, in HICSS 2002, IEEE Computer Society, 2002
- Margus Veanes, Modeling Software: From Theory to Practice, in FSTTCS 2002, Springer Verlag, 2002
2001
- Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Toward Industrial Strength Abstract State Machines, no. MSR-TR-2001-98, October 2001
- U. Glässer, Y. Gurevich, and M. Veanes, Universal Plug and Play Machine Models, no. MSR-TR-2001-59, June 2001
- Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Conformance Testing with Abstract State Machines, in EUROCAST 2001, February 2001
- Yuri Gurevich and Nikolai Tillmann, Partial Updates: Exploration, in J. UCS, vol. 7, no. 11, pp. 917-951, Springer Verlag, 2001
