The language presented in this paper is fully implemented. The system is used as the basis for the Montages/Gem-Mex, where generated XASM code is translated into an interpreter for the language specified using Montages. As a case study the full specificatio of ANSI C has been entered by Wuwei Shen [18]. Other case studies are currently under development, see for example an application to microprocessor simulation in [31] and the application of XASM as gluing code in legacy systems [3].
As next steps, the XASM compiler, runtime system and graphical support environment will be further optimized. Also, a concept how tools for the (automatic) verification, model checking and analysis of the ASM formalizations can be integrated into the system is currently under development and will be part of the support system in future versions of the tool. Furthermore, the connection to repository systems will be subject to future considerations concerning the XASM-language. For example, certain ASM functions may be marked as ``persistent'', meaning that the values of the locations of these functions are stored in the repository system, so that they can be access the next time the XASM is executed. This kind of extension is currently part of work carried out in an industry-based research project running at GMD In this project, it is currently considered to use XASM for formulating certain consistency check algorithms occurring in the context of this project.
Additional applications outside the ASM area are possible, since ASMs can be considered as an instance of so called transitions system models, which form as well the basis for other popular formalisms such as UNITY [10], TLA [22], SPL [23] and the SAL intermediate language [28]. As mentioned in Section 6 the XASM system is integrated with the Montages method such that new or alternative constructs can be easily supported by XASM. Using Montages, both syntax and semantics of new or alternative XASM constructs can be developed in an integrated development environment called Gem-Mex. Such an extensible system architecture allows to tailor XASM as a tool for one of the above mentioned formalisms based on transition systems.
An adopted version of XASM would be especially useful in a context like the SAL architecture [6], where various other tools are integrated for tasks like theorem proofing and model checking. The development cycle supported by the tools integrated with SAL could be extended with a tool like XASM for debugging and animation of the transition system under consideration. After the developer gained confidence in his specification by debugging and animating them with XASM, the other tools would be used to further analyze the specification. As a result of the further analysis, the original specification typically undergoes major changes. To avoid typos introduced by those changes, the specification can again be debugged and animated using XASM before it is passed to the other tools.
We plan to adapt XASM to architectures like SAL in order to make it accessible to a large basis of users. By following this lines we are further able to adapt the Montages method to formalisms like SAL, allowing to give language semantics with SAL. A specific language may then be developed such that the SAL semantics of programs written in that language is easy to analyze by the available tools. The concrete syntax of such a language can be adapted to the terminology of domain experts using the language to describe their system. An example of using Montages to develop a language for a special domain is given in [21].