Local model update with an application to sliding window protocol

Michael Kelly, Yan Zhang

    Research output: Chapter in Book / Conference PaperConference Paperpeer-review

    1 Citation (Scopus)

    Abstract

    Local model update is a procedure whereby a property is found unsatisfied in some model and can be effectively made satisfied in the error reporting counterexample through a series of modifications. With this the counterexample can be reintegrated into the original model to derive a global fix. In this paper we put forward the case for local model update as a method for automatic update. We review theory underlying local model update and introduce the use of a tool lmu for automatically generating candidate updates, looking at general design principles. Finally we present a case study of the update process as applied to an abstraction of the sliding window protocol under a man-in-the-middle attack, showing the modelling process, update procedure and final derivation of a coherant model fix.
    Original languageEnglish
    Title of host publicationProceedings Knowledge-Based and Intelligent Information and Engineering Systems: 14th International Conference, KES 2010, Cardiff, UK, September 8-10, 2010
    PublisherSpringer
    Pages11-21
    Number of pages11
    ISBN (Print)9783642153839
    DOIs
    Publication statusPublished - 2010
    EventInternational Conference on Knowledge-Based Intelligent Information and Engineering Systems -
    Duration: 8 Sept 2010 → …

    Publication series

    Name
    ISSN (Print)0302-9743

    Conference

    ConferenceInternational Conference on Knowledge-Based Intelligent Information and Engineering Systems
    Period8/09/10 → …

    Fingerprint

    Dive into the research topics of 'Local model update with an application to sliding window protocol'. Together they form a unique fingerprint.

    Cite this