SCIENCE@home

Model-Based Trace-Checking

Y. Howard,S. Gruner,A. Gravell,Carla Ferreira,J. Augusto

Published 2011 in arXiv.org

ABSTRACT

Trace analysis can be a useful way to discover problems in a program under test. Rather than writing a special purpose trace analysis tool, this paper proposes that traces can usefully be analysed by checking them against a formal model using a standard model-checker or else an animator for executable specifications. These techniques are illustrated using a Travel Agent case study implemented in J2EE. We added trace beans to this code that write trace information to a database. The traces are then extracted and converted into a form suitable for analysis by Spin, a popular model-checker, and Pro-B, a model-checker and animator for the B notation. This illustrates the technique, and also the fact that such a system can have a variety of models, in different notations, that capture different features. These experiments have demonstrated that model-based trace-checking is feasible. Future work is focussed on scaling up the approach to larger systems by increasing the level of automation.

PUBLICATION RECORD

  • Publication year

    2011

  • Venue

    arXiv.org

  • Publication date

    2011-11-11

  • Fields of study

    Computer Science

  • Identifiers
    arXiv 1111.2825
  • External record

    Open on Semantic Scholar

  • Source metadata

    Semantic Scholar

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-25 of 25 references · Page 1 of 1

CITED BY

Showing 1-13 of 13 citing papers · Page 1 of 1