検索結果 87件中 1-20 を表示

  • 1 / 5
  • 有界モデル検査の高速化を指向した差分論理に基づく時間ペトリネットの論理式表現 (ソフトウェアサイエンス)

    井川 直 , 横川 智教 , 宮崎 仁 , 近藤 真史 , 佐藤 洋一郎 , 有本 和民

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116(426), 59-64, 2017-01-26

  • 有界モデル検査の高速化を指向した差分論理に基づく時間ペトリネットの論理式表現 (システム数理と応用)

    井川 直 , 横川 智教 , 宮崎 仁 , 近藤 真史 , 佐藤 洋一郎 , 有本 和民

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116(425), 59-64, 2017-01-26

  • 適応的重点サンプリングによる統計的モデル検査手法

    西木 悠 , 結縁 祥治

    本研究では,フォールトツリー解析と適応的重点サンプリングを使用した統計的モデル検査手法を提案する.統計的モデル検査はモンテカルロ法と時相論理による検証を組み合わせた軽量形式手法の一種である.統計的モデル検査において主となる問題は稀な事象の検証である.モンテカルロ法の稀な事象の検証に対処可能な方法として,適応的重点サンプリングがある.目的となる性質の充足可能性を検査する直接的なサンプリングでは,適応 …

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 114(510), 37-42, 2015-03-02

  • 割込み遷移削減手法を導入した組込みアセンブリコード向けSMTベースモデル検査器の開発(離散事象システム及び一般)

    小橋 潤平 , 竹下 淳 , 山根 智 [他] , 櫻井 孝平

    近年の発展を続けている組込みシステムにおいて,ハードウェアに依存する性質を持つソフトウェアが用いられており,開発期間の短縮や信頼性の向上の観点から,それらの性質に対応した形式的検証手法について需要が高まっている.本論文ではSMTソルバを用いた有界モデル検査を検証手法として採用し,アセンブリプログラムを対象とした詳細なモデル検査手法,及びアセンブリコードのコードブロックを利用したモデル化手法について …

    電子情報通信学会技術研究報告. MSS, システム数理と応用 114(493), 53-58, 2015-02-26

  • Bounded model checking of Time Petri Nets using SAT solver

    Yokogawa Tomoyuki , Kondo Masafumi , Miyazaki Hisashi , Amasaki Sousuke , Sato Yoichiro , Arimoto Kazutami

    … The TPN model needs to satisfy required properties such as deadlock freeness. … We proposed a symbolic representation of TPN for SAT-based bounded model checking. …

    IEICE Electronics Express 12(2), 20141112-20141112, 2015

    J-STAGE DOI

  • 有界な時区間におけるコスト制約問題としての電力消費解析(形式方法)

    中島 震

    電力供給を電池に頼るシステムでは、意図しない電力消費が大きな問題となる。開発の初期段階からソフトウェアに起因する電力消費の問題を検討するモデルベース解析の方法が期待されている。形式的な解析が可能な厳密な表現として、電力消費オートマトンならびに時相論理に基づく性質記述の方法が提案された。本稿では、電力消費に関わる典型的な検査パターンを時相論理の枠組みで表し、さらに、既存のモデル検査ツールReal-T …

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 114(271), 29-34, 2014-10-16

  • 組込みアセンブリプログラム解析によるSMTモデル検査

    小橋 潤平 , 山根 智 , 竹下 淳

    組込みシステムシンポジウム2014論文集 2014, 22-27, 2014-10-15

    情報処理学会

  • Runtime Control of a Program based on Quantitative Information Flow (ソフトウェアサイエンス)

    CHU Bao Trung , HASHIMOTO Kenji , SEKI Hiroyuki

    … We also report on the experiments conducted by a prototype system based on bounded model checking and model counting of a Boolean formula. …

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 113(422), 71-76, 2014-01-23

  • CISC型組込みアセンブリプログラムのSMTベースの有界モデル検査

    竹下 淳 , 小橋 潤平 , 山根 智

    本研究では,組込みシステム向けアセンブリプログラムのコードブロックを対象とした,SMT有界モデル検査手法による性質検証を述べる.アセンブリプログラムのコードブロック生成規則とモデル化について提案する.また,実際のプログラムに対して提案手法によるコード変換を行った.

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 113(422), 65-70, 2014-01-23

  • Runtime Control of a Program based on Quantitative Information Flow (システム数理と応用)

    CHU Bao Trung , HASHIMOTO Kenji , SEKI Hiroyuki

    … We also report on the experiments conducted by a prototype system based on bounded model checking and model counting of a Boolean formula. …

    電子情報通信学会技術研究報告. MSS, システム数理と応用 113(421), 71-76, 2014-01-23

  • CISC型組込みアセンブリプログラムのSMTベースの有界モデル検査

    竹下 淳 , 小橋 潤平 , 山根 智

    本研究では,組込みシステム向けアセンブリプログラムのコードブロックを対象とした,SMT有界モデル検査手法による性質検証を述べる.アセンブリプログラムのコードブロック生成規則とモデル化について提案する.また,実際のプログラムに対して提案手法によるコード変換を行った.

    電子情報通信学会技術研究報告. MSS, システム数理と応用 113(421), 65-70, 2014-01-23

  • Bounded Model Checking of Time Petri Nets using SAT Solver

    Yokogawa Tomoyuki , Kondo Masafumi , Miyazaki Hisashi , Amasaki Sousuke , Sato Yoichiro , Arimoto Kazutami

    … The TPN model needs to satisfy required properties such as deadlock freeness. … We proposed a symbolic representation of TPN for SAT-based bounded model checking. …

    IEICE Electronics Express advpub(0), 2014

    J-STAGE DOI

  • ハイブリッド制約言語HydLaの記号実行シミュレータHyrose

    松本 翔太 , 上田 和紀

    ハイブリッドシステムとは時間の経過に伴って状態が連続変化したり,状態や方程式系が離散変化したりする動的システムであり,物理学をはじめとした様々な分野への応用が可能である.HydLaはハイブリッドシステムの仕様を制約によって記述する宣言型言語であり,今回我々はHydLaの記号実行シミュレータとしてHyroseを開発した.Hyroseは公開されている唯一のHydLaの実装であり,パラメータを含むシステ …

    コンピュータソフトウェア 30(4), 18-35, 2013-10-25

    J-STAGE DOI 参考文献19件

  • Automated Error Localization with Weighted Partial Maximum Satisfiability (知能ソフトウェア工学)

    LAMRAOUI Si-Mohamed , NAKAJIMA Shin

    Localizing error in programs is a hard task that requires human engineers to find real bug locations with the manual analysis of lengthy counterexample traces. Automatic error localization methods exi …

    電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学 113(160), 1-6, 2013-07-18

  • Automated Error Localization with Weighted Partial Maximum Satisfiability (ソフトウェアサイエンス)

    LAMRAOUI Si-Mohamed , NAKAJIMA Shin

    Localizing error in programs is a hard task that requires human engineers to find real bug locations with the manual analysis of lengthy counterexample traces. Automatic error localization methods exi …

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 113(159), 1-6, 2013-07-18

  • Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker

    KITAMURA Takashi , OKAMOTO Keishi

    … In this paper, we propose and implement an automated route planning framework for milk-run transport logistics by applying model checking techniques. … Then by applying the bounded semantics of LTL, the framework then defines the notion of "optimal truck routes", which mean truck routes on a given route map that satisfy given delivery requirements (specified by LTL) with the minimum cost. …

    IEICE Transactions on Information and Systems E96.D(12), 2555-2564, 2013

    J-STAGE DOI

  • A New Formal Verification Approach for Hardware-dependent Embedded System Software

    Schmidt Bernard , Villarraga Carlos , Fehmel Thomas , Bormann Jörg , Wedler Markus , Nguyen Minh , Stoffel Dominik , Kunz Wolfgang

    … This paper describes a method to generate a computational model for formal verification of hardware-dependent software in embedded systems. … The computational model of the combined HW/SW system is a <i>program netlist</i> … The model can be easily integrated into SAT-based verification environments such as those based on Bounded Model Checking (BMC). …

    IPSJ Transactions on System LSI Design Methodology 6(0), 135-145, 2013

    J-STAGE DOI

  • 確率線形ハイブリッドオートマトンの到達可能性検証

    畠中 克也 , 山根 智

    … procedureを拡張し,確率線形ハイブリッドオートマトンに対する検証を可能にする.さらに,モデルに対する検証を自動化するため,拡張したprocedureを計算機上に実装する.ケーススタディとして,無線センサネットワークをとりあげ,確率線形ハイブリッドオートマトンによるモデル化と,その検証例を示す.Model checking is a formal method exhaustively verifying whether behaviors of a system satisfy specific characteristics. …

    情報処理学会論文誌 53(12), 2671-2681, 2012-12-15

    情報処理学会 情報処理学会

  • アセンブリプログラムに対するSMTソルバを使用する有界モデル検査

    小橋 潤平 , 竹下 淳 , 山根 智

    本稿では,組み込みシステム向けアセンブリ言語プログラムコードのレジスタレベルモデルに対して,SMTソルバを用いた有界モデル検査手法による性質検証を述べる.SMTソルバを用いた検証手法とアセンブリコードのモデル化について提案し,簡単なアセンブリプログラムに対して提案した手法による性質検証を行なった.

    電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学 112(314), 19-24, 2012-11-15

    参考文献16件

  • 組込みアセンブラのSMT検証手法の提案と実装

    竹下 淳 , 小橋 潤平 , 山根 智

    組込みシステムシンポジウム2012論文集 2012, 197-202, 2012-10-10

    情報処理学会

  • 1 / 5
ページトップへ