アセンブラのモデル検査におけるモデルの自動生成について(検証・検査手法)
スポンサーリンク
概要
- 論文の詳細を見る
アセンブラプログラムのモデル検査についての知見と,アセンブラプログラムの検査モデルの自動生成について報告する.アセンブラプログラムのモデル検査では,CTL式を使用した到達可能性検査が有効である.また,検査モデルを正確に生成するために,モデル変換スクリプトによるモデルの半自動生成が有効である.
- 2007-05-28
著者
関連論文
- マルチタスクからマルチコアへの対応まで 組み込みOSで使われるマルチタスク技術の歴史 (特集 CPU,OS,部品,プログラミング言語がさまざまな進化を遂げた 進化するコンピュータ・アーキテクチャの30年)
- LTSAとSPINを連携させたタスク設計の提案(組込みシステムプラットフォーム)
- 新・組み込みソフトへの数理的アプローチ(第12回)テストとプログラム検証--TDD(テスト駆動開発)におけるテスト
- 新・組み込みソフトへの数理的アプローチ(第11回)プログラム検証とテスト--CBMCを使ってソース・コードから仕様を検証する
- 組み込みプログラミング・ノウハウ入門(第28回)動作モデル検証ツールを使いこなそう--LTSAで「調教師とライオン」パズルを解く
- 動作要求のモデル化と管理(モデルベース開発)
- 新・組み込みソフトへの数理的アプローチ(第14回)形式仕様記述は役に立つのか--形式手法導入でバグはどれくらい減らせたのか
- 新・組み込みソフトへの数理的アプローチ(第7回)組み合わせ問題とLTSA--モデル検査ツールで組み合わせパターンを列挙する
- 複数シーケンス図を使ったシナリオ検証とタスク設計(モデル表記・モデル検査)
- AS-4-5 モデル検査への事前条件・事後条件検証の導入(離散事象システムとモデル検査,AS-4.組込みシステムの形式的手法,シンポジウム)
- アセンブラのモデル検査におけるモデルの自動生成について(検証・検査手法)
- モデル検査への事前条件・事後条件検証の導入(検証・検査手法)
- モデル検査ツールの利用 マルチコア環境におけるタスク設計検証 (並列プログラミングは難しくない!マルチタスク/マルチコア時代の並列処理技術)
- 組み込みソフトへの数理的アプローチ(第7回)到達可能性と安全性を検証する--NuSMVとLTSAによる時相論理式の実験
- 組み込みプログラミング・ノウハウ入門(第32回)LTSAをタスクのテストに使う--タスク動作モデルの作成(3)
- モデル検査への事前条件・事後条件検証の導入(検証・検査手法)
- 新・組み込みソフトへの数理的アプローチ(第15回・最終回)総まとめ--推論,ステート・マシンと検証
- 動作要求のモデル化と管理(モデルベース開発)
- 複数シーケンス図を使ったシナリオ検証とタスク設計(モデル表記・モデル検査)
- 新・組み込みソフトへの数理的アプローチ--形式仕様記述をどのように使うか(第13回)検証しながらプログラムを作るPDD--事前条件と事後条件による仕様記述
- 新・組み込みソフトへの数理的アプローチ(第10回)要求のトレーサビリティとモデリング--仕様書の書き方とCBMC
- 新・組み込みソフトへの数理的アプローチ(第9回)Alloyによるモデリング--クラスやインスタンスの概念をモデル化して検証する
- 新・組み込みソフトへの数理的アプローチ(第8回)組み合わせ問題で写像に親しむ--仕様記述で写像を使いこなす準備
- 新・組み込みソフトへの数理的アプローチ(第6回)原因結果グラフ--原因と結果の関係を木構造で表現する
- 新・組み込みソフトへの数理的アプローチ(第5回)AND-OR木の形式化--機能の取捨選択をグラフで表現する
- 新・組み込みソフトへの数理的アプローチ(第4回)充足問題(4)真理表から場合分け表へ
- 新・組み込みソフトへの数理的アプローチ(第3回)充足問題--真理表を使いこなす(3)
- 新・組み込みソフトへの数理的アプローチ(第2回)推論の正しさの検証--真理表を使いこなす(2)
- 新・組み込みソフトへの数理的アプローチ(新連載・第1回)仕様の形式化のはじめの一歩--真理表を使いこなす
- 組み込みソフトへの数理的アプローチ(第9回)オーバラップ制御用ステート・マシンの設計と検証--処理の多重化を検証する
- 組み込みソフトへの数理的アプローチ(第8回)時相論理式を見る--LTSAで時相論理式をステート・マシンに変換する
- LTSAとSPINを連携させたタスク設計の提案(組込みシステムプラットフォーム)
- LTSAとSPINを連携させたタスク設計の提案(組込みシステムプラットフォーム)
- LTSAとSPINを連携させたタスク設計の提案 (計算機アーキテクチャ 組込みシステム)
- アセンブラのモデル検査におけるモデルの自動生成について(検証・検査手法)
- 組み込みソフトへの数理的アプローチ(第4回)論理式の実験場を作る,全数チェックへの道--数理的アプローチの基礎トレーニング(2)
- 組み込みソフトへの数理的アプローチ(第2回)プログラムの証明--ホーア論理とダイクストラのプログラム検証法
- 第4章 μITRON準拠OS NORTi4/H8/36014を使った 市販のOSソースで理解するディスパッチャ(1) (特集 ハードウェアの基礎からRTOSのしくみまで 組み込みOSを使ったプログラミングの基礎)
- 組み込みソフトへの数理的アプローチ(第6回)時相論理の導入--CTLとLTL--NuSMVでステート・マシンと実行系列を検査する
- 組み込みソフトへの数理的アプローチ(第5回)様相論理で変化を扱う--様相とは何か,冥王星って今どうなの
- リアルタイム・システム開発者に必須の時間制約検証作業に使える モデル検査ツールで時間仕様を検証する
- デッドラインに間に合うシステムを作成するための手法 NuSMVでタイミング解析&スケジユーリング
- 第6章 複数のタスクが連携するための同期・通信機構--タスク間インターフェース (特集 ハードウェアの基礎からRTOSのしくみまで 組み込みOSを使ったプログラミングの基礎)
- 組み込みソフトへの数理的アプローチ(第3回)論理式のテスト--数理的アプローチの基礎トレーニング
- 組み込みプログラミング・ノウハウ入門(23)Use Case現場検証:ユース・ケースは何故ばらつくのか--システム設計とプロダクト・ライン
- 組み込みプログラミング・ノウハウ入門(第31回)タスクの動きをモデル化する--タスク動作モデルの作成(2)
- 組み込みプログラミング・ノウハウ入門(第30回)RTOSを使った場合の動作モデル--タスク動作モデルの作成(1)
- 第5章 OSなしの世界とOSありの世界の違い RTOSにおけるタスクのしくみ (特集 ハードウェアの基礎からRTOSのしくみまで 組み込みOSを使ったプログラミングの基礎)
- 第3章 OSなしで実現する 割り込みを使ったプログラミング (特集 ハードウェアの基礎からRTOSのしくみまで 組み込みOSを使ったプログラミングの基礎)
- 第2章 ハードウェアがわかれば組み込みソフトウェアもわかる! プログラマのためのハードウェアの読み方の基礎 (特集 ハードウェアの基礎からRTOSのしくみまで 組み込みOSを使ったプログラミングの基礎)
- 第1章 時間スケール,ハードとソフトの切り分け,協調モデル 組み込みソフトウェアの特徴 (特集 ハードウェアの基礎からRTOSのしくみまで 組み込みOSを使ったプログラミングの基礎)
- 組み込みソフトへの数理的アプローチ(第1回)時間仕様のあつかい--ガス・バーナー問題の例
- 組み込みプログラミング・ノウハウ入門(第35回)何に対して何を検査するのかが重要--LTSAのまとめと最新のLTSA
- 組み込みプログラミング・ノウハウ入門(第34回)動作モデルからのテスト・ケース生成(2)Prologを用いてステート・マシンを検証する
- 組み込みプログラミング・ノウハウ入門(第33回)動作要求の開発--テスト・ケースをモデル・ベースで作成する
- 組み込みプログラミング・ノウハウ入門(第29回)状態の分析からモデル化,実装まで--デバイス系の設計の実例
- 組み込みプログラミング・ノウハウ入門(第27回)自走式ロボットの動作モデルを検証する--LTSAを用いた事例研究
- 組み込みプログラミング・ノウハウ入門(第26回)評価ボードを使った動作モデルの事例--要求レベルと設計レベルでLTSAを使う
- 組み込みプログラミング・ノウハウ入門(第25回)プロセス代数を使った動作モデルの検証--LTSAモデルの作り方と要求レベルでの使い方
- 組み込みプログラミング・ノウハウ入門(第24回)LTSAによる動作モデルの検証--他人のモデルのバグ探しから始めよう