DocumentCode :
2509464
Title :
Trace anonymity in the OTS/CafeOBJ method
Author :
Kong, Weiqiang ; Ogata, Kazuhiro ; Cheng, Jian ; Futatsugi, Kokichi
Author_Institution :
Japan Adv. Inst. of Sci. & Technol., Ishikawa
fYear :
2008
fDate :
8-11 July 2008
Firstpage :
754
Lastpage :
759
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.
Keywords :
data handling; formal languages; CafeOBJ method; I-O automaton; Larch prover; interactive theorem prover; observational transition systems; trace anonymity; Artificial intelligence; Automata; Equations; Formal verification; Privacy; Safety; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer and Information Technology, 2008. CIT 2008. 8th IEEE International Conference on
Conference_Location :
Sydney, NSW
Print_ISBN :
978-1-4244-2357-6
Electronic_ISBN :
978-1-4244-2358-3
Type :
conf
DOI :
10.1109/CIT.2008.4594769
Filename :
4594769
Link To Document :
بازگشت