モデル検査のユースケース
著者：早水公二 (株式会社フォーマルテック)、高井利憲 (チェンジビジョン) みなさん、こんにちは。 2017年7月31日の記事では、ステートマシン図の設計品質の向上のための方法として、モデル検査を紹介しました。今回は、ソフトウェア開発におけるモデル検査の利用例をいくつか紹介します。 前回の記事では、モデル検査の概要とステートマシン図にモデル検査を適用して設計ミスを発見した事例を紹介しました。紹介した事例では、モデル検査のメリットである、 (1) 網羅的な検査ができること がいかされました。モデル検査のメリットには他にも次のようなものもあります。 (2) モデルと検査式を作成した後の繰り返し試験が容易であること (3) モデルと反例を共有することで不具合情報を共有できること 今回は、上の(1)(2)(3)のメリットをそれぞれ有効に活用したモデル検査のユースケースをご紹介します。 1.
アジャイルと形式手法
8. 仕様を書く 自分たちの手法 ー ユーザーストーリーの実現の仕方 8 自分たちの手法 テストケース をつくる ソースコード レビュー 不具合を 修正する テストを 実施する ユーザー ストーリー 仕様書 （形式的記述） 設計して 実装する プログラム テストケース 開発チーム QAチーム 9. 自分たちの手法 ー 仕様の書き方 9 自分たちの手法 仕様は状態遷移モデルで記述する。遷移の構成要素は、 – 遷移元の状態、イベント（パラメータを含む）、ガード条件、事後条件、遷移先の状態 状態は変数をもつことができる。ガード条件、事後条件の記述を論理式と自然言語で書く。 論理式は、独自の仕様記述言語KMLで書く 独自の言語を作った理由 – 気に入ったものがなかった。VDMも候補だったが、補助関数については関数型プログラ ムのように書けるものがほしかった。 10. KMLの記述例 1
NGK2015B で AWS + Alloy について話してきました - チェシャ猫の消滅定理
先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。 AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 from y_taka_23 www.slideshare.net 当日の動画は [3] NGK2015B（名古屋合同懇親会 2015 忘年会） - YouTube から見ることができます。 TL;DR AWS でインフラ運用中 でも設定が大人の都合でカオスになりがちだったりして辛い よろしい、ならば形式手法だ サンプルコードを動かしてみよう！ まずはインストールしてみる 公式ページ Alloy - download から、jar ファイルで提供されているものをダウンロードしましょう。 java -jar alloy4.2.jar でウィンドウが起動すれば OK です。 なお、dmg 版も提供
How Amazon Web Services Uses Formal Methods – Communications of the ACM
Since 2011, engineers at Amazon Web Services (AWS) have used formal specification and model checking to help solve difficult design problems in critical systems. Here, we describe our motivation and experience, what has worked well in our problem domain, and what has not. When discussing personal experience we refer to the authors by their initials. At AWS we strive to build services that are simp
Blogs/20141224-IntroductionToKeYProver/README.md at master · ikedaisuke/Blogs
KeY-project とはプログラム、 特に Java (の subset) プログラムに対する形式手法のためのツール群です。 The KeY Book (2007) によれば、 以下の大学の共同プロジェクトです： University of Karlsruhe Chalmers University of Technology in Göteborg University of Koblenz-Landau 執筆時では以下のツールが開発されているようです： KeY Prover (for Java Card) KeY-Hoare KeYmaera KeY for C ASMKey 本稿では Key Prover の簡単な紹介を行います。 その他のツールについては、筆者の能力の限界＆アドベントカレンダーの締切のせいもあり、 紹介することができません。 また、KeY Prover の Ec
2012年に形式手法を学び始めるならこの7冊 - masateruk’s blog
前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。 １冊目。 VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive) 作者: ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカージー、ニコ・プラット、マーセル・バーホフ,酒匂寛出版社/メーカー: 翔泳社発売日: 2010/08/03メディア: 大型本購入: 1人 クリック: 32回この商品を含むブログ (8件) を見るVDM++の本。形式手法を学び始めるならこの本から始めると取っ付きやすいのではないかと思う。高級言語をつかった陽関数定義（実行可能形式）でモデルをがんがん書いて、シミュレーションとテストでモデルを洗練していくや
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ソニーの画像処理IC設計手法が進展、SystemCに形式検証
Event-B | 近代科学社