Masaki Nakamura

J-GLOBAL         Last updated: Dec 18, 2018 at 11:52
 
Avatar
Name
Masaki Nakamura
Affiliation
Toyama Prefectural University

Academic & Professional Experience

 
Apr 2017
 - 
Today
Associate Professor, Toyama Prefectural University
 
2011
 - 
2017
TOYAMA Prefectural University
 
Apr 2008
   
 
Assistant Professor, Kanazawa University
 

Published Papers

 
Ryusei Mori,Masaki Nakamura
2017 IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2017, Tokyo, Japan, March 13-17, 2017   403-404   2017   [Refereed]
ヒューマンインタフェース学会論文誌 The transactions of Human Interface Society   18(1) 133-140   2016   [Refereed]
Akira Urashima,Masaki Nakamura,Tomoji Toriyama,Junichi Oshima,Mitsuko Nakagawa,Tadao Nomura
11th Asia Pacific Conference on Computer Human Interaction, APCHI '13, Bangalore, India - September 24 - 27, 2013   192-194   2013   [Refereed]
Masaki Nakamura
IEICE Transactions   100-D(6) 1157   2017
Masaki Nakamura
IEEE 5th Global Conference on Consumer Electronics, GCCE 2016, Kyoto, Japan, October 11-14, 2016   1-2   2016   [Refereed]
Masaki Nakamura,Akira Urashima,Tomoji Toriyama,Toshihiro Ninomiya,Noriyuki Fukumoto,Yuuki Aiboshi
IEEE 4th Global Conference on Consumer Electronics, GCCE 2015, Osaka, Japan, 27-30 October 2015   502-503   2015   [Refereed]
Masaki Nakamura
IEICE Transactions   98-A(2) 611   2015
Masaki Nakamura,Kazuhiro Ogata,Kokichi Futatsugi
Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi   92-109   2014   [Refereed]
Min Zhang 0002,Kazuhiro Ogata,Masaki Nakamura
IEICE Transactions   94-D(5) 976-988   2011   [Refereed]
Masaki Nakamura,Kazuhiro Ogata,Kokichi Futatsugi
J. Symb. Comput.   45(5) 551-573   2010   [Refereed]
Min Zhang 0002,Kazuhiro Ogata,Masaki Nakamura
Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings   678-693   2010   [Refereed]
Nakamura Masaki, El-Nashar Alaa Ismail, Futatsugi Kokicih
8(1) 85-92   Aug 2009   [Refereed]
NAKAMURA Masaki, OGATA Kazuhiro, FUTATSUGI Kokichi
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, ...
NAKAMURA Masaki, SEINO Takahiro
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...
OGATA Kazuhiro, FUTATSUGI Kokichi, NAKAMURA Masaki
26(2) 93-106   Apr 2009   [Refereed]
Ogata Kazuhiro, Futatsugi Kokichi, Nakamura Masaki
26(1) 71-83   Dec 2009   [Refereed]
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...
OGATA Kazuhiro, FUTATSUGI Kokichi, NAKAMURA Masaki
Computer Software   26(1) 71-83   2009   [Refereed]
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...
Futatsugi Kokichi, Ogata Kazuhiro, Nakamura Masaki
25(4) 68-84   Feb 2008   [Refereed]
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...
Nakamura Masaki, Futatsugi Kokichi, Ogata Kazuhiro
25(3) 69-80   Jul 2008   [Refereed]
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...
Futatsugi Kokichi, Ogata Kazuhiro, Nakamura Masaki
25(2) 1-13   Apr 2008   [Refereed]
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...
Nakamura Masaki, Futatsugi Kokichi, Ogata Kazuhiro
25(2) 14-27   Apr 2008   [Refereed]
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...
Ogata Kazuhiro, Nakamura Masaki, Futatsugi Kokichi
25(2) 78-84   Apr 2008   [Refereed]
FUTATSUGI Kokichi, OGATA Kazuhiro, NAKAMURA Masaki
Computer Software   25(4) 68-84   2008   [Refereed]
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...
OGATA Kazuhiro, NAKAMURA Masaki, FUTATSUGI Kokichi
Computer Software   25(2) 78-84   2008   [Refereed]
FUTATSUGI Kokichi, OGATA Kazuhiro, NAKAMURA Masaki
Computer Software   25(2) 1-13   2008   [Refereed]
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...
Nakamura Masaki, Futatsugi Kokichi
6(0) 27-30   Aug 2007   [Refereed]
Masahiro Nakano,Kazuhiro Ogata,Masaki Nakamura,Kokichi Futatsugi
International Journal of Software Engineering and Knowledge Engineering   17(6) 783-804   2007   [Refereed]
Masaki Nakamura,Kokichi Futatsugi
Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings   381-395   2007   [Refereed]
Nakamura Masaki, Futatsugi Kokichi
Computer Software   23(3) 35-50   Jul 2006   [Refereed]
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...
NAKAMURA Masaki, WATANABE Masahiro, FUTATSUGI Kokichi
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...
Keiichirou Kusakari,Masaki Nakamura,Yoshihito Toyama
J. Autom. Reasoning   37(3) 205-229   2006   [Refereed]
Masahiro Nakano,Kazuhiro Ogata,Masaki Nakamura,Kokichi Futatsugi
Sixth International Conference on Quality Software (QSIC 2006), 26-28 October 2006, Beijing, China   49-56   2006   [Refereed]
NAKAMURA MASAKI, OGATA KAZUHIRO, FUTATSUGI KOKICHI
情報処理学会論文誌. プログラミング   46(25)    Apr 2005   [Refereed]
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...
NAKAMURA MASAKI, OGATA KAZUHIRO, FUTATSUGI KOKICHI
46(6)    Apr 2005   [Refereed]
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...
Kazuhiro Ogata,Masahiro Nakano,Masaki Nakamura,Kokichi Futatsugi
Sixth International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2005), 5-8 December 2005, Dalian, China   416-420   2005   [Refereed]
Masaki Nakamura,Kazuhiro Ogata
Electr. Notes Theor. Comput. Sci.   36 212-228   2000   [Refereed]
NAKAMURA Masaki, KUSAKARI Keiichirou, TOYAMA Yoshihito
The transactions of the Institute of Electronics, Information and Communication Engineers. D-I   82(10) 1225-1231   Feb 1999   [Refereed]
Kusakari Keiichirou, Nakamura Masaki, Toyama Yoshihito
Research report   99(0) 1-14   Mar 1999   [Refereed]

Misc

 
ISHIURA Nagisa, MAKINO Mitsunori, USAMII Kimiyoshi, YAMADA Isao, HIRAISHI Kunihiko, YAMAGUCHI Shingo, NAKAMURA Masaki
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...
NAKAMURA Masaki, YAMASAKI Tatsushi, YAMAGUCHI Shingo, MIYAMOTO Toshiyuki, UCHIHIRA Naoshi
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...
YAMAGUCHI Shingo, NAKAMURA Masaaki
IEICE ESS Fundamentals Review   4(4) 322b-324   2011
SEINO Takahiro, NAKAMURA Masaki
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...
中村 正樹, 緒方 和博, 二木 厚吉
電子情報通信学会総合大会講演論文集   2010(0) "S-27"-"S-28"   Mar 2010
中村 正樹, 山崎 達志, 山口 真悟, 宮本 俊幸, 内平 直志
電子情報通信学会総合大会講演論文集   2010(0) "S-29"-"S-30"   Mar 2010
NAKAMURA Masaki, SEINO Takahiro
Technical report of IEICE. SS   107(392) 25-30   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 ...
HARA Koutaro, OGATA Kazuhiro, NAKAMURA Masaki, FUTATSUGI Kokichi
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...
Nakamura Masaki, Futatsugi Kokichi
情報科学技術レターズ   3(0) 13-14   Aug 2004
Watanabe Masahiro, Nakamura Masaki, Futatsugi Kokichi
情報科学技術フォーラム一般講演論文集   3(1) 173-174   Aug 2004
Hara Kotaro, Ogata Kazuhiro, Nakamura Masaki, Futatsugi Kokichi
情報科学技術フォーラム一般講演論文集   3(1) 177-178   Aug 2004
Asaba Yoshiyuki, Nakamura Masaki, Amano Noriki, Fuatsugi Kokichi
情報科学技術フォーラム一般講演論文集   2002(1) 89-90   Sep 2002
NAKANO Masahiro, NAKAMURA Masaki, OGATA Kazuhiro, FUTATSUGI Kokichi
情報科学技術フォーラム一般講演論文集   2002(1) 91-92   Sep 2002
Nakamura Masaki, Futatsugi Kokichi
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...
Nakamura Masaki, Toyama Yoshihito
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,...

Conference Activities & Talks

 
秋葉健人, 中大輔, 榊原一紀, 中村正樹, 吉本達郎, 濱貴子
計測自動制御学会システム・情報部門学術講演会講演論文集(CD-ROM)   25 Nov 2017   
尾山武史, 青木真一郎, 榊原一紀, 中村正樹, 松本卓也, 大原誠
計測自動制御学会システム・情報部門学術講演会講演論文集(CD-ROM)   25 Nov 2017   
尾山武史, 青木真一郎, 榊原一紀, 中村正樹, 松本卓也, 大原誠
電気学会電子・情報・システム部門大会講演論文集(CD-ROM)   6 Sep 2017   
安藤 大貴, 中村 正樹, 榊原 一紀
システム制御情報学会研究発表講演会講演論文集   23 May 2017   
森隆晴, 中村正樹
電子情報通信学会大会講演論文集(CD-ROM)   7 Mar 2017   

Research Grants & Projects

 
Ministry of Education, Culture, Sports, Science and Technology: Grants-in-Aid for Scientific Research(基盤研究(B))
Project Year: 2006 - 2009    Investigator(s): Kokichi FUTATSUGI
"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 ...
Ministry of Education, Culture, Sports, Science and Technology: Grants-in-Aid for Scientific Research(若手研究(B))
Project Year: 2006 - 2008    Investigator(s): Masaki NAKAMURA
Ministry of Education, Culture, Sports, Science and Technology: Grants-in-Aid for Scientific Research(基盤研究(B))
Project Year: 2003 - 2005    Investigator(s): Kokichi FUTATSUGI
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...
Ministry of Education, Culture, Sports, Science and Technology: Grants-in-Aid for Scientific Research(特定領域研究(B), 特定領域研究)
Project Year: 2000 - 2003    Investigator(s): Kokichi FUTATSUGI
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...