Stability of Real-Time Abstract State Machines under Desynchronization

Abstract

In our paper TR-LACL-2008–02 ( www.univ-paris12.fr/lacl/) we give sufficient conditions that permit to implement a real-time ASM with instantaneous actions (IA-ASM) by an ASM with delayed actions (DA-ASM) with approximate bisimulation of runs. The time is continuous and time constraints are linear inequalities with rational coefficients. As IA-ASM we consider ASM whose programs are blocks of if guard then blockOfUpdates. The implementation is an ASM of more general type. It works by 2 phases: backup phase memorizes the values of functions, and update phase makes the updates using the backed up values. Such an implementation implies shifts of time instants and, consequently, of the values of the real-valued functions. The approximation of runs (and, thus approximate bisimulation) is determined by 2 positive parameters , where bounds time shifts, and bounds the deviations of real-valued functions. We introduce a notion of -sturdy IA-ASM, and prove that the implementation of any such IA-ASM gives an DA-ASM with -approximately bisimular runs if the delay satisfies some constraints. An interesting point is that the sources of desynchronization that destroy the bisimulation are much more subtle and numerous than one can think a priori. Another conceptual consequence concerns the adequacy of the notion of IA-ASM that was introduced in Gurevich–Huggins (LNCS, vol. 1092, 1996), and later studied in Beauquier–Slissenko, (APAL, 113(1–3):13–52, 2002) for the specification of real-time system.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{CohenS08,
  author       = {Jo{\"{e}}lle Cohen and
                  Anatol Slissenko},
  editor       = {Egon B{\"{o}}rger and
                  Michael J. Butler and
                  Jonathan P. Bowen and
                  Paul Boca},
  title        = {Stability of Real-Time Abstract State Machines under Desynchronization},
  booktitle    = {Abstract State Machines, {B} and Z, First International Conference,
                  {ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5238},
  pages        = {341},
  publisher    = {Springer},
  year         = {2008},
  url          = {https://doi.org/10.1007/978-3-540-87603-8\_29},
  doi          = {10.1007/978-3-540-87603-8\_29},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/CohenS08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}