2017 IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2017, Tokyo, Japan, March 13-17, 2017 403-404 2017 [Refereed]
2014 11th Int. Joint Conf. on Computer Science and Software Engineering: "Human Factors in Computer Science and Software Engineering" - e-Science and High Performance Computing: eHPC, JCSSE 2014 337-342 Jan 2014
OBJ algebraic specification languages support automated equational reasoning based on term rewriting for interactive verification. The equational reasoning is sound but not always complete in general. In our previous work, we have given a conditio...
IAENG International Journal of Computer Science 40 117-123 Aug 2013
OBJ algebraic specification languages support semi-automated verification of algebraic specifications basedon equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees...
Lecture Notes in Engineering and Computer Science 2202 516-521 Jan 2013
OBJ algebraic specification languages support semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantee...
Lecture Notes in Engineering and Computer Science 2195 269-274 Jan 2012
OBJ algebraic specification languages support automated equational reasoning based on term rewriting systems (TRSs) for specification verification. Termination is one of the most important properties of TRSs. Terminating TRSs guarantee that any eq...
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...
An example of verification of communication protocols with CafeOB J algebraic specification language is shown. The SCP communication protocol is a simplified version of the ABP communication protocol, which uses unreliable cells as communication c...
Technical report of IEICE. SS 107(392) 25-30 Dec 2007
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 ...
NAKAMURA Masaki, MIRCEA GAINA Daniel, OGATA Kazuhiro, FUTATSUGI Kokichi
Technical report of IEICE. SS 114(510) 1-6 Mar 2015
CafeOBJ algebraic specification language supports description of specifications whose models are constructor-based order-sorted algebras, and also supports parameterized specifications. Sufficient completeness is one of the most important properti...
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...
IEICE technical report. Welfare Information technology 114(217) 75-80 Sep 2014
Cognitive Dysfunction patients are sometimes unable to drive with safety check action by symptoms such as attention disorders. We believe that this safety check action is related to the characteristics of the intersections. We experimented using r...
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. Welfare Information technology 113(272) 29-34 Oct 2013
Cognitive Dysfunction is a diagnosed state of symptom such as dysmnesia and attention disorders sourced of various diseases. This symptom is expected to be recovered by medical treatment, but may cause trouble of driving according to its severity....
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 1702 47-61 Jan 1999
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,...
Analyzing sit-to-stand movement is important to understand how the balance function of a rehabilitation patient is recovered. For analyzing sit-to-stand movement, we propose a system to visualize center of gravity (COG) and base of support (BOS) i...
Human error occupies a large part of the medical accidents(such as injection of wrong medicine by mistake). Although pointing and calling is one of the countermeasures of Nurses' error, it is reported that pointing and calling is not thorough from...
IEICE technical report. Welfare Information technology 112(475) 175-180 Mar 2013
Analyzing sit-to-stand movement is important to understand how the balance function of a rehabilitation patient is recovered. For analyzing sit-to-stand movement, we propose a system to visualize center of gravity (COG) and base of support (BOS) i...
IEICE technical report. Welfare Information technology 112(475) 181-186 Mar 2013
Human error occupies a large part of the medical accidents(such as injection of wrong medicine by mistake). Although pointing and calling is one of the countermeasures of Nurses' error, it is reported that pointing and calling is not thorough from...
IEICE technical report. Image engineering 112(473) 175-180 Mar 2013
Analyzing sit-to-stand movement is important to understand how the balance function of a rehabilitation patient is recovered. For analyzing sit-to-stand movement, we propose a system to visualize center of gravity (COG) and base of support (BOS) i...
IEICE technical report. Image engineering 112(473) 181-186 Mar 2013
Human error occupies a large part of the medical accidents(such as injection of wrong medicine by mistake). Although pointing and calling is one of the countermeasures of Nurses' error, it is reported that pointing and calling is not thorough from...
Technical report of IEICE. Multimedia and virtual environment 112(474) 175-180 Mar 2013
Analyzing sit-to-stand movement is important to understand how the balance function of a rehabilitation patient is recovered. For analyzing sit-to-stand movement, we propose a system to visualize center of gravity (COG) and base of support (BOS) i...
Technical report of IEICE. Multimedia and virtual environment 112(474) 181-186 Mar 2013
Human error occupies a large part of the medical accidents(such as injection of wrong medicine by mistake). Although pointing and calling is one of the countermeasures of Nurses' error, it is reported that pointing and calling is not thorough from...
We are developing a monitoring system for in-home patients. For the monitoring system, we equipped peripheral instruments for daily living (such as wheelchair, bed and handrail of toilet) with sensors which conflict sense of privacy not too much. ...
我々は，在宅患者が日常生活で利用する車椅子，ベッド，トイレ手すりに荷重センサなどを複数設置し，それらを用いてプライバシ侵害感の少ない見守りシステムを実現しようとしている．しかし，見守り実現のためには，取得した複数のセンサ情報を集約し，患者の行動と結びつける必要がある．本稿では，構築したセンサシステムと予備実験結果について述べる．We are developing a monitoring system for in-home patients. For the monitoring sys...
IEICE technical report. Circuits and systems 111(102) 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...
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...
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...
Mathematical Systems Science and its Applications : IEICE technical report 111(105) 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...
IEICE technical report. Theoretical foundations of Computing 99(492) 57-64 Dec 1999
For reducing a given term in term rewriting systems (TRS), we match a subterm of the term to the left-hand side of a rule and replace the subterm by the right-hand side of the rule. A Context-sensitive rewriting system consists a TRS and a replace...
