Trace anonymity in the OTS/CafeOBJ method

Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, Kokichi Futatsugi

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

1 Citation (Scopus)

Abstract

We report on a case study in which the OTS/CafeOBJ method is used to formalize and verify trace anonymity property of distributed systems. In this case study, the property of trace anonymity is formalized with the trace notations of Observational Transition Systems (OTSs), and CafeOBJ language/system is used as an interactive theorem prover to verify that systems satisfy such property. The work presented in the paper follows the approach proposed in [3], in which I/O automaton and Larch prover are employed for handling trace anonymity.

Original languageEnglish
Title of host publicationProceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008
Pages754-759
Number of pages6
DOIs
Publication statusPublished - Sep 22 2008
Event2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008 - Sydney, NSW, Australia
Duration: Jul 8 2008Jul 11 2008

Publication series

NameProceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008

Other

Other2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008
CountryAustralia
CitySydney, NSW
Period7/8/087/11/08

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Information Systems

Cite this

Kong, W., Ogata, K., Cheng, J., & Futatsugi, K. (2008). Trace anonymity in the OTS/CafeOBJ method. In Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008 (pp. 754-759). [4594769] (Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008). https://doi.org/10.1109/CIT.2008.4594769