Falsification of OTSs by searches of bounded reachable state spaces

Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    5 Citations (Scopus)

    Abstract

    We propose a way to search a bounded reachable state space of an observational transition system, or an OTS for a counterexample that the OTS satisfies an invariant property Two case studies are also reported in which the proposed solution has been applied to an incorrect mutual exclusion protocol and the NSPK authentication protocol.

    Original languageEnglish
    Title of host publication18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006
    Pages440-445
    Number of pages6
    Publication statusPublished - Dec 1 2006
    Event18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006 - San Francisco Bay, CA, United States
    Duration: Jul 5 2006Jul 7 2006

    Publication series

    Name18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006

    Other

    Other18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006
    Country/TerritoryUnited States
    CitySan Francisco Bay, CA
    Period7/5/067/7/06

    All Science Journal Classification (ASJC) codes

    • Software

    Fingerprint

    Dive into the research topics of 'Falsification of OTSs by searches of bounded reachable state spaces'. Together they form a unique fingerprint.

    Cite this