2024/11/21 更新

写真b

チョウ　カンメイ
張　漢明
CHANG Han-Myung
所属
理工学部 ソフトウェア工学科 教授
職名
教授
主な研究課題
長期研究：形式手法に基づいたソフトウェア開発支援環境

短期研究：形式手法に基づいた組込みシステム開発手法
専攻分野
ソフトウェア工学，形式手法

学位

  • 博士（工学） 博第43号 （ 1999年3月   奈良先端科学技術大学院大学 ）

    　 詳細を見る

    博士

  • 修士（工学） （ 1995年3月   奈良先端科学技術大学院大学 ）

    　 詳細を見る

    修士

  • 学士 （ 1989年3月   同志社大学 ）

    　 詳細を見る

    学士

研究分野

  • 情報通信 / ソフトウェア

学歴

  • 奈良先端科学技術大学院大学   情報科学研究科   情報システム学専攻

    - 1999年3月

  • 同志社大学   工学部   機械工学科

    - 1989年3月

所属学協会

  • 各会員

  • ソフトウェア技術者協会会員，

  • 情報処理学会会員，

  • 日本ソフトウェア科学会会員，

委員歴

  • 各会員  

  • ソフトウェア技術者協会会員，  

  • 情報処理学会会員，  

  • 日本ソフトウェア科学会会員，  

論文

  • IoTアプリケーションのためのコンテキスト指向ソフトウェアアーキテクチャ

    ソフトウェア工学の基礎30（日本ソフトウェア科学会ソフトウェア工学の基礎研究会FOSE2023）   159 - 164   2023年11月

    　詳細を見る

    出版者・発行元：近代科学社  

    コンテキストに応じて協調するマイクロサービス群としてIoTアプリケーションを構成する方法が一般的となってきている．
    このような背景のもと，IoTアプリケーションの設計に際して，コンテキスト指向，サービス指向，マイクロサービス群のマッシュアップを考慮したソフトウェアアーキテクチャの必要性が指摘されている．
    本研究の目的は，コンテキスト指向で設計されたIoTアプリケーションをサービス化し，並行処理記述を用いてサービス連携を実現するための枠組みを整理することである．
    すなわち，IoTアプリケーションのためのアーキテクチャを定義し，マイクロサービス連携のための記述方式について検討する．

  • 自動運転における危険予測のためのコンテキスト指向ソフトウェアアーキテクチャ

    ソフトウェアエンジニアリングシンポジウム2023論文集   Vol. 2023   pp. 154 - 163   2023年8月

    　詳細を見る

    出版者・発行元：情報処理学会  

    概要（Abstract） AI 技術の応用研究として自動車の自動運転に関する取り組みが盛んにおこなわれている．AI 技術を適用した危険予測システムにおいて，予測精度と処理速度はともに重要な非機能特性であるが，これらに対する要求は一般に対立する．本研究では，対立する非機能要求の調整を目的とし，危険予測に用いる
    ニューラルネットワークの状況に応じた選択を支援するソフトウェアアーキテクチャを提案する．提案するアーキテクチャは，コンテキスト指向を適用することで，動的なコンポーネント選択を可能とする構造として定義する．一方で，ニューラルネットワークには時間が経過するとともにモデルが劣化する問題がある．この問題に対処するために，コンテキストとそれに応じたコンポーネント選択の論理に関するコンポーネント群をメタレベルに位置づけ，実際の危険予測に関わるベースレベルのコンポーネント群から明確に分離したアーキテクチャを定義することで変更容易性を確保する．提案するアーキテクチャに基づいて対立する要求の調整が実現できることを，プロトタイプシステムの実装により評価する．また，構築したシステムの変更容易性の観点からの評価もおこなう．

  • VDM-SL in Action: A FRAM-Based Approach to Contextualize Formal Specifications

    Proceedings of the 20th Overture Workshop   1 - 14   2022年10月

  • Refactoring for Exploratory Specification in VDM-SL

    THE 19TH OVERTURE WORKSHOP   2021年10月

  • アスペクト指向アーキテクチャに基づく組込みソフトウェアの設計法の提案

    ソフトウェアエンジニアリングシンポジウム2021論文集   32 - 40   2021年8月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • Specifying Abstract User Interface in VDM-SL

    THE 18TH OVERTURE WORKSHOP   1 - 15   2020年10月

  • 探索的仕様記述のための履歴ツールの提案と実装

    ソフトウェアシンポジウム2020論文集   95 - 103   2020年6月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

    小田朋宏，張漢明，山本恭裕，中小路久美代，荒木啓二郎

  • 探索的仕様記述のための履歴ツールの提案と実装

    ソフトウェアシンポジウム2020論文集   95 - 103   2020年6月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

  • ViennaDoc: An Animatable and Testable Specification Documentation

    Proceedings of the 17th Overture Workshop   CS-TR- 1530   76 - 90   2019年9月

    　詳細を見る

    出版者・発行元：Newcastle University  

  • MVCアーキテクチャのメタレベル適用による形式仕様モデルに関する考察

    ソフトウェア工学の基礎XXIV（日本ソフトウェア科学会FOSE2017）   183 - 188   2017年11月

    　詳細を見る

    出版者・発行元：近代科学社  

  • 複数事象の発生を含意した区間振る舞い記述法とその検証法の提案

    コンピュータソフトウェア   34 ( 2 )   3 - 15   2017年5月

    　詳細を見る

    出版者・発行元：岩波書店  

  • コンパイル方式による高速軽量なXQuery問い合わせプログラム生成系の設計と実現

    コンピュータソフトウェア   30 ( 4 )   4_67 - 4_81   2013年11月

    　詳細を見る

    出版者・発行元：岩波書店  

  • 前処理プログラムに対する記号表の構成手法

    情報処理学会論文誌   54 ( 2 )   912 - 921   2013年2月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • Webページ記述内のプログラム断片に対する DOM tree を用いた構文木の構成手法

    ソフトウェアエンジニアリングシンポジウム2012論文集   2012   1 - 6   2012年8月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • 前処理プログラムに対する記号表の構成手法

    ソフトウェアエンジニアリングシンポジウム2012論文集   2012   1 - 6   2012年8月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • 属性付き字句系列に基づくソースコード書換え支援環境

    情報処理学会論文誌   53 ( 7 )   1832 - 1849   2012年7月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • コンパイル方式によるXQuery問い合わせプログラム生成方法

    ソフトウェア工学の基礎XVIIIー日本ソフトウェア科学会 FOSE2011   21 - 30   2011年11月

    　詳細を見る

    出版者・発行元：日本ソフトウェア科学会  

  • A Design Map for Recording Precise Architecture Decisions

    Proceedings of the 18th Asia-Pacific Software Engineering Conference (APSEC2011)   298 - 305   2011年11月

  • ソースコードインスペクションツールのためのソフトウェアアーキテクチャの設計と進化

    コンピュータソフトウェア   28 ( 4 )   4_241 - 4_261   2011年11月

    　詳細を見る

    出版者・発行元：岩波書店  

  • HTML要素の状態を考慮した CSS の拡張方法の提案

    電子情報通信学会論文誌 D   J94-D ( 11 )   1931 - 1934   2011年11月

    　詳細を見る

    出版者・発行元：電子情報通信学会  

  • パターンに基づくCSP記述の検査に関する考察

    電子情報通信学会技術研究報告／ソフトウェアサイエンス研究会   111 ( 268 )   49 - 54   2011年10月

    　詳細を見る

    出版者・発行元：電子情報通信学会  

  • 表現の違いを考慮したマクロ逆置換方法の提案

    ソフトウェアエンジニアリングシンポジウム2011(SES2011)論文集   Vol. 2011   1 - 6   2011年9月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • デザインパターンを用いたソースコードインスペクションツールのソフトウェアアーキテクチャ設計

    ソフトウェア工学の基礎XVII－日本ソフトウェア科学会FOSE2010   15 - 24   2010年11月

    　詳細を見る

    出版者・発行元：近代科学社  

  • モデル検査を用いた振舞検証の実用化技術に関する考察－網羅性に着目して－

    ソフトウェア工学の基礎XVII－日本ソフトウェア科学会FOSE2010   107 - 112   2010年11月

    　詳細を見る

    出版者・発行元：近代科学社  

  • 階層分割に基づく組込みソフトウェアの振舞い検証の支援について

    情報処理学会研究報告／組込みシステム研究会   2010-EMB-18 ( 6 )   1 - 8   2010年8月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • 属性付き字句系列に基づくプログラム書換え支援環境の試作

    ソフトウェアエンジニアリング最前線－情報処理学会SES2010   119 - 126   2010年8月

    　詳細を見る

    出版者・発行元：近代科学社  

  • E-AoSAS++における振舞い検証の枠組み

    電子情報通信学会技術研究報告   109 ( 456 )   97 - 102   2010年3月

    　詳細を見る

    出版者・発行元：電子情報通信学会  

  • 組込みソフトウェアの仕様モデルとアーキテクチャの関係に関する考察

    情報処理学会研究報告／ソフトウェア工学研究会   2010-SE-167 ( 25 )   1 - 6   2010年3月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • 遅延パーサを用いた軽量なXQuery処理系

    電子情報通信学会技術研究報告   109 ( 456 )   157 - 162   2010年3月

    　詳細を見る

    出版者・発行元：電子情報通信学会  

  • アスペクト指向ソフトウェアアーキテクチャの振る舞い検証に関する考察

    ソフトウェア工学の基礎XVI - 日本ソフトウェア科学会FOSE2009   267 - 274   2009年11月

    　詳細を見る

    出版者・発行元：近代科学社  

  • データフロー解析を用いたアスペクトの干渉の検出

    ソフトウェア工学の基礎XIII，レクチャーノート／ソフトウェア学32   19 - 28   2006年11月

    　詳細を見る

    出版者・発行元：近代科学社  

    AspectJのようにアドバイス機構を用いるプログラミング言語の場合，アスペクトの干渉問題が報告されている．我々は，アスペクトの干渉問題をオブジェクト内の副作用が意図しない形で顕在化する問題であると定義する．本稿では，アスペクトの干渉の可能性箇所をプログラム実行前に検出する方法を提案する．アスペクトの干渉可能性を分析するために，オブジェクト指向プログラムにおけるデータフロー解析を応用する．AspectJ を対象として，アスペクトの干渉とその確度を定義し，干渉可能性箇所を検出する方法を示す．

  • 組込みソフトウェアにおける構成制御とその記述法の提案

    ソフトウェアエンジニアリング最前線2006 情報処理学会SEシンポジウム   177 - 184   2006年10月

    　詳細を見る

    出版者・発行元：近代科学社  

    組込みソフトウェアは，一般的に，イベント駆動で並行に動作する状態遷移機械の集合としてモデル化可能である．しかしながら，大規模かつ複雑化する組込みシステムに対して，状態遷移機械を適切に構成するための手法は提案されていない．本研究では，状態遷移機械の分割の指針として構成制御の概念を導入し，システム構成の動的な変更を状態遷移機械で表現することの妥当性，および形式的なアプローチの適用を検討する．既存の成熟した技術を応用し，実際の開発現場において適用が容易であることを目指した．本論文では，UMLのステートマシン図を用いた構成制御の図式表記法を提案し，図式表現から CSP への変換手法について議論する．構成制御の概念は，イベント駆動でモデル化されるソフトウェアの簡潔かつ矛盾のない記述を可能にする．

  • アスペクト指向技術を用いたORBミドルウェア開発方法

    情報処理学会論文誌   Vol.45 No.6   1533 - 1545   2004年6月

    　詳細を見る

    出版者・発行元：情報処理学会  

    本論文ではアスペクト指向技術を適用したORBミドルウェアの開発方法を示す．ORBミドルウェアを階層モデルで表現すると複数の層を横断した構成要素が存在してしまう．われわれは層をアスペクトとしてとらえてアスペクト間の関係を整理したソフトウェアアーキテクチャを提案する．アーキテクチャに基づいて，ORBのフレームワークとスタブ，スケルトン生成系の言語独立な設計方法を示す．ORBに関するアスペクトは独立したフレームワークとして実現する．スタブ，スケルトン生成系はウィーバの役割を果たし，ORBフレームワークを利用するためのコードが織り込まれたスタブ，スケルトンを生成する．提案した開発方法に基づいてXML-RPCのORBミドルウェアを実現し，ORBミドルウェアの開発が省力化できること，ORBミドルウェアの機能の追加が容易なことを確認した．

  • 組込みソフトウェアの階層化されたアスペクト指向ソフトウェアアーキテクチャ群の構築

    ソフトウェア工学の基礎X，レクチャーノート／ソフトウェア学29   41 - 52   2003年11月

    　詳細を見る

    出版者・発行元：近代科学社  

    Aspect-oriented technolgies, role based computation or field based computation have been developed for solving each problems. We integrated these technologies to aspect-oriented software architecture style. We tried to apply this architecture style to embedded systems to construct software architecture for embedded systems. As a result, we construct aspect-oriented software architecture to separate concerns without crosscut each other and active objects' behaviors.

  • ORBミドルウェアのためのアスペクト指向ソフトウェア・アーキテクチャの提案

    オブジェクト指向最前線2003 情報処理学会OO2003シンポジウム   161 - 168   2003年8月

    　詳細を見る

    出版者・発行元：近代科学社  

    本研究ではORBミドルウェアの構造を整理し開発を省力化するために，ORBミドルウェアのアスペクト指向ソフトウェア・アーキテクチャを提案する．ORBミドルウェアを階層モデルで表現すると複数の層を横断した構成要素が存在してしまう．われわれは層をアスペクトとしてとらえてアスペクト間の関係を整理した．アーキテクチャに基づいて，ORBのフレームワークとスタブ，スケルトンの自動生成系を設計・実現する．ORBに関するアスペクトは独立したフレームワークとして実現する．自動生成系はウィーバの役割をし，ORBフレームワークを利用するためのコードが織り込まれたスタブ，スケルトンを生成する．提案したアーキテクチャに基づいてXML-RPCのORBミドルウェアを実現し，開発が省力化できることを確認した．

  • 組込みソフトウェアのアスペクト指向ソフトウェアアーキテクチャ〜自動販売機のカップ機構制御ソフトウェアアーキテクチャの構築〜

    ソフトウェア・シンポジウム2003論文集   76 - 85   2003年7月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

    一般的にソフトウェアの構造は，注目する視点ごとに最適な構造が異なるという問題点がある．この問題の解決策の一つとしてアスペクト指向が注目されている．本研究の目的は，組み込みソフトウェアのアスペクト指向ソフトウェアアーキテクチャを提案することである．組み込みソフトウェアという広い領域でのアーキテクチャを構築することは困難なので，事例として自動販売機のカップ機構制御のソフトウェアアーキテクチャを提案する．カップ機構制御のソフトウェアアーキテクチャを構築するさいに，複数の視点から見ても整理された構造を得るためにアスペクト指向を適用する．ハードウェア制御と時間制御をアスペクトとして分割することで，組み込みソフトウェアの開発に有効なアーキテクチャが提案できた．

  • VDM-SLによるソフトウェアアーキテクチャの記述法

    『アカデミア』南山大学紀要数理情報編   vol.3   pp53 - 60   2003年3月

    　詳細を見る

    出版者・発行元：南山大学  

    本論文では、ソフトウェアアーキテクチャにおけるソフトウェアコンポーネント間の関係を分析し、ソフトウェアアーキテクチャの形式的な仕様記述の枠組みについて議論する。住所録システムの事例を通して、同一レベルのソフトウェアの構成要素間の「関係」と、異なった抽象レベルのソフトウェアの構造間の「関係」を明らかにして、形式仕様記述言語 VDM-SL による記述例を示す。

  • ソフトウェアアーキテクチャにおける形式手法の適用に関する考察

    ソフトウェア工学の基礎IX『レクチャーノート／ソフトウェア工学   179 - 183   2002年11月

    　詳細を見る

    出版者・発行元：近代科学社  

    ソフトウェアの構成要素間の関係を明らかにして、形式手法に基づいたソフトウェアアーキテクチャの表記法を提示することを目指して、形式手法に基づいた記述モデルと形式手法の適用指針について考察した。仕様、設計、実現の各々の抽象レベルにおいて、形式仕様記述言語VDM-SLにおける仕様記述の指針を示し、販売管理システムの事例を通してその有用性を議論した。

  • Design of an Aspect-Oriented Software Architecture for Web-based Information System

    Proc. International Symposium on Future Software Technology 2002 (CD-ROM)   2002年10月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

    本稿では、Web情報システム（WIS）のためのアスペクト指向ソフトウェアアーキテクチャを提案する。WISの開発では、CGIスクリプト、アプレット、PHP、サーブレットなどの既存のWeb開発技術をどのように組み合わせるかが重要な課題である。アスペクト指向ソフトウェアアーキテクチャの概念と、その有用性について議論する。

  • データ型を考慮した軽量なXML文書処理系の自動生成

    コンピュータソフトウェア   Vol.19 No.5   334 - 344   2002年9月

    　詳細を見る

    出版者・発行元：日本ソフトウェア科学会編集 岩波書店  

    軽量なXML文書処理系の自動生成系xpgen の設計とその実現について述べた。軽量かつ実用的なXML文書処理系の作成支援のために、xpgenはDTDから、字句・構文解析をおこなうlexおよびyaccのソースプログラムを生成するように設計した。意味解析のためのコードはyaccのソースプログラム内のアクションとして記述する。xpgenを試作し、既存のXML パーサよりも静的意味検査等の処理記述が容易であること、文書の解析に必要なメモリ量が少ないことを確認した。

  • World-Wide Web Server with Application Layer Queue: System and Object-Oriented Software Architecture

    IEICE Transaction on Information and Systems   Vol. E85-D,No.8   1195 - 1204   2002年8月

    　詳細を見る

    出版者・発行元：IEICE  

    WWWサーバが安定稼働するための機構として、応用層での待ち行列を用い受付制限と先着順などのサービスを提案し、オブジェクト指向ソフトウェアアーキテクチャによって試作したサーバの性能を評価した。

  • Web情報システムのソフトウェアアーキテクチャ

    情報処理学会OO2002シンポジウム   93 - 96   2002年8月

    　詳細を見る

    出版者・発行元：近代科学社  

    Web情報システム（WIS）の開発者は無秩序に存在するWeb技術に混乱しており、Web技術の理解、選択などに多くの労力を費やしている。本研究では、適切なWeb技術を使用するための枠組みを示すことを目的とし、WISのオブジェクト指向ソフトウェアアーキテクチャを構築する。

  • An Application Framework for TCP/IP Applications

    COMPSAC2002   627〜 - 634   2002年8月

    　詳細を見る

    出版者・発行元：IEEE  

    本稿では、TCP/IPアプリケーションのためのアプリケーションフレームワークを提示する。フレームワークは、利用者がカスタマイズすることができるコンポーネントを含んだ、再利用可能なコンポーネントの集まりを提供する。本フレームを用いて様々なTCP/IPアプリケーションを実現し、アプリケーションフレームワークの有効性を示す。

  • TCP/IPアプリケーション開発支援キットの設計，実現とその運用

    『アカデミア』　数理情報編   2巻   35 - 42   2002年3月

    　詳細を見る

    出版者・発行元：南山大学  

    現在，TCP/IPアプリケーションは一部の有能なプログラマによって，システムコールライブラリ等の低粒度部品を使用して手続き指向で実現されており，ソフトウェア工学的には多くの問題を孕んでいる。この問題の解決策としてTCP/IPアプリケーションの開発支援キットIpakを設計，実現する。Ipakは，クラスライブラリ，自動生成系，アプリケーションフレームワーク等の技術を応用した開発支援キットである。Ipakを使用してTCP/IPアプリケーションを開発し，その有用性について考察する。

  • A Generic Graph Analysis Tool with Attributed Path Query

    Proc. of Internation-al Symposium on Future Software Technology 2001   240 - 245   2001年11月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

    This paper presents Graph Analyser and PQL. Graph Analyser is developed as a generic tool which can not only edit many sorts of graphs but also have functionality to analyse them. PQL is a query language for Graph Analyser to specify paths. We show that

  • Systematic Generation of Statechart from VDM-SL in Multi-Aspect Formal Methods for System Developme

    Proc. of Internation-al Symposium on Future Software Technology 2001   9 - 14   2001年11月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

    It is very important to analyze both static and dynamic aspects of the system to describe good specification. In such cases, using only one specification language is not enough. Therefore, we have intended to use two kinds of specification languages, mode

  • 形式手法による配電線自動制御システムのドメイン分析

    ソフトウェア工学の基礎VI FOSE’99   13 - 17   1999年12月

    　詳細を見る

    出版者・発行元：近代科学社  

  • モデル形成支援のための仕様記述変換技術

    情報処理学会論文誌『数理モデル化と問題解決応用』   40巻 No.SIG9(TO   18 - 29   1999年12月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • SSLプロトコルの形式仕様記述と検証

    情報処理学会論文誌『数理モデル化と問題解決応用』   40巻 No.SIG9(TO   51 - 61   1999年12月

    　詳細を見る

    出版者・発行元：情報処理学会  

  • システム仕様記述のための変換技術に関する基礎的研究 (博士論文)

    125 pp.   1999年3月

    　詳細を見る

    出版者・発行元：奈良先端科学技術大学院大学  

  • システム要求定義における4Wダイアグラムの提案

    ソフトウェア・シンポジウム’98論文集   190 - 197   1998年6月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

  • 形式的手法に基づいた構造化ダイアグラムの一貫性検証について

    コンピュータソフトウェア   Vol. 15No. 3   2 - 16   1998年5月

    　詳細を見る

    出版者・発行元：日本ソフトウェア科学会  

  • Software Development with Common Formal System Descriptions

    Proc. of Internation-al Symposium on Future Software Technology　’97   143 - 150   1997年11月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

  • Extracting System Invariants from Operation Specifications

    Proc. Changsha Internation-al CASE Symposium　’95   16 - 22   1995年10月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

  • 形式的手法による機能分割手法

    第1回ソフトウェア工学の基礎ワークショップFOSE’94論文集   129 - 134   1994年12月

    　詳細を見る

    出版者・発行元：日本ソフトウェア科学会  

  • Formal Approach to Modeling and Requirement Analysis with Z

    Proc. Kunming Internation-al CASE Symposium　’94   5B.1 - 5B.14   1994年11月

    　詳細を見る

    出版者・発行元：ソフトウェア技術者協会  

▼全件表示

書籍等出版物

  • プログラム仕様記述論

    （ 担当： 共著）

    オーム社  2002年11月 

    　詳細を見る

    総ページ数：210p.  

    情報関連の大学学部学生およびソフトウェア技術者を対象として、高品質のソフトウェアを効率よく開発するために、プログラムの正しさを証明するためのプログラム検証理論と形式仕様記述を解説する。検証理論としてFloydの手法とFloyd-Hoare論理の基本概念を説明し、形式仕様記述言語VDM-SLの概説と、実践的なVDM-SLの仕様記述例を用いて形式仕様記述の基本的な考え方を解説する。

  • ソフトウェア開発のモデル化技法

    （ 担当： 共訳）

    岩波書店　  2003年2月 

    　詳細を見る

    担当ページ：306p.  

    大規模システムのソフトウェアは、顧客の要求が多様で複雑、かつ不完全なため、何度も大幅な手直しをしながら、仕上げられている。ISOで標準化された言語、VDM-SLは、抽象性と厳密性をあわせもった仕様記述言語で、システムのモデル化に最適である。これを使えば、システムの全体構造を容易に把握できるようになり、開発コストの削減にも役立つ。本書では、実践例をもとにその記述を解説する。

MISC

  • Formal Methods in Japan - Current State, Problems and Challenge -

    VDM2002 Third VDM Workshop   2002年7月

    　詳細を見る

    形式手法は日本ではあまり普及していない。しかしながら、近年、形式手法の普及を目指した様々な活動が行われている。本稿では、日本における実際のシステム開発、教育における形式手法に関する活動を紹介し、形式手法を普及するための方策について議論する。

講演・口頭発表等

  • 機械学習を用いた危険予測システムのためのソフトウェアアーキテクチャ設計

    ソフトウェアサイエンス研究会2023年7月研究会   2023年7月  電子情報通信学会

    　詳細を見る

    概要（Abstract） 本研究では，自動運転システムにおける物体検知および危険予測に機械学習技術を応用することを目的とする．LiDAR センサから得られる3 次元点群データをもとに，機械学習を用いた物体検出と危険予測を行うアーキテクチャを提案する．機械学習技術を用いた危険予測システムの実行時間と予測精度という対立する要求の調整に向けて，実行時間と予測精度を考慮した複数のCNN やLSTM，QRNN を採用した．さらに，機械学習技術の進歩に伴って使用技術の変更や追加を想定し，アーキテクチャを定義した．提案アーキテクチャに基づいてプロトタイプの実装を行い，実験を行った．実験結果から対立要求解決の着想の妥当性を定量的に示すとともに，新技術への追従の観点から，変更容易性について定性的に議論した．

  • FRAM to Contextualise Specifications of Software Systems

    The 14th FRAMily Meeting  2022年11月 

  • 並行システムデバッグ支援のためのフォールトパターンに関する考察

    情報処理学会第59回組込みシステム研究発表会  2022年3月  情報処理学会

  • FRAMとVDMを用いた要求仕様記述支援に関する考察

    FRAM Workshop（第3回 AI/IoTシステム安全性シンポジウム）  2021年12月  JST未来社会創造事業

  • 同時に起こる事象を考慮した区間振る舞いモデルの提案

    第56回組込みシステム研究発表会  2021年3月  情報処理学会

  • MVCに基づいた組み込みソフトウェアの形式仕様メタモデルに関する考察

    情報処理学会第53回組込みシステム研究会  2020年2月  情報処理学会

    　詳細を見る

    本研究の目的は，組み込みソフトウェアにおける形式仕様のメタモデルを提示することである．本研究の基本的なアイデアは，対象に対する機能と振る舞いの2 つの視点から，MVC アーキテクチャに基づいて仕様の構造を整理することである．形式仕様のメタモデルは，仕様のメタモデルにおける表現（ビュー）の構造に特徴づけられる．提案するメタモデルは，視点に応じた仕様記述のための，形式的な表現と非形式的な表現が混在する記法定義の基盤となる．

  • MVCアーキテクチャに基づく形式仕様と仕様記述プロセスに関する考察

    情報処理学会第50回組込みシステム研究会  2019年3月  情報処理学会

    　詳細を見る

    ソフトウェア開発における形式仕様導入の障壁として，形式仕様の難解さと記述のための適切な指針がないことがあげられる．本稿では，形式仕様のモデルを MVC アーキテクチャの概念に基づいて定義し，詳細化関係を考慮した構成要素および要素間の関係を整理する．

  • MVCアーキテクチャのメタレベル適用による形式仕様モデルに関する考察

    第44回組込みシステム研究発表会  2017年3月  情報処理学会

  • 並列事象の同時生起を考慮した振る舞い仕様記述法に関する考察

    第23回ソフトウェア工学の基礎ワークショップ（FOSE2016）  2016年12月  日本ソフトウェア科学会ソフトウェア工学の基礎研究会

  • 自動販売機システム開発文書への形式仕様記述の適用事例

    情報処理学会第191回ソフトウェア工学研究発表会  2016年3月  情報処理学会

  • 同時性を考慮した並行システムの振舞い検証に関する考察

    情報処理学会第36回組込みシステム研究発表会  2015年3月  情報処理学会

    　詳細を見る

    プロセス代数 CSP を用いて並行システムの同時性を定義し，同時性を考慮した振舞い検証の枠組みを提示した．同時性の仕様記述を一般化してモジュール化することにより，同時性に関する仕様と検証の記述を容易にした．

  • A Discussion on the Verification of Concurrent Systems based on E-AoSAS++

    International Symposium on Practical Formal Approaches to Software Development  2014年10月  Research Center for Architecture-Oriented Formal Methods, Kyushu University and Graduate School of Information Science and Electrical Engineering, Kyushu University

    　詳細を見る

    アスエペクト指向ソフトウェアアーキテクチャスタイル E-AoSAS++ を用いた設計に対して，プロセス代数 CSP を用いた検証手法を提示した．

  • 際どい実行順序を考慮した並行システム検証に関する考察

    情報処理学会組込みシステム研究会  2014年3月  情報処理学会

  • パターンを用いたフォールト検出法

    第20回ソフトェア工学の基礎ワークショップ  2013年11月  日本ソフトウェア科学会

  • パターンを用いたフォールト検出

    ワークショップ：プログラム・デバッグ自動化の現状と今後（ソフトウェアエンジニアリングシンポジウム2013）  2013年9月  情報処理学会ソフトウェア工学研究会

  • アーキテクチャ指向開発における形式手法の適用に関する考察

    情報処理学会組込みシステム研究会  2013年3月  情報処理学会

  • フォールトパターンを用いたデバッグ支援

    第19回ソフトウェア工学の基礎ワークショップ（FOSE2012）  2012年12月  日本ソフトウェア科学会

  • ネットワークの振る舞いに依存するシステムへの形式的手法の適用の検討

    電子情報通信学会ソフトウェアサイエンス研究会  2012年11月  電子情報通信学会

  • 並行システム記述におけるフォールトパターンに関する考察

    電子情報通信学会ソフトウェアサイエンス研究会  2012年11月  電子情報通信学会

  • パターンを用いたフォールトの検出に関する考察

    ソフトウェア・シンポジウム 2012  2012年6月  ソフトウェア技術者協会

▼全件表示

共同研究・競争的資金等の研究課題

  • 不確かな振舞いをもつモジュールの影響を考慮した品質主導型CPS設計方法論

    2023年

    日本学術振興会   科学研究費補助金　日本学術振興会  

    　 詳細を見る

    資金種別：競争的資金

    配分額：3700円

    本研究の目的は，不確かな振舞いを示すモジュールがCPS（サイバーフィジカルシステム）の品質特性に与える影響を解明し，高品質のCPSアプリケーション開発を支援する工学的基
    盤としての設計方法論を確立することである．機械学習技術の一般化に伴い，その挙動を決定的に予測できないモジュールがCPSにおいても使用されるようになってきた．これら不確かな振舞いをもつモジュール（以下，「機械学習モジュール」と呼ぶ）の存在を前提としながらCPSの品質を保証するための方法論を，ソフトウェアアーキテクチャに関する設計知識の拡張に基づいて定式化する．

  • 並行プロセス記述デバッグ支援のための誤り軌跡パターンに関する研究

    2022年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

  • 同時性を含む区間振る舞いモデルの形式化と事象の抽象化支援に関する研究

    2021年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

    　 詳細を見る

    配分額：300000円

  • 並行システムにおける同時性を考慮した形式仕様の構成法と検証手法に関する研

    2020年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

    　 詳細を見る

    配分額：300000円

  • IoTシステムのための品質主導型ソフトウェアアーキテクチャ設計手法の研究

    2020年

    日本学術振興会  科学研究費補助金　基盤研究(C)  基盤研究(C)

    　 詳細を見る

    資金種別：競争的資金

    配分額：4290000円

  • アーキテクチャに基づく区間振る舞いモデルを用いた記述法と形式検証法

    2019年

    南山大学  科学研究費補助金　基盤研究(C)(一般)  基盤研究(C)

    　 詳細を見る

    担当区分：研究代表者  資金種別：競争的資金

    配分額：3300000円

    高度に情報化されたネットワーク社会では，異なったシステムを統合してシステムのシステムを構築することが求められる．このようなシステムの信頼性を高めるためには，従来のテスト技術だけでは十分ではなく，設計の信頼性を高めるために，仕様記述に対する設計記述を検証する技術の実用化が必要不可欠である．並列に動作するシステムでは，複数の事象が並列に発生するので，同時に発生する事象を考慮する必要がある．この並列事象の同時性を正しく認識できないことはシステム障害（failure）の原因となる．これは，並列システムにおける並列事象を並行システムとして実現するさいに，適切に並行事象として記述していないことが起因する．本研究では，並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様の記述法とその検証法を体系化することにより，形式検証技術の実用化を目指す．

  • アーキテクチャに基づく同時性を考慮した振る舞い仕様の形式化に関する研究

    2019年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

    　 詳細を見る

    配分額：300000円

    並列に動作するシステムでは，複数の事象が同時に発生する可能性があり，この並列事象の同時性を正しく認識できないことがシステム障害（failure）の原因となる．並列事象の同時性を区間に局所化した「区間振る舞いモデル」を提案し，並列事象の同時性を並行システムとして実現するさいの振る舞い仕様記述法の実用化を目指す

  • 組込みシステムの形式仕様モデルに関する研究

    2018年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

  • 組み込みシステムにおける区間振る舞いモデルを用いた並列システム検証支援に関する研究

    2017年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

  • 区間の概念を用いた分散システム検証支援に関する研究

    2016年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

  • 協調シミュレーションを用いた組み込みシステム設計の検証技術に関する研究

    2015年

    南山大学  南山大学パッヘ研究奨励金I-A-1 

  • ソフトウェアアーキテクチャの検証技術の体系化に関する研究

    2014年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

  • アーキテクチャ指向開発における実行前検査および検証支援に関する研究

    2013年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

  • アーキテクチャ指向形式手法に基づく高品質ソフトウェア開発法の提案と実用化

    2012年

    日本学術振興会   科学研究費補助金　基盤研究（S） 

    　 詳細を見る

    担当区分：研究分担者  資金種別：競争的資金

    配分額：122200000円

  • クラウドソフトウェアのための関心事分離に基づくプロダクトライン構築方式

    2012年

    日本学術振興会  科学研究費補助金　基盤研究（C） 

    　 詳細を見る

    担当区分：研究分担者  資金種別：競争的資金

    配分額：4000000円

  • 確率的言語モデルを用いたソフトウェア解析の研究

    2010年

    日本学術振興会  科学研究費補助金 

    　 詳細を見る

    担当区分：研究分担者  資金種別：競争的資金

    配分額：3300000円

    基盤研究（C）

  • プロダクトラインソフトウェア工学における要求とアーキテクチャとの関連付け

    2009年

    日本学術振興会  科学研究費補助金 

    　 詳細を見る

    担当区分：研究分担者  資金種別：競争的資金

    配分額：1500000円

    基盤研究（C）

  • ソフトウェア仕様記述の形式化に関する研究

    2003年

    日本学術振興会  日韓科学協力事業 

    　 詳細を見る

    研究助成

  • 形式手法による組込み制御システムの設計手法

    2002年

    南山大学  南山大学パッヘ研究奨励金I-A-2 

    　 詳細を見る

    研究助成

  • 形式手法に基づく高品質組込み制御システム開発法の系統化に関する基礎的研究

    2001年

    日本学術振興会  科学研究費補助金 

    　 詳細を見る

    資金種別：競争的資金

    研究助成

  • ネットワークソフトウェアの形式的構成法に関する研究

    2001年

    南山大学  南山大学パッヘ研究奨励金I-A 

    　 詳細を見る

    研究助成

  • 形式手法に基づいた組込みシステム開発手法

    　 詳細を見る

    本研究の目的は，形式手法に基づいた組込みシステムの開発支援技術を提示することである．実際の組込みシステムを対象として，システムのモデルを構築するとともに，形式手法による組込みシステムの仕様と設計の分析を行い，仕様と分析の間の関連を明らかにする。

  • 形式手法に基づいたソフトウェア開発支援環境

    　 詳細を見る

    本研究の目的は，理論的な方法論を土台とした，実用的なソフトウェア開発手法を提示することである．実際のソフトウェア開発に基づいて，要求定義，仕様記述，設計，実装における開発作業の本質を解明することにより，形式手法（フォーマルメソッド）に基づいたソフトウェア開発支援技術の体系化をはかり，その支援環境を構築する。

▼全件表示

その他

  • プログラム委員

    2006年2月 - 2006年11月

    　詳細を見る

    ソフトウェア工学の基礎ワークショップ(FOSE2006)

  • プログラム委員

    2005年10月 - 2006年7月

    　詳細を見る

    ソフトウェアシンポジウム2006

  • プログラム委員

    2005年2月 - 2005年11月

    　詳細を見る

    ソフトウェア工学の基礎ワークショップ(FOSE2005)

  • プログラム委員

    2003年

    　詳細を見る

    組込みソフトウェアシンポジウム2003

  • 広報委員長

    2003年

    　詳細を見る

    オブジェクト指向2003シンポジウム

  • プログラム委員

    2003年

    　詳細を見る

    ソフトウェアシンポジウム2003

  • プログラム委員

    2003年

    　詳細を見る

    ソフトウェア工学の基礎ワークショップ（FOSE'03）

  • プログラム委員

    2002年10月

    　詳細を見る

    ソフトウェア工学の基礎ワークショップ（FOSE2002）

  • プログラム委員

    2002年7月

    　詳細を見る

    ソフトウェアシンポジウム2002

  • 運営委員

    2002年4月 - 2005年3月

    　詳細を見る

    情報処理学会ソフトウェア工学研究会

  • 編集委員

    2002年4月 - 2004年3月

    　詳細を見る

    情報処理学会数理モデル化と問題解決研究会

  • 運営委員

    2002年4月 - 2004年3月

    　詳細を見る

    情報処理学会システム評価研究会

  • プログラム委員

    2001年11月

    　詳細を見る

    ソフトウェア工学の基礎ワークショップ（FOSE2001）

▼全件表示