Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method

Electronic Notes in Theoretical Computer Science - Tập 201 - Trang 127-154 - 2008
Kazuhiro Ogata1, Kokichi Futatsugi1
1School of Information Science, Japan Advanced Institute of Science and Technolog, 1-1 Asahidai, Nomi, Ishikawa 923-1290

Tài liệu tham khảo

Abrial, 1996

Abrial, J.-R., Refinement, decomposition and instantiation of discrete models, in: 12th International Workshop on Abstract State Machines (12th ASM), 2005, pp. 17–40

Davies, 1996

Diaconescu, 1998, CafeOBJ report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, 6

Diaconescu, 2000, Behavioural coherence in object-oriented algebraic specification, Journal of Universal Computer Science, 6, 74

Diaconescu, 2003, CafeOBJ: Logical foundations and methodologies, Computing and Informatics, 22, 257

Futatsugi, K., Verifying specifications with proof scores in CafeOBJ, in: 21st International Conference on Automated Software Engineering (ASE 2006) (2006), pp. 3–10.

Goguen, 2000, A hidden agenda, Theoretical Computer Science, 245, 55, 10.1016/S0304-3975(99)00275-3

Hsiang, 1983, Rewrite methods for clausal and nonclausal theorem proving, 154, 331

Jones, 1990

Kong, 2007, Algebraic approaches to formal analysis of the Mondex electronic purse system, 4591, 393

Lynch, 1996

Milner, 1989

Ogata, 2003, Formal analysis of the iKP electronic payment protocols, 2609, 441

Ogata, 2003, Proof scores in the OTS/CafeOBJ method, 2884, 170

Ogata, K. and K. Futatsugi, Equational approach to formal analysis of TLS, in: 25th International Conference on Distributed Computing Systems (25th ICDCS) (2005), pp. 795–804

Ogata, 2006, Some tips on writing proof scores in the OTS/CafeOBJ method, 4060, 596

Thông tin
Thông tin xuất bản

Electronic Notes in Theoretical Computer Science

Tập 201

127-154

Thông tin tác giả