中村正樹 更新日: 18/12/18 11:52
研究キーワード
システム検証(5) ,
振舞仕様(1) ,
形式手法(37) ,
システム安全性(1) ,
CafeOBJ(1) ,
問題モデル(1) ,
項書換システム(1) ,
ソフトウェア工学(211) ,
項書き換えシステム(5) ,
証明スコア(1) ,
代数仕様(2) ,
認証プロトコル(1) ,
検証システム(1) ,
フォーマルメソッド(3) ,
モジュールシステム(1) ,
安全性・信頼性(4) ,
要求仕様(2) ,
検証(6) ,
帰納法(1) 経歴
2017年4月
-
現在
富山県立大学 電子・情報工学科 准教授
2011年
-
2017年
富山県立大学 情報システム工学科 講師
2008年
-
2011年
金沢大学 電子情報学類 助教
2007年
-
2008年
北陸先端科学技術大学院大学 情報科学研究科 助教
2003年
-
2007年
北陸先端科学技術大学院大学 情報科学研究科 助手
論文
浅井康平, 榊原一紀, 中村正樹
進化計算学会論文誌 9(2) 53-60 2018年 [査読有り]
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年 [査読有り]
ヒューマンインタフェース学会論文誌 The transactions of Human Interface Society 18(1) 133-140 2016年 [査読有り]
浦島智，鳥山朋二，中村正樹，中川美都子，大島淳一，吉野修，野村忠雄
電子情報通信学会論文誌D J99-D(2) 224-231 2015年 [査読有り]
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年 [査読有り]
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年 [査読有り]
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年 [査読有り]
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年 [査読有り]
Min Zhang 0002,Kazuhiro Ogata,Masaki Nakamura
IEICE Transactions 94-D(5) 976-988 2011年 [査読有り]
Masaki Nakamura,Kazuhiro Ogata,Kokichi Futatsugi
J. Symb. Comput. 45(5) 551-573 2010年 [査読有り]
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年 [査読有り]
緒方和博, 二木厚吉, 中村正樹
コンピュータソフトウェア 26(1) 71-83 2009年12月 [査読有り]
代数仕様言語CafeOBJによる認証プロトコルの検証の例を示す.NSLPK認証プロトコルは,公開鍵暗号方式に基づく,2つの主体間の相互認証のためのプロトコルである.NSLPK認証プロトコルに定められたメッセージ送受信を終えると,2つの主体はある情報を共有する.その情報が,たとえ悪意のある主体が存在していたとしても第三者にもれることはない,という性質を秘匿性という.NSLPK認証プロトコルが秘匿性を満たすことの証明譜による検証を解説する.
中村 正樹, El-Nashar Alaa Ismail, 二木 厚吉
情報科学技術フォーラム講演論文集 8(1) 85-92 2009年8月 [査読有り]
NAKAMURA Masaki, OGATA Kazuhiro, FUTATSUGI Kokichi
IEICE transactions on information and systems E92-D(7) 1401-1411 2009年7月 [査読有り]
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 2009年5月 [査読有り]
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...
緒方 和博, 二木 厚吉, 中村 正樹
コンピュータソフトウェア 26(2) 93-106 2009年4月 [査読有り]
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...
緒方 和博, 二木 厚吉, 中村 正樹
コンピュータ ソフトウェア 26(1) 71-83 2009年 [査読有り]
代数仕様言語CafeOBJによる認証プロトコルの検証の例を示す．NSLPK認証プロトコルは，公開鍵暗号方式に基づく，2つの主体間の相互認証のためのプロトコルである．NSLPK認証プロトコルに定められたメッセージ送受信を終えると，2つの主体はある情報を共有する．その情報が，たとえ悪意のある主体が存在していたとしても第三者にもれることはない，という性質を秘匿性という．NSLPK認証プロトコルが秘匿性を満たすことの証明譜による検証を解説する．
中村正樹, 二木厚吉, 緒方和博
コンピュータソフトウェア 25(3) 69-80 2008年7月 [査読有り]
等式推論は代数仕様言語CafeOBJの最重要の推論機構である.等式推論の効率的な実行を可能とする項書換システムについて,CafeOBJ仕様の作成の助けとなる知識に焦点を当てて解説する.項書換システムの停止性,合流性,十分完全性などの基本的性質を満たす仕様作成の指針を示し,AC演算子属性,条件付き等式などを含む仕様への適用を議論する.
NAKAMURA Masaki, KONG Weiqiang, OGATA Kazuhiro, FUTATSUGI Kokichi
IEICE transactions on information and systems E91-D(5) 1492-1503 2008年5月 [査読有り]
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...
二木厚吉, 緒方和博, 中村正樹
コンピュータソフトウェア 25(2) 1-13 2008年4月 [査読有り]
CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,...
中村正樹, 二木厚吉, 緒方和博
コンピュータソフトウェア 25(2) 14-27 2008年4月 [査読有り]
代数仕様言語CafeOBJは,柔軟なmix-fix構文,部分型をともなった強力な型システム,数種類の輸入,パラメータ化モジュール,ビューによるパラメータの具現化などを持つ洗練されたモジュールシステムなどの特徴を持つ.CafeOBJ仕様は代数を意味する.代数は,抽象データ型や抽象機械などの現実のシステムの記述に有効なモデルを包含する汎用性のあるモデル化の枠組みであり,形式仕様の作成と検証を統一的に扱うことができる.本論文では,代数仕様言語CafeOBJの構文および意味について解説する.またC...
緒方和博, 中村正樹, 二木厚吉
コンピュータソフトウェア 25(2) 78-84 2008年4月 [査読有り]
二木厚吉, 緒方和博, 中村正樹
コンピュータソフトウェア 25(4) 68-84 2008年2月 [査読有り]
証明譜を用いた簡約のみに基づくCafeOBJの検証法を解説する.待ち行列を用いる相互排除プロトコルQlockの相互排除性の検証を例として,証明譜を用いた検証法の原理や仕組みを説明するとともに,証明譜の記述の技法も解説する.
二木 厚吉, 緒方 和博, 中村 正樹
コンピュータ ソフトウェア 25(4) 68-84 2008年 [査読有り]
証明譜を用いた簡約のみに基づくCafeOBJの検証法を解説する．待ち行列を用いる相互排除プロトコルQlockの相互排除性の検証を例として，証明譜を用いた検証法の原理や仕組みを説明するとともに，証明譜の記述の技法も解説する．
緒方 和博, 中村 正樹, 二木 厚吉
コンピュータ ソフトウェア 25(2) 78-84 2008年 [査読有り]
二木 厚吉, 緒方 和博, 中村 正樹
コンピュータ ソフトウェア 25(2) 1-13 2008年 [査読有り]
CafeOBJ言語システムを用いた形式手法，すなわち形式仕様の作成法と検証法，を全6回にわたり解説する．CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり，振舞仕様，書換仕様，パラメータ化仕様などが記述できる最先端の形式仕様言語である．CafeOBJ言語システムは，等式を書換規則として実行することで等式推論を健全にシミュレートすることができ，対話型検証システムとして利用出来る．<BR>第1回の今回は，「待ち行列を用いる相互排除プロトコル」を例題として，言語や検証法の細部に立ち入るこ...
中村 正樹, 二木 厚吉
情報科学技術レターズ 6(0) 27-30 2007年8月 [査読有り]
Masahiro Nakano,Kazuhiro Ogata,Masaki Nakamura,Kokichi Futatsugi
International Journal of Software Engineering and Knowledge Engineering 17(6) 783-804 2007年 [査読有り]
Masaki Nakamura,Kokichi Futatsugi
Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings 381-395 2007年 [査読有り]
中村正樹, 二木厚吉
コンピュータソフトウェア 23(3) 35-50 2006年7月 [査読有り]
モジュラーな代数仕様言語であるOBJ言語族は,モジュールをベースとした仕様記述スタイルを提供しており,組み込みのモジュールや過去に記述したモジュールの再利用などにより大規模で複雑なシステムの仕様記述に効果的である.一方,等式の集合を公理とするOBJ言語族の検証は,等式を書き換え規則と見なす項書き換えシステムによる等式推論をベースに行われるが,モジュールシステムによる洗練された仕様記述に比べ,仕様検証ではモジュールシステムの利点が活かされているとは言えない.本論文では,モジュラーな代数仕様言...
NAKAMURA Masaki, WATANABE Masahiro, FUTATSUGI Kokichi
IEICE transactions on fundamentals of electronics, communications and computer sciences E89-A(6) 1558-1565 2006年6月 [査読有り]
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年 [査読有り]
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年 [査読有り]
中村 正樹, 緒方 和博, 二木 厚吉
情報処理学会論文誌. プログラミング 46(25) 2005年4月 [査読有り]
項書き換えシステムでは, 書き換え規則の適用によって簡約できる項は可約項と呼ばれる.本研究では, この可簡約の概念を演算子に適用し, 可簡約演算子の性質を明らかにする.可簡約演算子とは, その演算子を含む項が可簡約であることと定義する.項は演算子をノードに持つ木構造であり, 項の簡約のしくみには演算子間の区別はない.しかし通常, システムの記述者はモデル上の要素を構成する構成子とその上の関数を表す演算子を区別して考える.可簡約演算子とは, 後者の関数としての演算子が持つべき性質である.本研...
中村正樹, 緒方和博, 二木厚吉
情報処理学会論文誌. プログラミング 46(6) 2005年4月 [査読有り]
項書き換えシステムでは, 書き換え規則の適用によって簡約できる項は可約項と呼ばれる.本研究では, この可簡約の概念を演算子に適用し, 可簡約演算子の性質を明らかにする.可簡約演算子とは, その演算子を含む項が可簡約であることと定義する.項は演算子をノードに持つ木構造であり, 項の簡約のしくみには演算子間の区別はない.しかし通常, システムの記述者はモデル上の要素を構成する構成子とその上の関数を表す演算子を区別して考える.可簡約演算子とは, 後者の関数としての演算子が持つべき性質である.本研...
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年 [査読有り]
Masaki Nakamura,Kazuhiro Ogata
Electr. Notes Theor. Comput. Sci. 36 212-228 2000年 [査読有り]
Kusakari Keiichirou, Nakamura Masaki, Toyama Yoshihito
Research report 99(0) 1-14 1999年3月 [査読有り]
中村正樹, 草刈圭一朗, 外山芳人
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理 82(10) 1225-1231 1999年2月 [査読有り]
従来の停止性判定法を適用できない項書換え系(TRS)の停止性を示すために,Ferreiraは一般消去法を提案した.一般消去法は,規則に現れる適当な関数記号を消去することでより単純な構造のTRSに変換する.変換後のTRSの停止性がもとのTRSの停止性を保証するため,停止性判定に有効である.一方,ArtsとGieslは,TRSの規則に現れる関数定義記号の出現に注目し,無限書換え列の本質を簡潔に記述できる依存対の概念を導入した.本論文では,一般消去法が変換後に付け加える規則に注目し,不必要な規則...
Misc
石浦 菜岐佐, 牧野 光則, 宇佐美 公良, 山田 功, 平石 邦彦, 山口 真悟, 中村 正樹
電子情報通信学会技術研究報告. SIP, 信号処理 111(104) 2011年6月
システムと信号処理サブソサイエティ4研専は,平成22年から合同研究会を開催している.合同研究会の意味をより深めるために,サブソ会長を座長に,各研専委員長または各研専の代表者をパネラーとしたパネルディスカッションを開催する.近年のICT技術の発展は,システムの高機能化・高信頼化・高安全性を実現したが,一方で大規模・複雑化し,高度なシステム・信号処理技術が必要となっている.システムと信号処理サブソサイエティの4研専は,システム・信号処理技術の基礎を支える研専として相補的な関係にある.そこで,お...
中村 正樹, 山崎 達志, 山口 真悟, 宮本 俊幸, 内平 直志
電子情報通信学会技術研究報告. CST, コンカレント工学 110(370) 1-4 2011年1月
マルチカーエレベータ(以降,MCEと略す)は一つのシャフト内に複数のかごを設けたエレベータである.本コンペでは2台以上のかごを設けたMCEの制御器(プログラム)を開発することを課題とする.マルチカーエレベータの最適制御を究めるべく,これまでのコンペ(CSTコンペ2007,CSTコンペ2008)の課題で開発対象となっていた群制御器に加え,今回はさらにシャフト制御器も開発対象とする.
山口 真悟, 中村 正樹
電子情報通信学会 基礎・境界ソサイエティ Fundamentals Review 4(4) 322b-324 2011年
清野 貴博, 中村 正樹
電子情報通信学会技術研究報告. CST, コンカレント工学 110(161) 7-12 2010年7月
形式仕様によるシステムの記述と、プログラミング言語によるソフトウェアの実装には隔たりがあるが、これを克服するために、筆者らは形式仕様の検証を元にテストスイートを生成し、テスト駆動による開発へ持ち込む手法を提案している。本稿では、提案済みの手法を発展させ、形式仕様を元に複数のオブジェクトから成る実装や並行実行を意識した実装を得る手法と、そのコードをテストするテストスイートの生成手法を提案する。
中村 正樹, 緒方 和博, 二木 厚吉
電子情報通信学会総合大会講演論文集 2010(0) "S-27"-"S-28" 2010年3月
中村 正樹, 山崎 達志, 山口 真悟, 宮本 俊幸, 内平 直志
電子情報通信学会総合大会講演論文集 2010(0) "S-29"-"S-30" 2010年3月
中村正樹, 清野貴博
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 107(392) 25-30 2007年
OTS/CafeOBJ法では,形式仕様言語CafeOBJで仕様を作成し,証明譜と呼ばれる検証スクリプトにより仕様の形式的な検証を行う.本研究では,OTS/CafeOBJ仕様およびその証明譜からのテスト生成手法を提案する.提案するテスト生成手法では,証明譜に含まれる場合分けなどの情報を指針として適切なテストを与える.生成されたテストは,実装が仕様および検証された性質を満たすかどうかを検査する.
中村正樹, 孔維強, 緒方和博, 二木厚吉
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 106(120) 1-6 2006年6月
代数仕様言語を用いて状態遷移機械を記述する手法に,振舞仕様に基づく観測遷移機械(OTS)による手法と書き換え論理に基づく書き換え仕様による手法がある.それぞれ記述言語としてCafeOBJおよびMaudeを持ち,各手法で異なる検証スタイルを持つ.本研究では,2つの異なる検証手法を統合した検証システムの構築のため,OTS/CafeOBJ仕様からMaude書き換え仕様への変換について考察する.
原光太朗, 緒方和博, 中村正樹, 二木厚吉
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 104(570) 1-6 2005年11月
形式手法により検証を行う技法は広く研究され, これまでに多くの方法が提案されてきた.しかし, 方法の提案や実例を扱う研究に比べ, その比較を扱う研究はあまり行われておらず, その結果, 形式手法を用いる際のガイドラインがないという問題点が存在する.本稿では, セキュリティプロトコルの一つであるSTSプロトコルを例題として取り上げ, 異なる二つの形式手法として, CafeOBJを用いる方法とCoqを用いる方法の双方で安全性等の検証を行う.この具体例を通して, 双方によるシステムの形式化および...
中村 正樹, 二木 厚吉
情報科学技術レターズ 3(0) 13-14 2004年8月
渡辺 真啓, 中村 正樹, 二木 厚吉
情報科学技術フォーラム一般講演論文集 3(1) 173-174 2004年8月
原 光太朗, 緒方 和博, 中村 正樹, 二木 厚吉
情報科学技術フォーラム一般講演論文集 3(1) 177-178 2004年8月
浅羽 義之, 中村 正樹, 天野 憲樹, 二木 厚吉
情報科学技術フォーラム一般講演論文集 2002(1) 89-90 2002年9月
中野 昌弘, 中村 正樹, 緒方 和博, 二木 厚吉
情報科学技術フォーラム一般講演論文集 2002(1) 91-92 2002年9月
中村正樹, 二木厚吉
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 100(569) 17-23 2001年11月
文脈依存書き換え(csr)とは, 関数記号の各引数に対して書き換え可能かどうかを定義することで形式化される制限付き書き換え関係である.現行のcsrにおいては, 引数に対する書き換え可能性の指定は, 常に可能か常に不可能かのどちらかしか定義できない.本論分で提案する遅延評価機能を伴った文脈依存書き換え(ocsr)は, 引数に対して必要に応じて書き換え可能にもなり, また別の場面では書き換え不可能にもなる新たな属性を付け加えた.これにより従来のcsrではうまく表現できなかった柔軟性のある制限が...
中村正樹, 外山芳人
電子情報通信学会技術研究報告. COMP, コンピュテーション 98(432) 57-64 1998年12月
従来の停止性判定法を適用できない項書換えシステム(TRS)の停止性を示すために, Ferreiraは一般消去法を提案した.一般消去法は, 規則に現れる適当な関数記号を消去することでより単純な構造のTRSに変換する.変換後のTRSが停止性を持つならば元のTRSも停止性を持つという性質があるため, 一般消去法は停止性判定に有効である.一方, ArtsとGieslは, TRSの規則に現れる関数定義記号の出現に注目し, 無限書換え列の本質を簡潔に記述できる依存対の概念を導入した.本稿では, 一般消...
講演・口頭発表等
秋葉健人, 中大輔, 榊原一紀, 中村正樹, 吉本達郎, 濱貴子
計測自動制御学会システム・情報部門学術講演会講演論文集(CD-ROM) 2017年11月25日
尾山武史, 青木真一郎, 榊原一紀, 中村正樹, 松本卓也, 大原誠
計測自動制御学会システム・情報部門学術講演会講演論文集(CD-ROM) 2017年11月25日
尾山武史, 青木真一郎, 榊原一紀, 中村正樹, 松本卓也, 大原誠
電気学会電子・情報・システム部門大会講演論文集(CD-ROM) 2017年9月6日
安藤 大貴, 中村 正樹, 榊原 一紀
システム制御情報学会研究発表講演会講演論文集 2017年5月23日
森隆晴, 中村正樹
電子情報通信学会大会講演論文集(CD-ROM) 2017年3月7日
競争的資金等の研究課題
文部科学省: 科学研究費補助金(基盤研究(B))
研究期間: 2006年 - 2009年 代表者: 二木厚吉
「帰納法」と「場合分け」は、問題モデル(問題領域や応用領域におけるモデル)の証明スコアによる検証法の基本技術である。本研究では、多様な応用分野で有効な帰納法と場合分けについて以下の成果を得た。(1)帰納法をデータ型・プロセス型の帰納的な構造に基づき定式化した。(2)場合分けを構成子からの項の生成に基づき定式化した。(3)(1),(2)に基づき、汎用的な証明規則を定式化するとともに、推論と探索を融合した強力な検証法を開発した。
文部科学省: 科学研究費補助金(若手研究(B))
研究期間: 2006年 - 2008年 代表者: 中村正樹
本研究では, モジュラーな項書換えシステムに基づく仕様検証システムの開発を行った. これにより, 特に仕様作成, 実行, 検証時におけるデータ仕様の扱いが容易となり, 形式仕様言語の幅広い利用を促す研究成果が得られた. また, 仕様から実装を得るためのツールの開発, 異なる検証技術の融合技術, 検証エンジンの基礎理論など, ソフトウェア開発工程全体を取り扱うことが可能な形式仕様言語の構築へとつながる研究成果が得られた.
文部科学省: 科学研究費補助金(基盤研究(B))
研究期間: 2003年 - 2005年 代表者: 二木厚吉
安全性を重要な要件として問題モデル(問題領域や応用領域のモデル)を構築しそれを検証する技術は,21世紀のネットワーク社会において最重要のソフトウェア技術となりつつある.こうした技術は,ソフトウェア工学分野における,要求獲得技術,仕様技術,検証技術といったカテゴリに属するが,「安全性が議論できる程度に厳密に問題モデルを構築しかつ検証する技術」はいまだに確立されていない.本研究では,このような現状を打破すべく,研究代表者のグループが今まで研究成果を蓄積してきた振舞仕様技術に基づき,実用的な問題...
文部科学省: 科学研究費補助金(特定領域研究(B), 特定領域研究)
研究期間: 2000年 - 2003年 代表者: 二木厚吉
一貫した論理体系に基づき,適応性と汎用性に優れ,かつ自動化の容易な安全性検証技術を実現することを目標に研究を進め,振舞仕様に基づく以下のような技術を開発した.(1)未知ウイルス検知技術:振舞仕様の理論的枠組に基いてプログラムの挙動をモデル化することで,プログラムの安全性(=ウイルスで「あること」ならびに「ないこと」の判定)を論理的に解析し,自動的に検知する枠組を提案し,処理系を作成した.具体的には,Microsoft社のWindows OS上のプログラムを対象として,未知ウィルス検知ソフト...
