| 電子情報通信学会 研究会発表申込システム 研究会 開催スケジュール |
技報閲覧サービス [ログイン] 技報アーカイブ |
すべての研究会開催スケジュール (検索条件: すべての年度)
| 研究会 | 発表日時 | 開催地 | タイトル・著者 | 抄録 | 資料番号 | |
| KBSE | 2024-03-15 13:20 |
沖縄 | 沖縄県総合福祉センター （ハイブリッド開催，主：現地開催，副：オンライン開催） |
可変性モデル分割手法の改善 ○岸 知二（早大）  KBSE2023-87 |
可変性モデルの解析や検証は論理に基づいて行われることが多いが，可変性モデルの持つ構成数は組み合わせ的になりうるためスケー... [more] | KBSE2023-87 pp.120-125 |
| KBSE, SC (共催) |
2023-11-17 15:30 |
宮城 | 仙都会館 | スケーラビリティ改善のための可変性モデル分割について ○岸 知二（早大） KBSE2023-37 SC2023-20 |
可変性モデルを利用して論理に基づく解析や検証が行われているが，バリエーションの数は組み合わせ的になるため，近年のシステム... [more] | KBSE2023-37 SC2023-20 pp.31-36 |
| KBSE | 2023-03-16 15:10 |
広島 | JMS アステールプラザ（広島） （ハイブリッド開催，主：現地開催，副：オンライン開催） |
非形式/準形式混成記法に基づくトレーサビリティ管理手法 ○岡田遼嗣・大濱吉紘・伊藤誠悟（豊田中研） KBSE2022-56 |
ソフトウェア及びシステムの設計における仕様情報のトレーサビリティ管理方法として，非形式的な表記法を用いる方法，準形式手法... [more] | KBSE2022-56 pp.13-18 |
| MSS, CAS (共催) IPSJ-AL (連催) [詳細] |
2018-11-13 15:15 |
静岡 | 熱海伊豆山温泉 ハートピア熱海 | 代数仕様を用いた数理計画モデルの形式的検証について ○中村正樹・榊原一紀（富山県立大） CAS2018-76 MSS2018-52 |
最適化ソルバーを数理計画モデルに適用するためには，ソルバーが適用可能な形式にモデル化する必要がある．本研究では，与えられ... [more] | CAS2018-76 MSS2018-52 pp.127-130 |
| SS, KBSE (共催) IPSJ-SE (連催) [詳細] |
2017-07-19 10:45 |
北海道 | 函館コミュニティプラザ | 端末交通システムにおける運行スケジュールのモデル検査法を用いたデッドロック検出手法 ○辻 光顕・長谷部浩二・加藤和彦（筑波大） SS2017-2 KBSE2017-2 |
著者らは車両の自律動作により隊列走行可能な端末交通システムの研究開発を行っている．このシステムの特長は，隊列を再編成する... [more] | SS2017-2 KBSE2017-2 pp.7-12 |
| SS | 2015-03-09 09:55 |
沖縄 | 沖縄県青年会館 | 環境許容性のあるリアクティブシステム合成法 ○上野篤史・冨田 尭・島川昌也・萩原茂樹・米崎直樹（東工大） SS2014-56 |
形式的に記述された仕様からリアクティブシステム（RS）を自動合成する手法では，仕様$varphi_{sys}$を満たす振... [more] | SS2014-56 pp.7-12 |
| VLD, DC, IPSJ-SLDM (連催) ICD, CPM (共催) CPSY, RECONF (併催) [詳細] |
2014-11-26 10:45 |
大分 | ビーコンプラザ（別府国際コンベンションセンター） | タイミング制約を含んだ回路記述方式とその意味論 ○西村俊二・尼崎太樹・末吉敏則（熊本大） VLD2014-82 DC2014-36 |
数学的な理論に基づく厳密な検証が可能となることから，各種の形式検証手法が広がりつつあるが，その検証対象は同期回路に限られ... [more] | VLD2014-82 DC2014-36 pp.81-86 |
| RECONF | 2014-09-19 14:40 |
広島 | 杜の宿 | 様相論理によるマルチクロック同期回路の形式検証体系 ○西村俊二・尼崎太樹・末吉敏則（熊本大） RECONF2014-33 |
数学的な理論に基づく厳密な検証が可能となることから，各種の形式検証手法が広がりつつあるが，多くの場合検証対象は単一クロッ... [more] | RECONF2014-33 pp.93-98 |
| SC, IPSJ-UBI (連催) |
2014-07-28 10:00 |
東京 | 国立情報学研究所 | 異なる形式手法を用いて検査されたサービスの合成結果の検証 ○船越和大・細野 繁（NEC） SC2014-6 |
複数の形式手法を用いてそれぞれ検査されたサービスのモデルとその制約を示す論理式を入力とし，定理証明支援系であるCoq 上... [more] | SC2014-6 pp.49-54 |
| SS | 2014-03-11 10:30 |
沖縄 | てんぷす那覇：第１・２会議室 | SATソルバを活用した決定表作成・検証方式 ○伊藤信治・佐藤直人・金藤栄孝・宮崎邦彦・森 浩起・木村 誠・山口 潔（日立） SS2013-73 |
条件の組合せパターンの考慮漏れを防止する方法の１つとして、決定表の活用が有効である。しかし、決定表は、条件項目の数が多く... [more] | SS2013-73 pp.7-11 |
| IN, NV (併催) |
2013-07-19 15:15 |
北海道 | 北海道大学 工学部アカデミックラウンジ3 | 記号実行によるパケットの抽象化を用いたOpenFlowネットワークのモデル検査方式の提案 ○八鍬 豊・富沢伸行・登内敏夫（NEC） IN2013-54 |
OpenFlowネットワークに対し，モデル検査を用いて転送ループ等の不具合の有無を検証する方式を提案する．モデル検査では... [more] | IN2013-54 pp.107-112 |
| KBSE | 2013-03-14 15:30 |
東京 | 芝浦工業大学 | モデル検査を使ったデッドロック可能性検出 ○猿渡卓也・塚本英昭・神谷慎吾・宮田俊介（NTT） KBSE2012-76 |
形式手法の適用によるITシステムの信頼性向上が期待されている．しかし，形式手法の適用にはモデル作成等の専門的な知識が必要... [more] | KBSE2012-76 pp.43-48 |
| KBSE | 2013-03-15 11:25 |
東京 | 芝浦工業大学 | アーキテクチャに基づく検証ケースの提案 ○山本修一郎（名大） KBSE2012-82 |
システムの妥当性を形式手法だけで検証することは実践的ではない．このため形式手法と，テストやレビュなどとの組み合わせを明確... [more] | KBSE2012-82 pp.79-83 |
| DC | 2012-12-14 17:00 |
福井 | アオッサ(福井) | SMTソルバによる単線自動閉そく装置の検証 ○寺田夏樹（鉄道総研） DC2012-79 |
形式手法によりプログラム仕様の品質を向上させることが期待されている．仕様の検証に関して，定理証明を使用する手法は，厳密な... [more] | DC2012-79 pp.31-36 |
| SWIM | 2012-11-30 11:00 |
東京 | 東海大学（高輪） | Event-Bによるモデル駆動モバイルアプリケーション開発 ○越賀 準・新川芳行（龍谷大） SWIM2012-16 |
近年，ソフトウェアの複雑化にともない，従来の手法ではソフトウェアの信頼性や開発生産性の向上に限界が見えてきたため，上流工... [more] | SWIM2012-16 pp.7-12 |
| SS | 2012-03-13 13:05 |
沖縄 | てんぶす那覇 | Alloyを用いたRuby on Railsアプリケーションの開発支援 ○水谷浩明・結縁祥治（名大） SS2011-64 |
本稿では，Ruby on Rails アプリケーションのソースコードをモデル規範形式仕様記述言語 Alloy による記述... [more] | SS2011-64 pp.43-48 |
| DC | 2011-12-16 14:30 |
兵庫 | 豊岡市社会福祉協議会／城崎地区センター | A Safety Estimation of the ATPB System using UML and Formal Method ○Guo Xie・Hiroshi Mochizuki・Sei Takahashi・Hideo Nakamura（Nihon Univ.） DC2011-70 |
在来線の経営改善と活性化を目指し、新たな列車制御システム「ATP閉そく」が提案された。本論文では、システムの仕様の正当性... [more] | DC2011-70 pp.13-16 |
| SS | 2011-10-28 11:15 |
石川 | 北陸先端科学技術大学院大学 | 有限Alloy記述の段階的な構築について ○小飼 敬（茨城高専）・中島 震（NII）・上田賀一（茨城大） SS2011-36 |
Alloy記述を作成する過程では，記述の確認を行う繰り返し作業の際に，探索スコープを限定したコマンドで解析することが多い... [more] | SS2011-36 pp.55-60 |
| SWIM | 2011-06-17 16:25 |
東京 | 機械振興会館 | Event-BモデルのHaskellによる実装 ○越賀 準・新川芳行（龍谷大） SWIM2011-7 |
近年，ソフトウェアの複雑化にともない，従来の手法ではソフトウェアの信頼性や開発生産性の向上に限界が見えてきたため，上流工... [more] | SWIM2011-7 pp.31-36 |
| SWIM | 2010-11-19 15:25 |
東京 | 東海大学（高輪） | 時間制約を含むUMLシーケンス図の検証手法 ○安田佳宏・新川芳行（龍谷大） SWIM2010-23 |
ソフトウェアの仕様検証は，構造や機能に焦点を当てた静的検証，振る舞いに焦点を当てた動的検証，そして時間制約の検証が独立に... [more] | SWIM2010-23 pp.39-44 |
[研究会発表申込システムのトップページに戻る]