Keyword : CafeOBJ


TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned
Iakovos OURANOS Kazuhiro OGATA Petros STEFANEAS 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2014/05/01
Vol. E97-D  No. 5 ; pp. 1160-1170
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
Keyword: 
source authenticationTESLA protocolCafeOBJverificationtimed OTSlessons learned
 Summary | Full Text:PDF(1.7MB)

An Algorithm for Allocating User Requests to Licenses in the OMA DRM System
Nikolaos TRIANTAFYLLOU Petros STEFANEAS Panayiotis FRANGOS 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2013/06/01
Vol. E96-D  No. 6 ; pp. 1258-1267
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Methods
Keyword: 
mobile DRMOMAorder of rights object evaluationCafeOBJsafetyinvariant properties
 Summary | Full Text:PDF(275.7KB)

Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support
Min ZHANG Kazuhiro OGATA Masaki NAKAMURA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Vol. E94-D  No. 5 ; pp. 976-988
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Specification Translation
Keyword: 
specification translationCafeOBJMaudeequational theory specificationrewrite theory specification
 Summary | Full Text:PDF(919.9KB)

Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method
Masaki NAKAMURA Takahiro SEINO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2009/05/01
Vol. E92-D  No. 5 ; pp. 1012-1021
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Software Testing
Keyword: 
formal specificationproof scoresoftware testingOTSCafeOBJ
 Summary | Full Text:PDF(233KB)

Proof Score Approach to Verification of Liveness Properties
Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/12/01
Vol. E91-D  No. 12 ; pp. 2804-2817
Type of Manuscript:  PAPER
Category: Fundamentals of Software and Theory of Programs
Keyword: 
CafeOBJequationsobservational transition systems (OTSs)rewritingspecification
 Summary | Full Text:PDF(261.7KB)

A Specification Translation from Behavioral Specifications to Rewrite Specifications
Masaki NAKAMURA Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/05/01
Vol. E91-D  No. 5 ; pp. 1492-1503
Type of Manuscript:  PAPER
Category: Fundamentals of Software and Theory of Programs
Keyword: 
specification translationverificationalgebraic specificationbehavioral specificationrewirte specificationCafeOBJMaude
 Summary | Full Text:PDF(306.5KB)

An Algebraic Framework for Modeling of Mobile Systems
Iakovos OURANOS Petros STEFANEAS Panayiotis FRANGOS 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2007/09/01
Vol. E90-A  No. 9 ; pp. 1986-1999
Type of Manuscript:  PAPER
Category: Concurrent Systems
Keyword: 
mobile computingalgebraic specificationformal verificationobservational transition systemsCafeOBJMobileOBJ
 Summary | Full Text:PDF(312KB)

A Behavioral Specification of Imperative Programming Languages
Masaki NAKAMURA Masahiro WATANABE Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2006/06/01
Vol. E89-A  No. 6 ; pp. 1558-1565
Type of Manuscript:  Special Section PAPER (Special Section on Papers Selected from 2005 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC2005))
Category: 
Keyword: 
semantics of imperative programsbehavioral specificationCafeOBJ
 Summary | Full Text:PDF(196.7KB)

Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ
Takahiro SEINO Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2001/06/01
Vol. E84-A  No. 6 ; pp. 1471-1478
Type of Manuscript:  Special Section PAPER (Special Section on Papers Selected from 2000 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2000))
Category: 
Keyword: 
CafeOBJformal methodrailroad signaling
 Summary | Full Text:PDF(413KB)