|
JAIST Repository >
School of Information Science >
Conference Papers >
Conference Papers >
Please use this identifier to cite or link to this item:
https://hdl.handle.net/10119/8487
|
| Title: | Trace anonymity in the OTS/CafeOBJ method |
| Authors: | Kong, Weiqiang
Ogata, Kazuhiro
Cheng, Jian
Futatsugi, Kokichi |
| Issue Date: | 2008-07 |
| Publisher: | Institute of Electrical and Electronics Engineers (IEEE) |
| Magazine name: | 8th IEEE International Conference on Computer and Information Technology, 2008. CIT 2008. |
| Start page: | 754 |
| End page: | 759 |
| DOI: | 10.1109/CIT.2008.4594769 |
| 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. |
| Rights: | Copyright (C) 2008 IEEE. Reprinted from 8th IEEE International Conference on Computer and Information Technology, 2008. CIT 2008., 754-759. This material is posted here with permission of the IEEE. Such permission of the IEEE does not in any way imply IEEE endorsement of any of JAIST's products or services. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to pubs-permissions@ieee.org. By choosing to view this document, you agree to all provisions of the copyright laws protecting it. |
| URI: | https://hdl.handle.net/10119/8487 |
| Material Type: | publisher |
| Appears in Collections: | b11-1. 会議発表論文・発表資料 (Conference Papers)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| A13846.pdf | | 165Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
