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

Fingerprint

Authentication

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Ogata, K., Kong, W., & Futatsugi, K. (2006). Falsification of OTSs by searches of bounded reachable state spaces. In 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006 (pp. 440-445). (18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006).

Falsification of OTSs by searches of bounded reachable state spaces. / Ogata, Kazuhiro; Kong, Weiqiang; Futatsugi, Kokichi.

18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006. 2006. p. 440-445 (18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006).

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

Ogata, K, Kong, W & Futatsugi, K 2006, Falsification of OTSs by searches of bounded reachable state spaces. in 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006. 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006, pp. 440-445, 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006, San Francisco Bay, CA, United States, 7/5/06.
Ogata K, Kong W, Futatsugi K. Falsification of OTSs by searches of bounded reachable state spaces. In 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006. 2006. p. 440-445. (18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006).
Ogata, Kazuhiro ; Kong, Weiqiang ; Futatsugi, Kokichi. / Falsification of OTSs by searches of bounded reachable state spaces. 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006. 2006. pp. 440-445 (18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006).
@inproceedings{a99bf39cd1e849978d7fe27a48944583,
title = "Falsification of OTSs by searches of bounded reachable state spaces",
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.",
author = "Kazuhiro Ogata and Weiqiang Kong and Kokichi Futatsugi",
year = "2006",
month = "12",
day = "1",
language = "English",
isbn = "9781627486606",
series = "18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006",
pages = "440--445",
booktitle = "18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006",

}

TY - GEN

T1 - Falsification of OTSs by searches of bounded reachable state spaces

AU - Ogata, Kazuhiro

AU - Kong, Weiqiang

AU - Futatsugi, Kokichi

PY - 2006/12/1

Y1 - 2006/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33845248783&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845248783&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:33845248783

SN - 9781627486606

T3 - 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006

SP - 440

EP - 445

BT - 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006

ER -