Abstract
We describe a concept and design of a simulator of Real-Time Abstract State Machines. Time can be continuous or discrete. Time constraints are defined by linear inequalities. Two semantics are considered: with and without non-deterministic bounded delays between actions. The simulator is easily configurable. Simulation tasks can be generated according to descriptions in a special language. The simulator will be used for on-the-fly verification of formulas in an expressible timed predicate logic. Several features that facilitate the simulation are described: external functions definition, delays settings, constraints specification, and others.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Gurevich, Y.: Evolving algebras 1993: Lipari Guide. In: Egon, B. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)
Beauquier, D., Slissenko, A.: A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic 113, 13–52 (2002)
Beauquier, D., Slissenko, A.: Periodicity based decidable classes in a first order timed logic (Annals of Pure and Applied Logic), 38 pages (to appear)
Gurevich, Y.: Sequential abstract-state machines capture sequential algorithms. ACM Transactions on Computational Logic 1, 77–111 (2000)
Huggins, J.: University of Michigan, ASM homepage, http://www.eecs.umich.edu/gasm/
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis (2003)
Beauquier, D., Crolard, T., Prokofieva, E.: Automatic parametric verification of a root contention protocol based on abstract state machines and first order timed logic. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 372–387. Springer, Heidelberg (2004)
Foundations of Software Engineering — Microsoft Research, Microsoft Corporation: AsmL: The Abstract State Machine Language (2002), http://research.microsoft.com/fse/asml/
Soloviev, I., Usov, A.: The language of interpreter of distributed abstract state machines. Tools for Mathematical Modeling. Mathematical Research 10, 161–170 (2003)
Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of ACM 17(8), 453–455 (1974)
Cohen, J., Slissenko, A.: On verification of refinements of timed distributed algorithms. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 34–49. Springer, Heidelberg (2000)
Börger, E., Gurevich, Y., Rosenzweig, D.: The bakery algorithm: yet another specification and verification. In: Börger, E. (ed.) Specification and Validation Methods, pp. 231–243. Oxford University Press, Oxford (1995)
Usov, A.: Development of the Interpreter for Distributed ASMs. Electronic Notes in Theoretical Computer Science (2004)
Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: Proc. of the 1999 Int. Symp. on Symbolic and Algebraic Computations (ISSAC 1999), pp. 129–136. ACM Press, New York (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vasilyev, P. (2006). Simulator for Real-Time Abstract State Machines. In: Asarin, E., Bouyer, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2006. Lecture Notes in Computer Science, vol 4202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11867340_24
Download citation
DOI: https://doi.org/10.1007/11867340_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45026-9
Online ISBN: 978-3-540-45031-3
eBook Packages: Computer ScienceComputer Science (R0)