研究活動

研究テーマ

• リアルタイム並行システムの仕様記述法および検証法に関する研究
• 上の基礎となる並行・分散システムのモデリングおよび セマンティクスに関する研究（プロセス代数，時相論理，True Concurrency, etc.）

業績リスト:

• Akio Nakata, Teruo Higashino and Kenichi Taniguchi: "LOTOS enhancements to specify time constraints among nonadjacent actions using 1st-order logic," In Formal Description Techniques, VI, pp.451-466, Elsevier Science Publishers B.V. (North-Holland), 1994. (presented at IFIP TC6/WG6.1 6th Int'l Conf. on Formal Description Techniques (FORTE'93), Boston, MA, USA, Oct. 1993)
  [Abstract]
• Teruo Higashino, Akio Nakata, Tatsuo Itoh and Kenichi Taniguchi : "Verification of Liveness Property for Communicating FSM's with Conditional Transitions depending on State Visiting Numbers", The 8th International Conference on Formal Description Techniques (FORTE'95), pp.433-440 (Oct. 1995).
• Akio Nakata, Teruo Higashino and Kenichi Taniguchi: "Protocol Synthesis from Timed and Structured Specifications," In Proc. of the 1995 Int'l Conf. on Network Protocols (ICNP'95), Tokyo, Japan, pp.74-81, IEEE Computer Society Press, Nov. 1995.
  [Abstract]
• 中田 明夫，東野 輝夫，谷口 健一：「隣接しない動作間の時間制約を 記述するためのLOTOS言語の拡張とその等価性の検証」, コンピュータソフトウェア, Vol.12, No.6, pp.3-16, 1995-11.
• 中田 明夫，東野 輝夫，谷口 健一：「時間制約の記述されたLOTOS仕様からの プロトコル合成」,情報処理学会論文誌, Vol.37, No.5, pp.672-685, 1996-05.
• Akio Nakata, Teruo Higashino and Kenichi Taniguchi: "Time-Action Alternating Model for Timed LOTOS and its Symbolic Verification of Bisimulation Equivalence", in Proc. of IFIP TC6/WG6.1 Joint Int'l Conf. on Formal Description Technique for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'96), Kaiserslautern, Germany , Chapman&Hall, pp.279-294, Oct. 1996.
  [Abstract]
• Akio Nakata: "Symbolic Bisimulation Checking and Decomposition of Real-Time Service Specifications", Ph.D. thesis, Osaka University, Jan. 1997.
• Akio Nakata, Teruo Higashino and Kenichi Taniguchi: "Time-Action Alternating Model for Timed Processes and its Symbolic Verification of Bisimulation Equivalence", IEICE Trans. on Fundamentals, Vol. E80-A, No. 2, pp.400-406, Feb. 1997.
• 水野 健太郎, 中田 明夫, 岡野 浩三, 東野 輝夫, 谷口 健一 : 「遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に 対する生存性の検証」, 情報処理学会論文誌, Vol. 39, No. 3, pp.750-759, 1998-03.
• Akio Nakata, Teruo Higashino and Kenichi Taniguchi: "Protocol Synthesis from Context-Free Processes using Event Structures", in Proc. of 5th Int'l Conf. on Real-Time Computing Systems and Applications (RTCSA'98), Hiroshima, Japan, IEEE Computer Society Press, pp.173-180, Oct. 1998.
  [Abstract]
• 深田 敦史，中田 明夫，東野 輝夫，谷口 健一： 「あるクラスの時間オートマトンに対する適合性試験系列生成の一手法」， 情報処理学会論文誌，Vol. 40，No.1，pp.85-94（平11-01）．
• Teruo Higashino, Akio Nakata, Kenichi Taniguchi and Ana R. Cavalli: "Generating Test Cases for a Timed I/O Automaton Model", in Proc. of 12th IFIP Int'l Work.Conf. on Testing of Communicating Systems (IWTCS'99), Budapest, Hungary, Kluwer Academic Publishers, Sept. 1999.
• 松岡 宏樹，中田 明夫，大場 充：「CCS仕様からのJavaソースコード自動生成 プログラムの作成と評価」， 平成１１年度電気・情報関連学会中国支部連合大会論文集，pp.4-5, 1999-10.
• 新子 浩康，中田 明夫，大場 充：「実時間システムの動作仕様と要求仕様からの パラメータ条件導出」，平成１１年度電気・情報関連学会中国支部連合大会論文集， pp.239-240, 1999-10.
• 中田 明夫，服部 哲，東野 輝夫，谷口 健一： 「時間制約と入出力データに関する条件判定が同時に記述できる オートマトンモデルとその双模倣等価性検証法」，第7回 マルチメディア通信と分散処理ワークショップ論文集， 情報処理学会シンポジウムシリーズ，Vol.99, No.18, pp. 37-42, 1999-12.
• 新子 浩康，中田 明夫，大場 充：「時相論理式を満足する 実時間プロトコル仕様のパラメータ条件導出」，第97回マルチメディア通信と 分散処理研究会，2000-03.
• 中田 明夫，服部 哲，東野 輝夫，谷口 健一：「データ付時間オートマトンの双模 倣等価性の記号的検証法」，情報処理学会論文誌，Vol. 41, No. 9, pp.2487-2497, 2000-09．
• Atsushi Fukada, Akio Nakata, Junji Kitamichi, Teruo Higashino and Ana Cavalli: "A Conformance Testing Method for Communication Protocols Modeled as Concurrent DFSMs -Treatment of Non-observable Non-determinism-", Proceedings of 15th International Conference on Information Networking (ICOIN-15), 2000-12, pp.155-162.
• Akio Nakata: "Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas", 計算理論とアルゴリズムの新展開(冬のLAシンポジウム2001), 京都大学数理解析研究所考究録 No.1205, pp.160-165, 2001.
• Teruo Higashino, Hirozumi Yamaguchi, Akio Nakata and Keiichi Yasumoto: "Perspectives in Developing Distributed Cooperative Systems", Proceedings of 2nd International Conference on Software Engineering, Artificial Intelligence, Networking & Parallel/Distributed Computing, 2001-07, pp.xi-xix (Invited Paper).
• Akio Nakata and Teruo Higashino: "Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas", Proc. of IFIP TC6/WG6.1 Int'l Conf. on Formal Techniques for Networked and Distributed Systems(FORTE2001), Cheju Island, Korea, Kluwer Academic Publishers, pp.151-166, Aug. 2001.
  [Abstract]
• Masakazu Fujii, Nobuo Funabiki, Shigeto Tajima, Akio Nakata, Tokumi Yokohira and Teruo Higashino: "An Optimal Path Selection Algorithm for Static and Mobile Multicast Routing Problems", Proceedings of IEEE 16th International Conference on Information Networking(ICOIN-16), 2001-12, pp.6B2.1-2.10.
• Makoto Yamada, Takanori Mori, Atsushi Fukada, Akio Nakata and Teruo Higashino: "A Method for Functional Testing of Media Synchronization Protocols", Proceedings of IEEE 16th International Conference on Information Networking(ICOIN-16), 2001-12, pp.539-550.
• 安本 慶一，中田 明夫，寺島 芳樹，梅津 高朗，東野 輝夫，谷口 健一： 「マルチランデブチャネルの動的確立機構を持つ モバイルアプリケーション記述言語の提案」， コンピュータソフトウェア, Vol.19, No.2, 2002-02, pp.35-46.
• Takaaki Umedu, Hirozumi Yamaguchi, Keiichi Yasumoto, Akio Nakata and Teruo Higashino: "A Constraint-Oriented Design Method for Distributed Cooperative Systems and Efficient Verification Using Symmetries", International Journal of Computer and Information Science, Vol. 3,No. 2, 2002-05, pp. 125-136.
• Takaaki Umedu, Yoshiki Terashima, Keiichi Yasumoto, Akio Nakata,Teruo Higashino and Kenichi Taniguchi: "A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels", Proceedings of the 11th International Conference on Formal Methods Europe (FME2002), Lecture Notes in Computer Science, Vol.2391, 2002-06,pp.607-624.
• Masayuki Kirimura, Yoshifumi Takamoto, Takanori Mori, Keiichi Yasumoto, Akio Nakata and Teruo Higashino: "Design and Implementation of FPGA Circuits for High Speed Network Monitors", Proceedings of the 12th International Conference on Field Programmable Logic and Applications (FPL 2002), Lecture Notes in Computer Science, Vol.2438, 2002-08, pp. 393-403.
• Takaaki Umedu, Keiichi Yasumoto, Akio Nakata, Hirozumi Yamaguchi and Teruo Higashino: "Middleware for Synchronous Group Communication in Wireless Ad Hoc Networks", Proceedings of the International Conference on Communications and Computer Networks 2002 (CCN 2002), 2002-10, pp. 48-53.
• 森 亮憲，大塚 裕孝，舩曵 信生，中田 明夫，東野 輝夫： 「通信プロトコルの試験系列生成問題に対するSATアルゴリズム適用法の提案」， 電子情報通信学会論文誌 D-I,Vol.J85-D-I,No.11, 2002-11,pp.1038-1046.
• Keiichi Yasumoto, Takaaki Umedu, Hirozumi Yamaguchi, Akio Nakata and Teruo Higashino: "Protocol Animation based on Event-driven Visualization Scenarios in Real-time LOTOS", Computer Networks,Vol.40,No.5, 2002-11, pp. 639-663.
• 森 亮憲，中田 明夫，東野 輝夫： 「並行周期EFSMに対するパラメトリックモデル検査手法」， 電子情報通信学会論文誌 D-I,Vol.J86-D-I,No.2, 2003-02,pp.75-87.
• 桐村　昌行，高本　佳史，森　亮憲，安本　慶一，中田　明夫，東野　輝夫： 「高速ネットワーク向けネットワークモニタ回路の設計と実装」， 情報処理学会論文誌,Vol.44,No.6, 2003-05,pp.1593-1603.
• Takanori Mori, Akio Nakata and Teruo Higashino: "Design of Media Synchronization Protocols using Parametric Model Checking and Functional Testing", Proceedings of the 2003 International Workshop on Testing Real-Time and Embedded Systems (WTRTES 2003), 2003-08.
• Tomoya Kitani, Yoshifumi Takamoto, Isao Naka, Keiichi Yasumoto, Akio Nakata and Teruo Higashino: "Design and Implementation of Priority Queuing Mechanism on FPGA using Concurrent Periodic EFSMs and Parametric Model Checking", Proceedings of the 13th International Conference on Field Programmable Logic and Applications (FPL 2003), pp. 1145-1148, 2003-09.
• Takanori Mori, Akio Nakata, and Teruo Higashino, "A Method for Designing Multimedia Protocols using Both Parametric Model Checking and Functional Testing", STUDIA INFORMATICA UNIVERSALIS, Vol. 3, No. 2, pp.203-230, Apr. 2004.
• Harry D. Foster, Adam C. Krolnik, and David J. Lacey著： "Assertion-Based Design Second Edition", 東野 輝夫, 岡野 浩三, 中田 明夫 監訳：「アサーションベース設計」, 丸善, p.532, 2004-09.
• 梅津 高朗，安本慶一，中田 明夫，東野 輝夫，「マルチランデブに基 づくグループ通信機能を提供するJavaミドルウェアの提案」，情報処理学会論 文誌，Vol. 45, No. 11, pp.2519-2527, 2004-11.
• Tadaaki Tanimoto, Suguru Sasaki, Akio Nakata, and Teruo Higashino: "A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata", Proc. of 2nd Int'l Symp. on Automated Technology for Verification and Analysis (ATVA2004), Taipei, Taiwan, Vol. 3299 of Lecture Notes in Computer Science, Springer-Verlag, pp.179-195, Nov. 2004.
• Tomoya Kitani, Yoshifumi Takamoto, Keiichi Yasumoto, Akio Nakata, and Teruo Higashino, "A Flexible and High-Reliable HW/SW Co-Design Method for Real-Time Embedded Systems," Proceedings of the 25th IEEE International Real-Time Systems Symposium(RTSS2004), pp. 437-446, Dec. 2004.
• Takaaki Umedu, Shigeharu Urata, Akio Nakata, and Teruo Higashino, "Automatic Decomposition of Java Program for Implementation on Mobile Terminals," Proceedings of the IEEE 19th International Conference on Advanced Information Networking and Applications(AINA2005), pp. 544-549, Mar. 2005.
• 木谷 友哉, 高本 佳史, 安本 慶一, 中田 明夫, 東野 輝夫, 「リアル タイム組込みシステムを対象とした高信頼性ハードウェア設計のための一手法」, 電子情報通信学会論文誌(A), Vol. J88-A, No. 12, pp. 1487-1496, 2005.
• Tadaaki Tanimoto, Akio Nakata, Hideaki Hashimoto, and Teruo Higashino: "Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata", IEICE Trans. on Fundamentals, Vol. E88-A, No. 11, pp.3007-3021, Nov. 2005.
• 谷本 匡亮，北口 智，中田 明夫，東野 輝夫：「バス通信構造のリファイン メントにおけるシミュレーションモデルの変更を容易化したバスシステム設計支援ツー ルの提案」，情報処理学会論文誌, Vol.47, No.3, pp.884-896, 2006.
• Tadaaki Tanimoto, Seiji Yamaguchi, Akio Nakata, and Teruo Higashino: "A Real Time Budgeting Method for Module-Level-Pipelined Bus Based System using Bus Scenarios", Proceedings of the 43rd ACM/IEEE International Design Automation Conference (DAC2006), pp.37-42, Jul. 2006.
• Akio Nakata, Tadaaki Tanimoto, Suguru Sasaki, and Teruo Higashino, "A Timed Failure Equivalence Preserving Abstraction for Parametric Time-Interval Automata", International Journal of Foundations of Computer Science, Vol. 17, No.4, pp.833-850, 2006.
• 河井 敏宏，中田 明夫：「実時間ソフトウェア再利用のためのパラメトリック 実行時間解析の一手法」， 電子情報通信学会技術研究報告(ソフトウェアサイエンス SS), Vol.107, No. 505, pp.97-102, 2008.
• 中田 明夫：「時間オートマトンのモデル検査」(招待論文)， 電子情報通信学会論文誌(和文誌D分冊), Vol.J92-D, No. 5, pp.576-586, 2009.
• 中田 明夫：「時間オートマトンによる実時間システムの形式的検証」 (解説論文)， 計測と制御, Vol.48, No. 11, pp.803-809, 計測自動制御学会, 2009.
• 百々 太市，山脇 弘，中田 明夫： 「リソーススケジューリングを考慮したUML MARTE振る舞い仕様の性能検証」， 情報処理学会研究報告(システムLSI設計技術 SLDM), Vol.2010-SLDM-144, No. 35, pp.1-8, 2010. (優秀発表学生賞)
• 百々 太市，中田 明夫： 「プリエンプティブスケジューリングによりリソースを共有する複数タスク動 作仕様の性能検証」， 情報処理学会 組込みシステムシンポジウム2010論文集, 2010.
• 椛島 和宏，中田 明夫： 「再帰を含むプログラムに対するパラメトリック実行時間解析手法とツールの 試作」， 電子情報通信学会技術研究報告(ソフトウェアサイエンス SS), Vol.111, No. 268, pp.37-42, 2011.
• 倉田 和哉，百々 太市，中田 明夫： 「リソース制約を持つ複数タスク動作仕様におけるタイムバジェット最適化の 一手法」， 電子情報通信学会技術研究報告(ソフトウェアサイエンス SS), Vol.111, No. 268, pp.43-48, 2011.
• 船瀬 広岐，中田 明夫： 「変数の生存期間を考慮してヒープメモリ使用量削減を行うマルチタスクスケジューリング手法の検討」， 電子情報通信学会技術研究報告(ソフトウェアサイエンス SS), Vol.112, No. 23, pp.7-12, 2012.
• 嘉戸 彰，中田 明夫： 「飛行船自動航行ソフトウェアの事例による設計段階でのスループット性能検証手法の評価」， 電子情報通信学会技術研究報告(ソフトウェアサイエンス SS), Vol.112, No. 23, pp.25-30, 2012.

トップページへ戻る

Last modified: Wed Sep 26 13:31:57 JST 2012