社会人エンジニア向けの教育プログラム「トップエスイー」から、エンジニアの皆さんに対して有用な情報をお届けするコーナーです。ところで、形式手法という言葉はご存じでしょうか？ 一般には「数理論理学に基づき、効率よく高品質なソフトウェアを開発するための手法の総称」などといわれます。とはいえ「数理論理学」といわれてもなかなか実感ができないと思います。さらに「総称」と述べましたが、セミナーや書籍などで勉強した方も、その中の一つの手法や観点のみに触れたのではないかと思います。本記事ではAmazon Web ServiceやFacebook等の具体的な事例にも触れ、形式手法と呼ばれるアプローチのいくつかの方向性・可能性について紹介します。「形式手法」という広すぎる言葉はいったん忘れて、難しい専門用語に振り回されないよう、できるだけ一般的な言葉での説明を補足します。 「網羅的テストが可能な擬似コード」を用
岡野 浩三（信州大学 准教授、IPA/SEC システム安全性・信頼性分析手法WG委員）、岡本 圭史（仙台高等専門学校准教授、IPA/SEC システム安全性・信頼性分析手法WG委員） 近年、これまで個別に動作していたシステムがさまざまなレベルのネットワークを通じて相互に結ばれて協調動作するようになっている。このように複雑化したシステムに対する安全分析や障害原因診断では、推定要因とその箇所を絞り込んだ後に、絞り込んだ推定要因が本当の要因であることを検証することになる。また、システムの複雑化への対応策として、モデルベースでこうした分析・診断を行うようになってきている。 例えば、システムのコンポーネント間の相互作用に着目した安全分析手法である「STAMP（System Theoretic Accident Model and Processes）/STPA（System Theoretic Pro
エスクモーションの藤倉俊幸氏（コンサルティング本部 シニアコンサルタント）は、ソフトウエアの変更要求仕様書を基にして仕様内の矛盾や不整合などをモデル検査によって検出するアプローチを、2011年6月17日に開催された「XDDP（eXtreme Derivative Development Process）」のイベント「派生開発カンファレンス2011」において提案した。変更要求仕様書に加えてユース・ケース記述を用意し、これらをLTSAやNuSMVなどのモデル検査器で形式検証するという流れである。車載分野のワイパー制御システムの仕様書に今回のアプローチを適用し、仕様上の未定義を発見することに成功した。
形式的手法の発祥の地，欧州では 「同手法についてよくある誤解」とのテーマが学会などで語られる。 一方，日本ではその存在すらほとんど認知されておらず よくある誤解などが発生する以前の状態だ。 こうした中，国内でも先駆的に形式的手法を活用し成果を上げた企業がある。 研究者の興味の対象でしかなかった形式的手法が，いよいよ日本でも現場に広がり始めた。 仕様記述と形式検証（モデル検査）。 形式的手法を構成するぞれぞれの分野での最新事例を紹介する。 形式的手法は，主に2つに大別される。1つは，ソフトウエアの仕様を「形式的な仕様記述言語」を使って論理的に記述したり，検査したりすることで，少しでも早い段階でバグを洗い出す「仕様記述」。もう1つは，形式的な仕様記述言語とは別の専用言語で記述したシステムの状態遷移をコンピュータに入力することで，振る舞いにバグがないかどうかを高速かつ自動的に探索する「形式検証（
モデル検査やAUTOSARなどに関連したツールが登場 ―― 第11回 組込みシステム開発技術展（ESEC）レポート（2） 組み込みネット編集部 2008年5月14日～16日，東京ビッグサイト（東京都江東区）にて，組み込みシステムに関する展示会「第11回 組込みシステム開発技術展（ESEC）」が開催された（写真1）．モデル検査やAUTOSARなどに関連した開発ツールが注目を集めていた． [写真1] 受付の様子 東京ビッグサイト（東京都江東区）にて開催された． ●モデル検査をシーケンス図や状態図に適用 イーソルは，UMLのシーケンス図や状態図に対して，容易にモデル検査を適用できる検証環境を展示した（写真2）．この検証環境は，UMLモデリング・ツール「Enterprise Architect」からモデル検査ツール「LTSA」用のファイルを出力するものである．モデル検査とは，形式手法（Formal
組み込みソフトウエア向けコンサルティングを手掛けるエクスモーションは，C言語向けのモデル検査ツール「CBMC」を用いて，C言語プログラム中の関数について事前条件・事後条件を検証する実演を見せた。関数の仕様を設計者が事前・事後条件として明示的に与えることで，関数の実装が仕様通りであることを確かめたり，関数の呼び出し関係を検証したりする。
NuSMV 2.4.3 is OUT! Version 2.4.3 is a minor release that provides several bug fixes and commands completion when interactive shell is used. Follow this link to retrieve a copy. Read the announce for NuSMV 2.4.3. Read the announce for NuSMV 2.4.2. Read the announce for NuSMV 2.4.1. Read the announce for NuSMV 2.4.0. Read the announce for NuSMV 2.3.1. Read the announce for NuSMV 2.3.0. Read
1.はじめに 私は主に組み込み分野における開発に携わってきました。近年、組み込み分野では、品質に対する要求はどんどん厳しくなっています。現在、品質向上のための様々なアプローチが行われています。今回は、人間にわかりやすいモデルを、抜け漏れなく検証するという観点で、UMLとモデル検証の組み合わせの可能性を探ってみました。 本記事では、UMLの状態マシン図で記載したモデルに、モデル検証ツールspinを適用していきます。 spinとは、ベル研究所で開発されたオープンソースのモデル検証ツールです。検証対象のモデルの取りうる全ての状態において、検証条件を満たしているか確認することができます。また、複数のタスクで動作するシステムにおけるデッドロックの発生なども検出することができます。デッドロックの検出例は、書籍やWebサイトでも多く紹介されています。 組み込みシステムにおいては、現在でもRTOS（リアル
晴天の価値 2月中旬に出張で千葉へ行った。5日間の滞在中はずっと快晴で、気温は20℃に迫る春のような暖かさだった。仕事は朝から晩まで現場を走り回る過酷なもので、身体的にも精神的にも追い込まれた。毎朝、京葉線から見える美しい景色を眺めて正気を保っていた。太平洋へ燦々と…
フォーマルメソッド（形式手法）をご存じだろうか。これは，ほとんどの場合日本語で記述される「要求仕様」を，プログラミング言語によるコーディングと同じように，厳密に「仕様記述言語」で定義する手法のことである。 要求仕様を仕様記述言語で厳密に定義（モデリング）することで，要求仕様のあいまいさがなくなるほか，ライブラリを作成しておけば「要求仕様の再利用」も可能になる。構文チェックや型チェック，インタプリタによる動的テストにより，要求仕様の正しさもツールで検証できる。結果的に，要求定義フェーズの欠陥を大幅に減らせる。 言うまでもないが，システム全体の品質を高めるためには，要求定義などの上流工程の欠陥をどれだけ減らすかが大きなカギとなる。そういう意味で，「フォーマルメソッド」は高品質なシステムを作るための重要な武器になり得ると，記者は思っている。 ただし，「仕様記述言語を学ぶのが難しい」という理由で，
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Amazon.co.jp: ＳＰＩＮ モデル検査: 検証モデリング技法: 中島震: 本
