モデル検査への事前条件・事後条件検証の導入(検証・検査手法)
スポンサーリンク
概要
- 論文の詳細を見る
従来の形式仕様記述のレベルはデータ制約を扱うシミュレーションまでであったが,本研究によりモデル検査技術を利用することで検証レベルを上げることができたので報告する.
- 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による動作モデルの検証--他人のモデルのバグ探しから始めよう