谷口健一 TANIGUCHI Kenichi

研究者番号	00029513
その他のID
所属 (現在)	2025年度: 大阪大学, その他部局等, 名誉教授
所属 (過去の研究課題情報に基づく) *注記	2006年度: 大阪大学, 名誉教授 2002年度 – 2004年度: 大阪大学, 大学院・情報科学研究科, 教授 1997年度 – 2001年度: 大阪大学, 大学院・基礎工学研究科, 教授 1986年度 – 1996年度: 大阪大学, 基礎工学部, 教授
審査区分/研究分野	研究代表者計算機科学 / 情報工学 / 情報工学研究代表者以外情報工学 / ソフトウエア / 理工系
キーワード	研究代表者代数的手法 / 実時間システム / 通信プロトコル / マルチランデブ / LOTOS / 設計検証 / レジスタ転送レベル / 検証 / 段階的詳細化 / 仕様記述 … もっと見る / OCL / UML / プレスブルガー文 / 時間オートマトン / SMIL / FDT / multi-rendezvous / VHDL / CAD / ASIC / コンパイラ / 分散システム / パイプラインCPU / 拡張有限状態機械 / 同期式順序回路 / 自動検証 / 設計自動化 / Petri-nets / Program Derivation / Timed Automaton / Sate-chart / Distributed Real-time System / Object-Oriented / 時間制約 / GUI / カラーペトリネット / プログラム自動導出 / 分散オブジェクト / Java / コンポーネントベースシステム / 分散マルチメディアシステム / 線形計画法 / Quality of Services / ペトリネット / プログラム導出 / ステートチャート / 分散実時間システム / オブジェクト指向 / Time-Action-Deadlock / Behavioral Level / Register Transfer Level / Verification Support System / Verification of Timeliness / Verification of Functional Properties / High-Leveled Design / CTL / 並列同期回路 / モデルチェッカー / 並列同期システム / 時間オートマトン群 / 時相論理式 / 整数変数つきFSM / 時間領域デッドロック / 動作仕様レベル / 検証支援システム / 時間性質の保証 / 機能性質の保証 / ハードウェア高位設計 / Presburger sentences / parallel control systems / parallel sequential machines / real-times systems / symbolic model checking / out-of-order pipelined CPU / Design and verification technique / out-of-order型パイプラインCPU / モデル検査 / 動的性質 / 並行システム / 順序機械 / プレスブルガー文真偽判定 / 並列制御部 / 並列動作順序回路 / 記号モデル検査 / Out-of-order CPU / QoS control / real-time systems / multi-thread / distributed systems / LOTOS compiler / マルチスレッド機構 / マルチメディア / E-LOTOS / 制約指向 / マルチメディアシステム / QoS制御 / マルチスレッド / LOTOSコンパイラ / High level synthesis / Register transfer level / Automatic curcuit synthesis / Hardware design / Protocol / 並行プロセス / ハードウェア化 / 形式記述技法 / 高位レベル合成 / 回路自動合成 / ハードウェア / State diagram transformation / Presburger sentence / Design verification / Stepwise refinement / Algebraic method / Synchronous sequential circuit / 形式的手法 / 機能設計 / グラフィカルユーザインタフェース / 高位合成 / 状態図変形 / プレスブルガ-文 / 設計支援 / 順序回路 / ハードウェア設計 / エラーリカバリ / プロトコル / イーサーネット / バス結合型ネットワーク / プレスブルガ-算術 / 形式的検証 / 分散実行 / プログラム自動合成 / ペトリネットモデル / プレスブルガ文 / 順序機械型プログラム / マイクロプログラム / ハ-ドウェア設計 / 証明書 / 証明支援システム / 証明 / 詳細化 … もっと見る研究代表者以外 OCL / ソフトウェアプロセス / Programmer's Capability / Bug Numbers / Measurement / プログラム作成能力 / ソフトウェア設計法 / バグ数 / ツール / ソフトウェア・メトリクス / Program Transformation / Adaptation Mechanism / Dynamic Compilation / Partial Computation / Reflection Mechanism / Meta-programming / Software Evolution / 環境適応機器 / プログラム変換 / 環境適応機構 / 動的翻訳機構 / 部分計算機構 / 自己反映機構 / メタプログラミング / ソフトウェア発展 / 確率時間オートマント / CEGAR LOOP / 表明 / モデル駆動開発 / フォーマルアプローチ / ソフトウェア / JML / CEGAR / 時間オートマトン / 形式手法 / モデル / モデル検査 / timelines QoS / UPPAAL / Struts / WEB / UML / SPIN / 関数型言語 / 並列分散言語 / 初心者支援 / 設計プロセス / フィードバックメカニズム / プログラム導出 / ソフトウエア構成プロセス / 開発プロセス制御 / プログラム導出プロセス / プロセス知識獲得 / プロセスの共通問題 / 定量的評価 / 代数的言語 / プログラム正当性 / 設計プロセス知識 / プロセス記述言語隠す

モデル検査技術を活用したソフトウェア設計方法に関する研究
- 研究代表者
  
  岡野浩三
- 研究期間 (年度)
  2009 – 2013
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  ソフトウエア
- 研究機関
  大阪大学
状態爆発するWEBアプリケーションに対するソフトウェアモデル検査
- 研究代表者
  
  岡野浩三
- 研究期間 (年度)
  2006
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  大阪大学
ハードウェアの高位設計・検証支援システム研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  2001 – 2004
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
オブジェクト指向型ソフトウェアの仕様記述と検証及び実行プログラム導出研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  2001 – 2004
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
並行動作順序回路システムの設計と検証に関する研究研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1999 – 2000
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
分散システム記述言語のコンパイラ研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1998 – 2000
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
ソフトウェア発展のための基本機構の研究
- 研究代表者
  
  武市正人
- 研究期間 (年度)
  1997 – 1999
- 研究種目
  
  重点領域研究
- 研究機関
  東京大学
通信プロトコルの形式仕様からのハードウェア回路合成研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1997 – 1998
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
マルチランデブを含むLOTOSプログラムの分散実行系の構築研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1996
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
複数の制御部をもつ同期式順序回路の機能検証に関する研究研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1995
- 研究種目
  
  一般研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
ペトリネット型実行制御部をもつ代数的仕様記述の検証と分散実行系研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1994
- 研究種目
  
  一般研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
代数的手法を用いたプログラムの階層的設計と開発環境に関する研究研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1993
- 研究種目
  
  一般研究(C)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
ASIC設計の上流工程設計支援システムの開発研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1993 – 1994
- 研究種目
  
  試験研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  大阪大学
ソフトウエア構成プロセスの記述とその実働化の研究
- 研究代表者
  
  鳥居宏次
- 研究期間 (年度)
  1992
- 研究種目
  
  重点領域研究
- 研究機関
  奈良先端科学技術大学院大学
ソフトウェア構成プロセスの記述とその実働化の研究
- 研究代表者
  
  鳥居宏次
- 研究期間 (年度)
  1990
- 研究種目
  
  重点領域研究
- 研究機関
  大阪大学
ハ-ドウェアの仕様記述とマイクロプログラムを用いた実現への段階的詳細化及び検証研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1990
- 研究種目
  
  一般研究(C)
- 研究分野
  
  情報工学
- 研究機関
  大阪大学
ソフトウェア構成プロセスの記述とその実働化の研究
- 研究代表者
  
  鳥居宏次
- 研究期間 (年度)
  1990 – 1991
- 研究種目
  
  重点領域研究
- 研究機関
  大阪大学
代数的手法によるプログラムの正しさ証明システムの作成に関する研究研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1989
- 研究種目
  
  一般研究(C)
- 研究分野
  
  情報工学
- 研究機関
  大阪大学
代数的手法を用いたハードウェアの仕様記述と実現に関する研究研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1988
- 研究種目
  
  一般研究(C)
- 研究分野
  
  情報工学
- 研究機関
  大阪大学
通信プロトコルにおけるエラーリカバリ法の記述と検証に関する研究研究代表者
- 研究代表者
  
  谷口健一
- 研究期間 (年度)
  1987
- 研究種目
  
  一般研究(C)
- 研究機関
  大阪大学
ソフトウェア作成時のエラー意味分析と高信頼化技法に関する研究
- 研究代表者
  
  鳥居宏次
- 研究期間 (年度)
  1985 – 1986
- 研究種目
  
  一般研究(C)
- 研究分野
  
  情報工学
- 研究機関
  大阪大学

すべて 2005 2004 2003 2002

すべて雑誌論文

[雑誌論文] A Method to Develop Distributed Real-time Applications based on UML/OCL2005
- 著者名/発表者名
  Aya MAKIDERA, Eigo NAGAI, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.104, No.723
  
  ページ: 1-6
- NAID
  110003277300
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] An implementation of a decision procedure for Presburger sentences in ML and its application to verification support system2004
- 著者名/発表者名
  Tetsuya SAIMURA, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE Vol.103, No.708
  
  ページ: 7-12
- NAID
  110003276708
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13558028
[雑誌論文] Consistency Checking of Timeliness QoS of Multi-Media Systems and Derivation of Codes for Timing Control2004
- 著者名/発表者名
  Kazuo MORI, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.103, No.583
  
  ページ: 13-18
- NAID
  110003276701
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] Consistency Checking of Timeliness QoS with Linear Constraints2004
- 著者名/発表者名
  Kozo OKANO, Kazuo MORI, Kenichi TANIGUCHI
- 雑誌名
  
  Kokyuroku of Research Institute for Mathematical Sciences Kyoto University Vol.1375
  
  ページ: 151-157
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] A Verification method and verification support system based on the method for functional programming for ML2004
- 著者名/発表者名
  Tetsuya SAIMURA, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  Proceedings of Software Symposium, 2004 (ISBN4-916227-16-6)
  
  ページ: 53-57
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13558028
[雑誌論文] A verification support system for functional programming for ML2004
- 著者名/発表者名
  Tetsuya SAIMURA, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE Vol.104, No.243
  
  ページ: 13-18
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13558028
[雑誌論文] A Timeliness QoS Consistency Checker and a Timing Control Code Generator for Development of Real-time Applications in Distributed Environments2004
- 著者名/発表者名
  Aya MAKIDERA, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.104, No.243
  
  ページ: 19-24
- NAID
  110003276723
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] Symbolic Model Checking of Extended Finite State Machines with Linear Constraints over Integer Variables2004
- 著者名/発表者名
  Takashi TAKENAKA, Kozo OKANO, Teruo HIGASHINO, Kenichi TANIGUCHI
- 雑誌名
  
  IEICE Transactions on Information and Systems Vol.J87-DI, No.4
  
  ページ: 462-470
- NAID
  110003171323
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13558028
[雑誌論文] Specification and Verification of Real-Time System with Extended Timed Automata2003
- 著者名/発表者名
  Yuichiro KATO, Hirozumi.YAMAGUCHI, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.102, No.616
  
  ページ: 13-18
- NAID
  110003276632
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] Colored Petri-nets with time constraints for workflow descriptions2002
- 著者名/発表者名
  Kozo OKANO, Akira YAMAGUCHI, Kenichi Taniguchi
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.102, No.96
  
  ページ: 13-16
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] A Method for Describing Specification for GUI Controllers with Timing Restrictions.2002
- 著者名/発表者名
  Yuichiro KATO, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.102, No.629
  
  ページ: 15-22
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] Deriving Work Schedules from Workflow Description in Colored Petri-nets with Time Constraints2002
- 著者名/発表者名
  Akira YAMAGUCHI, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.102, No.629
  
  ページ: 23-30
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414
[雑誌論文] A Deriving Method for J2ME Program on Personal Appliances from Application Descriptions in Petri-nets and their Executional environment2002
- 著者名/発表者名
  Kosuke SAKAUE, Kozo OKANO, Kenichi TANIGUCHI
- 雑誌名
  
  TECHNICAL REPORT OF IEICE. Vol.102, No.246
  
  ページ: 1-6
- NAID
  110003498092
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-13680414

1. 東野輝夫 (80173144)

共同の研究課題数: 14件

共同の研究成果数: 1件
2. 岡野浩三 (70252632)

共同の研究課題数: 12件

共同の研究成果数: 13件
3. 北道淳司 (20234271)

共同の研究課題数: 8件

共同の研究成果数: 0件
4. 松浦敏雄 (40127296)

共同の研究課題数: 6件

共同の研究成果数: 0件
5. 杉山裕二 (50116050)

共同の研究課題数: 5件

共同の研究成果数: 0件
6. 山口弘純 (80314409)

共同の研究課題数: 5件

共同の研究成果数: 3件
7. 鳥居宏次 (10172222)

共同の研究課題数: 4件

共同の研究成果数: 0件
8. 菊野享 (50093745)

共同の研究課題数: 3件

共同の研究成果数: 0件
9. 安本慶一 (40273396)

共同の研究課題数: 3件

共同の研究成果数: 0件
10. 筧捷彦 (20062672)

共同の研究課題数: 3件

共同の研究成果数: 0件
11. 落水浩一郎 (10022310)

共同の研究課題数: 3件

共同の研究成果数: 0件
12. 藤井護 (00029464)

共同の研究課題数: 2件

共同の研究成果数: 0件
13. 北嶋暁 (00304030)

共同の研究課題数: 2件

共同の研究成果数: 0件
14. 森岡澄夫

共同の研究課題数: 2件

共同の研究成果数: 0件
15. 武市正人 (10011165)

共同の研究課題数: 1件

共同の研究成果数: 0件
16. 柴山悦哉 (80162642)

共同の研究課題数: 1件

共同の研究成果数: 0件
17. 二村良彦 (50238648)

共同の研究課題数: 1件

共同の研究成果数: 0件
18. 米澤明憲 (00133116)

共同の研究課題数: 1件

共同の研究成果数: 0件
19. 中田明夫 (60295839)

共同の研究課題数: 1件

共同の研究成果数: 0件
20. 工藤英男 (60133146)

共同の研究課題数: 1件

共同の研究成果数: 0件
21. 楠本真二 (30234438)

共同の研究課題数: 1件

共同の研究成果数: 0件
22. 伊藤実 (90127184)

共同の研究課題数: 1件

共同の研究成果数: 0件
23. 大蒔和仁

共同の研究課題数: 1件

共同の研究成果数: 0件

谷口 健一 TANIGUCHI Kenichi

研究課題

研究成果

共同研究者

モデル検査技術を活用したソフトウェア設計方法に関する研究

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

状態爆発するWEBアプリケーションに対するソフトウェアモデル検査

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

ハードウェアの高位設計・検証支援システム研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

オブジェクト指向型ソフトウェアの仕様記述と検証及び実行プログラム導出研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

並行動作順序回路システムの設計と検証に関する研究研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

分散システム記述言語のコンパイラ研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

ソフトウェア発展のための基本機構の研究

研究代表者

研究期間 (年度)

研究種目

研究機関

通信プロトコルの形式仕様からのハードウェア回路合成研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

マルチランデブを含むLOTOSプログラムの分散実行系の構築研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

複数の制御部をもつ同期式順序回路の機能検証に関する研究研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

ペトリネット型実行制御部をもつ代数的仕様記述の検証と分散実行系研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

代数的手法を用いたプログラムの階層的設計と開発環境に関する研究研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

ASIC設計の上流工程設計支援システムの開発研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

谷口健一 TANIGUCHI Kenichi