2017 IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2017, Tokyo, Japan, March 13-17, 2017 403-404 2017 [Refereed]
IEICE Transactions on Information and Systems E92-D(7) 1401-1411 Jul 2009 [Refereed]
We propose a user-defined on-demand matching strategy, called O-matching, in which users can control the order of matching arguments of each operation symbol. In ordinary matching schemes it is not important to set the order of matching, however, ...
IEICE Transactions on Information and Systems E92-D(5) 1012-1021 May 2009 [Refereed]
In the OTS/CafeOBJ method, software specifications are described in CafeOBJ executable formal specification language, and verification is done by giving scripts to the CafeOBJ system. The script is called a proof score. In this study, we propose a...
An example of verification of authentication protocols with CafeOBJ algebraic specification language is shown. The NSLPK authentication protocol is based on the public-key cryptosystem. Two principals can use the protocol to achieve the mutual aut...
An example of verification of authentication protocols with CafeOBJ algebraic specification language is shown. The NSLPK authentication protocol is based on the public-key cryptosystem. Two principals can use the protocol to achieve the mutual aut...
CafeOBJ's verification method with proof scores which only uses reductions is presented. The example of QLOCK (mutual exclusion protocol with a waiting queue) is used to present theory and principle of the verification method, and techniques for w...
Equational inference is the most fundamental inference mechanism for CafeOBJ algebraic specification language. Term rewriting system can realize equational inference in an efficient way. Several pieces of fundamental knowledge on term rewriting sy...
NAKAMURA Masaki, KONG Weiqiang, OGATA Kazuhiro, FUTATSUGI Kokichi
IEICE Transactions on Information and Systems E91-D(5) 1492-1503 May 2008 [Refereed]
There are two ways to describe a state machine as an algebraic specification: a behavioral specification and a rewrite specification. In this study, we propose a translation system from behavioral specifications to rewrite specifications to obtain...
The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the O...
CafeOBJ algebraic specification language features flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the pa...
CafeOBJ's verification method with proof scores which only uses reductions is presented. The example of QLOCK (mutual exclusion protocol with a waiting queue) is used to present theory and principle of the verification method, and techniques for w...
The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the O...
OBJ algebraic specification languages provide a sophisticate style to describe specifications based on modules. Reuse of build-in modules and modules described before makes it easy to describe large and complex specifications. An axiom of an OBJ s...
IEICE transactions on fundamentals of electronics, communications and computer sciences E89-A(6) 1558-1565 Jun 2006 [Refereed]
In this paper, we give a denotational semantics of imperative programming languages as a CafeOBJ behavioral specification. Since CafeOBJ is an executable algebraic specification language, not only execution of programs but also semi-automatic veri...
In term rewriting, a term to which some rewrite rule can be applied is called a reducible term. We apply the notion of reducibility to an operation symbol. A reducible operation symbol is defined as follows: a term having a reducible operation sym...
In term rewriting, a term to which some rewrite rule can be applied is called a reducible term. We apply the notion of reducibility to an operation symbol. A reducible operation symbol is defined as follows: a term having a reducible operation sym...
Sixth International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2005), 5-8 December 2005, Dalian, China 416-420 2005 [Refereed]
IEICE technical report. Signal processing 111(104) Jun 2011
The four technical committees of System and Signal Processing Sub-society have been holding joint workshop since 2010. We propose a panel discussion with president of System and Processing Sub-society as a chair and chairpersons or representatives...
Technical report of IEICE. CST 110(370) 1-4 Jan 2011
Multi-Car Elevator (MCE) is an elevator system that has several cars in a single shaft. In this solution competition, students teams develop MCE controllers. In the past CST solution competitions (2007 and 2008) only the group controller is a targ...
Technical report of IEICE. CST 110(161) 7-12 Jul 2010
In software developments with formal methods, there exists an unavoidable gap between a system description in formal specification languages and a system implementation in programming languages. In our previous work, we have proposed a method to g...
In the OTS/CafeOBJ method, we describe a specification in CafeOBJ specification language, and verify it with a proof score. In this study, we propose a test-generating method from an OTS/CafeOBJ specification together with proof scores. Our propos...
NAKAMURA Masaki, KONG Weiqiang, OGATA Kazuhiro, FUTATSUGI Kokichi
Technical report of IEICE. SS 106(120) 1-6 Jun 2006
There are two ways to describe a state machine with algebraic specifications: observation transition systems on CafeOBJ and rewrite specifications on Maude. Each specification language has different verification techniques. In this study, to make ...
Technical report of IEICE. SS 104(570) 1-6 Nov 2005
Many formal methods to verify systems have been proposed and utilized. But, it looks like that there are few studies that compare different fomal methods and make their strong and weak points clear. We have performed a case study that the STS prot...
Technical report of IEICE. SS 100(569) 17-23 Nov 2001
Context-sensitive rewriting is a restriction of rewriting formalized by a replacement map on function symbols. In the current context-sensitive rewriting we must choose each argument of a function symbol whether to be active or not. If an argument...
IEICE technical report. Theoretical foundations of Computing 98(432) 57-64 Dec 1998
The general dummy elimination defined by Ferreira is a transformation on TRSs that eliminates a function symbol in rules of TRSs to prove termimation easier thsn the original one. Recently, Arts and Giesl introduced the notion of dependency pairs,...
"Induction" and "case-splitting" are fundamentals of verifications of problem models (models in problem or application domains) by proof scores. The following research achievements are gotten about induction and case-splitting which are effective ...
The following two important problems about construction and verification of problem models are investigated :(1) How to set an appropriate abstraction level in constructions of problem models and/or specifications.(2) How to combine interactive th...
The following results have been gotten by doing research for developing the verification technology which is highly applicable and flexible, and is amenable for automation.(1)Inspection Technology for Unknown Viruses : Based on the logics of behav...
