Trace anonymity in the OTS/CafeOBJ method

Weiqiang Kong; Kazuhiro Ogata; Jian Cheng; Kokichi Futatsugi

doi:10.1109/CIT.2008.4594769

Trace anonymity in the OTS/CafeOBJ method

Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, Kokichi Futatsugi

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008
Pages	754-759
Number of pages	6
DOIs	https://doi.org/10.1109/CIT.2008.4594769
Publication status	Published - Sept 22 2008
Event	2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008 - Sydney, NSW, Australia Duration: Jul 8 2008 → Jul 11 2008

Publication series

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

Other

Other	2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008
Country/Territory	Australia
City	Sydney, NSW
Period	7/8/08 → 7/11/08

All Science Journal Classification (ASJC) codes

Computer Science Applications
Information Systems

Access to Document

10.1109/CIT.2008.4594769

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

Trace anonymity in the OTS/CafeOBJ method. / Kong, Weiqiang; Ogata, Kazuhiro; Cheng, Jian et al.

Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008. 2008. p. 754-759 4594769 (Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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., 4594769, Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008, pp. 754-759, 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008, Sydney, NSW, Australia, 7/8/08. https://doi.org/10.1109/CIT.2008.4594769

@inproceedings{a295a659dd264243ad4fa18cb51695b0,

title = "Trace anonymity in the OTS/CafeOBJ method",

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.",

author = "Weiqiang Kong and Kazuhiro Ogata and Jian Cheng and Kokichi Futatsugi",

year = "2008",

month = sep,

day = "22",

doi = "10.1109/CIT.2008.4594769",

language = "English",

isbn = "9781424423583",

series = "Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008",

pages = "754--759",

booktitle = "Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008",

note = "2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008 ; Conference date: 08-07-2008 Through 11-07-2008",

}

TY - GEN

T1 - Trace anonymity in the OTS/CafeOBJ method

AU - Kong, Weiqiang

AU - Ogata, Kazuhiro

AU - Cheng, Jian

AU - Futatsugi, Kokichi

PY - 2008/9/22

Y1 - 2008/9/22

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

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

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

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

U2 - 10.1109/CIT.2008.4594769

DO - 10.1109/CIT.2008.4594769

M3 - Conference contribution

AN - SCOPUS:51849122058

SN - 9781424423583

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

SP - 754

EP - 759

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

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

Y2 - 8 July 2008 through 11 July 2008

ER -

Trace anonymity in the OTS/CafeOBJ method

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this