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

4 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
CountryUnited 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