An Efficient System Verification based-on Check-points Extraction Method
スポンサーリンク
概要
- 論文の詳細を見る
Recently, model checking has played an important role in design of embedded systems, complex systems, and othercritical systems. However, it is inefficiency to verify the entire systems. This article considers the case where designers of systems can extract check-points easily in model checking offormal verification. Moreover, we propose a method by which temporal formulas can be obtained inductively for specificationsin model checking. Finally, we demonstrate verification results for some arbitration modules by NuSMV model checking tool.
- 沖縄工業高等専門学校の論文
著者
関連論文
- 小型組込み機器を用いた機能分散型システムの構築
- MIPSアーキテクチャ非同期プロセッサの設計とFPGA実装
- 非同期MIPSプロセッサの設計およびFPGA実装
- UML設計による組込み向けHW/SW雛形コード生成ツールの開発
- 小型組込み機器への暗号システムの実装
- 画像処理アルゴリズムのFPGAへの実装と評価
- Linux 搭載可能組込み評価ボードを用いた組込み開発実習の事例
- D-10-20 Reduced-STGとStrong/Weak temporal orderによる非同期式回路の検証
- 5-107 島嶼県沖縄における中学校に対する理科教育支援の実践(口頭発表論文,(23)地域貢献・地場産業との連携-II)
- D-18-3 機能分散型システムの小型組込み機器への実装(D-18.リコンフィギャラブルシステム,一般セッション)
- D-15-16 出席管理と寮生活管理を統合した学生生活支援システムの構築(D-15.教育工学,一般セッション)
- D-15-10 工学実験における視野映像の視覚化の検討(D-15.教育工学,一般セッション)
- D-10-4 高専カリキュラムへの高専版組込みスキル標準のマッピング(D-10.ディペンダブルコンピューティング,一般セッション)
- 8-215 高専連携による組込みシステム教育に関する取組み(口頭発表論文,(07)教材の開発-II)
- 6-102 高専教育におけるモデルベース組み込みシステムの導入 : 上流設計と実装設計の融合(口頭発表論文,(18)工学教育システムの個性化・活性化)
- 実践的なモデルベース開発のキーポイントを探る
- PCとFPGAが連携したシステムにおける簡易コード生成法の検討
- エンジン実習装置における点火時期制御の検討
- An Efficient System Verification based-on Check-points Extraction Method
- 暗号アルゴリズムの遠隔再構成システムへの実装
- D-15-9 高専版組込みスキル標準の構築(D-15.教育工学,一般セッション)
- D-15-22 出欠管理と授業改善アンケートによる教育実践の取組み(D-15.教育工学,一般セッション)
- D-18-1 確定的素数判定向けべき乗剰余演算器の改良に関する一考察(D-18.リコンフィギャラブルシステム,一般セッション)
- 学生生活支援のための出席管理システムの実践的運用
- 点火時期制御に基づくエンジン実習装置の検討
- Miller-Rabin 素数判定法におけるべき乗剰余演算部の構成
- ブラックボードの統合化による運用とその効果
- 携帯端末活用による学生生活カルテシステムの構築(エンタテインメントを活用した学習環境/一般)
- A-7-5 確定的素数判定法のハードウェア化に関する検討(A-7.情報セキュリティ,一般セッション)
- A-4-25 股関節CT画像からの骨外形抽出について(A-4.信号処理,一般セッション)
- リアルタイム出欠登録管理システムの教育的質向上効果に関する研究
- 学生生活支援システムによる教育改善への取組み
- 社会ニーズに即したモデルベース開発の教育システム構築 : 高専間連携によるモデルベース開発教材の開発
- D-15-9 シラバス特徴抽出システムの開発(D-15.教育工学,一般セッション)
- RSA暗号における剰余乗算回路の評価
- 楕円曲線素数判定法を用いた鍵生成組込み型RSA暗号システムのFPGA実装
- 高専版組込みスキル標準の開発と実践(Web技術と先端的学習支援/一般)
- 非同期式ALUの構成
- 高専版組込みスキル標準の開発と実践
- 重みの対称性を用いた適応的バイラテラルフィルタの高速化
- 複数台カメラを用いた簡易なポインティングデバイスの開発
- Towards Okinawa-style Robot-embedded Systems
- K-039 エンジニアリングデザイン教育を考慮した学生主導による実験(教育工学(5),K分野:教育工学・福祉工学・マルチメディア応用)
- A-4-6 分布間距離を用いたBilateral Filterのパラメータ推定法(A-4.信号処理,一般セッション)
- 離島中学校への体育の出前授業の教育効果
- Okinawa 型ロボット組み込みシステムに向けて
- C-016 Coarsely Integrated Operand Scanningアルゴリズムに基づくモンゴメリ乗算器の回路規模縮小手法の検討(C分野:ハードウェア・アーキテクチャ,一般論文)
- I-032 重みの対称性と空間分解による適応的バイラテラルフィルタの高速化の検討(I分野:グラフィクス・画像,一般論文)
- エンジニアリングデザイン教育を目的とした学生主導型実験の取組み
- マイコンを利用したジョイスティック型マウスの操作性改善
- 分布間距離に基づいたバイラテラルフィルタのパラメータ推定法の一考察
- Adaptive Bilateral Filter の高速化の検討