Researchers

HIGUCHI Masahiro

HIGUCHI Masahiro
Professor
Faculty Department of Informatics / Graduate School of Science and Engineering
Researchmap https://researchmap.jp/highig

Education and Career

Academic & Professional Experience

  • Apr. 2013 - Today , Kindai University Faculty of Science and Engineering 教授
  • Apr. 2000 - Mar. 2013 , Kindai University Faculty of Science and Engineering 助教授、准教授

Research Activities

Research Areas

  • Informatics, Software

Research Interests

不変式, 時間制約, 整数値レジスタ, タイムアウト処理, 非有界FIFO, 弱双模倣等価, プロセス代数, 安全性, 閉包性, 物流監視システム, 通信プロトコル, 論理検証, モデル検査, スケジューリング, 局所的コピー, 並行制御, 逐次化グラフ, 分散データベース

Published Papers

  1. 多重Ambient Calculusのための統合開発環境
    加藤暢; 山田瞭太; 鳥山颯斗; 大倉亮介; 樋口昌宏
    情報処理学会論文誌 数理モデル化と応用  14  (1)  , 21-32, Jan. 2021  , Refereed
  2. 多重 Ambient Calculus を用いた動的な海上物流計画に対するモデル検査
    加藤暢; 高岡久裕; 樋口昌宏; 大山博史
    情報処理学会論文誌 数理モデル化と応用  11  (3)  , 84-99, Dec. 2018  , Refereed
  3. Hybrid Timed Ambient Calculus for Logistics Specification
    藤坂吉秀; 稲森啓太; 樋口昌宏; 加藤暢
    情報処理学会論文誌プログラミング  10  (4)  , 12-27, Jul. 2017  , Refereed

MORE

Books etc

  1. Eclipse ではじめるオブジェクト指向Javaプログラミング入門 , 加藤 暢; 樋口 昌宏; 高田 司郎 , 近代科学社 , Aug. 2008
  2. UNIX(増補) -基礎から簡単な応用まで、さあ使ってみよう- , 西村 卓也; 加藤 暢; 広永 美喜也; 山口 孜; 天野 亮; 淺井 恒信; 湯本 真樹; 松居 哲生; 樋口 昌宏; 堀口和己 , コロナ社 , May. 2002

Conference Activities & Talks

  1. Timed Ambient Calculus , 樋口 昌宏 , 情報処理学会プログラミング研究会 , Jan. 2013
  2. DAOパターンを用いるWebアプリケーションのための単体テストケース補完ツール , 鎌田 高如; 樋口 昌宏 , 情報処理学会第74回全国大会 , Mar. 2012
  3. 集団行動支援のための位置情報頒布方式における適正なパラメータ値の算出 , 植田 健司; 樋口 昌宏 , 情報処理学会第74回全国大会 , Mar. 2012

MORE

MISC

  1. CTL Model Checking for Hybrid Timed Ambient Calculus , 稲森 啓太; 樋口 昌宏; 加藤 暢 , 情報処理学会論文誌プログラミング（PRO） , 10 , 5 , 2 , 2 , 14, Nov. 2017
    Summary:本発表では混合型時間アンビアント計算（HTAC）を用いて記述した物流システムについてのCTLモデル検査について述べる．HTACとは，アンビアント計算を時間的な制約が記述できるよう拡張したプロセス代数であり，物流システムの持つ動的な階層構造や時間制約を簡潔に表現することができる．HTACを用いて物流システムを記述する際には，物流システムと見なせるための条件をプロセス式が満たしているか確認する必要がある．また，HTACによって物流システムを記述したプロセス式が所期の目的を満たしているかを確認するためには，プロセス式に対してモデル検査を行う必要がある．これらには可達性解析による網羅的な式の列挙が必要であるが，時間制約に関するパラメータが大きいプロセス式を解析する場合，単純な可達性解析では状態空間爆発が起こる．本発表では，この問題を解決するため，式中の時間制約に関するパラメータを変数で表現した式と変数間の関係を表す連立不等式を用いた解析手法を提案する．さらに，提案手法に基づき開発した可達性解析プログラムについても述べる．また本発表では，物流システムが持つHTAC特有の性質を論理式として表現するための時間アンビアント論理を提案し，開発した可達性解析プログラムを利用し構築したプロセス式に対するCTLモデル検査プログラムについても述べる．CTLモデル検査プログラムを用いて行った検査実験の結果についても述べる．In this presentation, we present the CTL model checking method for logistics plans specified in the hybrid timed ambient calculus (HTAC).HTAC is a process algebra as an extension of the ambient calculus and suitable for specifying logistics plans, which contain dynamically changing nested structures and timing constraints.We need to confirm that a HTAC formula satisfies conditions to be regarded as a logistics plan.We also need to perform a CTL model checking for the HTAC formula to ensure that the HTAC formula satisfies desirable properties.Therefore, we have to perform a reachability analysis which enumerates all reachable HTAC formulas.Since a simple reachability analysis for the HTAC formula with large parameters on timing constraints causes a state explosion, we propose an efficient algorithm and developed a reachability analysis program based on it.We also propose the timed ambient logic to express properties of logistics plans specified in HTAC.We developed a CTL model checking program for the HTAC formula using the reachability analysis program.We present checking experiments using the CTL model checking program.
  2. The Dynamic Routing Function for the Freight Management System with the Multiple Ambient Calculus , 宮井 亜人夢; 加藤 暢; 樋口 昌宏; 大山 博史 , 情報処理学会論文誌プログラミング（PRO） , 9 , 4 , 29 , 29 , 12, Sep. 2016
    Summary:コンテナ輸送を行う海上物流システムに対し，RFID機器を用いてコンテナの輸送状況を監視する様々な方法が多くの機関で研究・実用化されている．これに対し我々は，海上物流システムの持つ動的な階層構造に着目し，この構造を正確にモデル化することのできる多重Ambient Calculus（MAC）を用いた物流監視システムを研究している．これは，実際の物流システムの中で使用される様々な書類からMACのプロセス式（モデル）を自動的に生成し，このモデルと実際の貨物の取扱いを対比させることでコンテナ輸送の監視を行うものである．船の乗り換えを含むコンテナの海上輸送では，コンテナが次に載せ換えられる船は運送途中でつねに動的に決定される．このようなコンテナ輸送をモデル化し，複雑な経路をたどるコンテナの取扱いを正しく監視するために，我々はモデルの自動生成機能の中に動的なルーティング機能を取り入れた．これは，コンテナが中継港に到着した際，中継港を発着するコンテナ船の航路表や時刻表などから，コンテナの目的地に応じた最適な船を選定し，コンテナの経路を表すプロセス式を自動的に生成するものである．本発表では動的経路設定機能および，この機能により生成されたMACのプロセス式をRFIDタグに書き込んで行った屋外実験について述べる．Various methods of monitoring the transportation of containers with RFID devices in freight systems have been studied and put to practical use by many institutions. We are developing a freight management system that can not only monitor the handling of containers with RFID devices but also confirms the correctness of it by modeling whole the freight system with Multiple Ambient Calculus (MAC). MAC is a formal description language that can express freight systems with nested structures that dynamically change. Our system generates the model from several real trading documents and confirms the correctness of handling by comparing the handling with the model. In the maritime transport of containers, including the transfer of the vessels in hab ports, those vessels are dynamically determined. Thus we have developed the modeling system that generates MAC formulae dynamically by refereeing routing tables and time tables of vessels so that our system can supervise handling of containers that follow complicated route with many transit ports. This presentation shows the implementation of the freight management system with the dynamic routing function and the results of several experiments of the system using RFID devices.
  3. A-005 Hybrid Timed Ambient Calculus : Comparison with Timed Mobile Ambient , Fujisaka Yoshihide; Higuchi Masahiro , 情報科学技術フォーラム講演論文集 , 14 , 1 , 105 , 106 , 24, Aug. 2015

MORE

Research Grants & Projects

  1. Japan Society for the Promotion of Science, Grants-in-Aid for Scientific Research, Extension of the Ambient Calculus and Freight Management Systems based on it , Kinki University
  2. Japan Society for the Promotion of Science, Grants-in-Aid for Scientific Research, Timed Extension of the Ambient Calculus and its Application for Freight System Specifications , Kinki University
  3. 日本学術振興会, 科学研究費助成事業, データベースシステムにおける分散型スケジューリング手法の開発 , 大阪大学

MORE