CPU設計導入教育への形式的設計検証手法の適用
スポンサーリンク
概要
- 論文の詳細を見る
形式的手法の設計導入教育への適用の有用性を調べるために, 大阪大学基礎工学部情報科学科3年次学生のCPU設計実験において, (i)我々の研究グループで作成した検証システムを用いて設計の正しさを形式的に証明する設計手法(新手法), (ii)慎重な見直しや波形シミュレーションなどで設計の正しさを確認する設計手法(従来手法)、の2つのコースを設けて, その2つのコース間で作業時間と設計したCPUにおける誤りの有無について2ヵ年にわたって比較を行った.定められた中間レポート提出期限までに誤りのないCPUを設計した学生は, 従来手法コースでは42人中0人, 新手法コースでは42人中41人であった.従来手法コースでは提出期限後に, 教官が誤りを指摘して学生が設計を修正する期間を設け, この期間に19人が誤りのないCPUを設計した.中間レポート提出期限までに費やした全作業時間の平均は新手法43時間に比べて従来手法のほうが13時間ほど短かった.以上より, あらかじめ定められた期限までに正しいCPUを設計するためには, 新手法は30%ほど作業時間がかかるものの効果的であることが確かめられた.
- 2000-11-15
著者
-
岡野 浩三
大阪大学大学院情報科学研究科
-
北嶋 暁
大阪大学大学院基礎工学研究科情報数理系専攻
-
谷口 健一
大阪大学大学院情報科学研究科
-
北嶋 暁
大阪電気通信大学総合情報学部メディアコンピュータシステム学科
-
北浜 優子
大阪大学大学院基礎工学研究科
関連論文
- Strutsフレームワークにおけるメタモデルを用いた追跡可能性実現手法の提案(アスペクト指向・Web)
- データ付時間オートマトンの双模倣等価性の記号的検証法
- 反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法
- 確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較
- UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
- SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法
- UML/OCLに記述された時間QoSの階層的検証手法の提案
- 確率的モデル検査ツールPRISMによるリアルタイム分散システムのネットワーク遅延を考慮した検証手法について
- SPINによるStrutsアプリケーションの動作検証を目的としたモデル生成手法の提案
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
- データタイプを考慮したASIP消費電力見積り手法の提案
- データタイプを考慮したASIP消費電力見積り手法の提案
- 命令インタリーブ発行機構を有するマルチスレッド向けプロセッサの提案
- 拡張時間オートマトン群による実時間システムの記述および検証
- 時間システムを対象とした到達可能性解析の高速化手法の提案
- 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
- OCLのJMLへの変換ツールの実装と評価
- OCLのJMLへの変換ツールの実装について
- 実時間システムを対象としたCEGARによる抽象洗練の並列化手法
- Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
- 上位設計におけるシステムの振る舞い検証技術(システム設計のための形式手法の基礎と応用)
- B-001 Javaに対するDaikonを用いたインバリアント自動生成のための汎用基盤ツール(ソフトウェア,一般論文)
- JMLを用いた在庫管理プログラムの設計とESC/Java2を用いた検証
- 制約指向に基づいたUMLモデルの不整合検出・解消手法の提案(ソフトウェア,フォーマルアプローチ論文)
- 時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,フォーマルアプローチ論文)
- Daikonの限定利用によるJavaメソッドの事後条件の自動導出
- UMLモデルに対するXPathとXMI-differenceを用いた不整合検出と解消
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- D-3-6 分散実時間アプリケーションのUML/OCL記述から時間オートマトンネットワークを用いた動作仕様記述への変換手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- 分散環境実時間アプリケーション開発支援のためのTimeliness QoS一貫性検証系および時間制御コード生成系の実装
- 関数型言語ML向け形式的検証支援システムの試作
- 線形制約式を用いた時間QoS一貫性の検証法 (計算機科学基礎理論の新展開)
- 関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
- D-3-8 分散環境における実時間アプリケーション動作仕様記述からのJavaコード自動導出手法の提案(D-3. ソフトウェアサイエンス)
- マルチメディアシステムにおけるTimeliness QoS一貫性検証と時間制御コード導出
- ペトリネットで記述された簡易ブラウザ型の組込みJavaプログラム動作仕様に対する実行方式の提案
- ワークフロー記述向きの時間付きカラーペトリネット
- 時間制約付きカラーペトリネットで記述されたワークフローからのスケジュール導出
- 時間制約を持つGUI制御部の仕様記述の一手法
- 凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
- 入力値のみ保持する変数をもつEFSM群に対する動的性質の検証
- CPU設計導入教育への形式的設計検証手法の適用
- 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
- 1G-6 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
- 複数時間オートマトンによる仕様記述と検証
- 組合わせ幾何を用いた有理数プレスブルガー文真偽判定アルゴリズムにおける投影操作の高速化
- 時間ペトリネットの拡張モデルを用いたプロトコル合成
- Tarski算術における冠頭標準形の閉論理式の真偽判定アルゴリズムの提案
- 耐故障性のための多重化リソースを持つ分散システムの導出法
- GUI制御部の記述と実現の一手法
- 規則右辺に照合外変数を含む条件付き項書換え系における階層合流性のモジュラ性
- MANETにおける位置情報マルチキャストルーティングMgCastの提案と性能評価(無線・モバイルネットワーク)
- 階層的キーワードベースの名前管理におけるキーワード管理手法
- あるクラスのOut-of-Order型パイプラインCPUの設計の正しさの十分条件とその形式的検証 (電子システムの設計技術と設計自動化)
- 多人数参加型アプリケーションにおける品質要求を考慮した帯域制御の一方式(マルチメディア通信と分散処理)
- 動画の品質劣化の許容度を考慮した帯域制御の一方式
- 帯域割譲交渉による動的帯域制御方式
- 品質要求を考慮した動的な帯域制御を行うプロトコルの提案とその性能評価
- 階層的キーワードに基づく名前管理手法とそれに基づくファイル共有手法
- 階層的キーワードに基づく名前管理手法とそれに基づくファイル共有手法
- MANETアプリケーション向けのシミュレータMobiREALの実装に関する検討(セッション2)(テーマ:モバイルコンピューティング,ITS,放送コンピューティング)
- MANETアプリケーション向けのシミュレータMobiREALの実装に関する検討(セッション2)(テーマ:モバイルコンピューティング,ITS,放送コンピューティング)
- データ付時間オートマトンの双模倣等価性の記号的検証法
- アプリケーション層マルチキャストミドルウェアにおける携帯端末への映像配信機構の実装(モバイルコンピューティングとユビキタス通信高度交通システム合同研究報告)
- アプリケーション層マルチキャストミドルウェアにおける携帯端末への映像配信機構の実装(モバイルコンピューティングとユビキタス通信高度交通システム合同研究報告)
- アプリケーション層マルチキャストミドルウェアにおける携帯端末への映像配信機構の実装
- 同期通信可能な周期EFSM群のハードウェア構成法
- 大規模ネットワークシミュレーション向けのルーティングテーブルの容量削減(ネットワーク品質・制御)
- 動画像を用いたコミュニケーションシステム向けのアプリケーション層マルチキャスト
- エンドホストの動画像フィルタリングによるアプリケーション層でのQoSマルチキャストプロトコルの提案(ネットワークプロトコル)(ブロードバンドネットワークサービス)
- モバイルアドホックネットワークシミュレーションの規模適応性を向上させる技法の検討(モバイルコンピューティングとユビキタス通信高度交通システム合同研究報告)
- MANETにおける位置情報マルチキャストルーティングMgCastの性能評価と応用に関する検討(モバイルコンピューティングとユビキタス通信高度交通システム合同研究報告)
- マルチランデブチャネルの動的確立機構を持つモバイルアプリケーション記述言語の提案(ソフトウェア工学の基礎)
- 並行モバイルエージェント間でのマルチランデブチャネルの動的設定が記述可能な言語とその実装
- SMILへのQoS保証文の導入とその柔軟な実装法(マルチメディアネットワークシステム)
- digitシリアル演算を用いたDSPシステム設計最適化の一手法
- 形式的手法を用いたin-order実行パイプラインCPUの自動設計検証(並列処理)
- digitシリアル演算を用いたDSPシステム設計最適化の一手法
- ASIP開発システムPEAS-IIIのための命令セットレベルシミュレータの自動生成
- パイプライン段数を考慮したASIP設計最適化の検討
- VHDLで記述されたシステム仕様のプロセスレベルでのHW/SW分割の一手法
- VHDLで記述されたシステム仕様のプロセスレベルでのHW/SW分割の一手法
- 複数反例抽出を用いたCEGARによる時間オートマトンの抽象洗練手法
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (知能ソフトウェア工学)
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (ソフトウェアサイエンス)
- OCLからJMLへの変換ツールにおける対応クラスの拡張と教務システムに対する適用実験
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価
- モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価
- 制約記述言語OCLとJMLのモデル駆動開発技法に基づいた双方向の変換手法の提案
- SMTソルバーとPDG作成ツールを用いたJavaのテストケース自動導出手法の提案
- PDGとSMTソルバを利用した表明自動導出手法の提案と評価(ソフトウェア工学,ソフトウェア基礎・応用論文)
- 契約記述の変更傾向の開発履歴情報を用いた調査
- 契約記述の変更傾向の開発履歴情報を用いた調査
- 異なるスキーマ間に対応するSQL文の整合性のAlloy Analyzerを用いた一検証手法
- 制約記述言語OCLとJMLのモデル駆動開発技法に基づいた双方向の変換手法の提案
- SMTソルバーとPDG作成ツールを用いた Java のテストケース自動導出手法の提案