How does SAM work? SAM is built on one of the most robust foundation of computer science (TLA+). SAM recommends factoring application state management along three building blocks, actions, model, and state that are invoked in well defined "steps". Actions are triggered by events, their role is to translate events into proposals to mutate the model The Model is solely responsible for the decision o

形式手法概論 形式手法関連のリンク集 ディペンダブル・システムのための形式手法の実践ポータル 中島震, 形式手法入門―ロジックによるソフトウェア設計―, オーム社, 2012 赤間世紀, 形式手法教科書, I・O BOOKS, 2012 IPA, 形式手法活用ガイドならびに参考資料, 2012 ディペンダブル・システムのための形式手法の実践ポータル 吉川健, JAXAにおける形式手法に対する取組み ～ソフトウェアIV&Vにおける形式手法の活用事例～, 2012 数理論理学関連のリンク集 オンラインで入手できる数理論理学・数学基礎論のテキスト Event-B Event-Bとは以下のような形式手法である。 Event-B is a formal method for system-level modelling and analysis. Key features of Event-B ar

ソフトウェアプログラム内の中核的なコミュニケーションと状態管理が論理的に100%正しいことを証明する手段として，コンピュータチェックモデルを利用する方法がある。同じようなモデルは，100%正確なソースコードの作成にも応用できる。このような形式的手法を利用することにより，市場提供のためのコストと時間を削減し，より信頼性の高いソフトウェア製品の提供が可能になる。 Wayne Lobb氏はBits&Chips Software Engineeringカンファレンスで，正当性立証可能(provably-correct)なソフトウェアについて，ビジネス的側面から講演を行う予定だ。 InfoQは氏にインタビューして，ソフトウェアが複雑である理由，正当性立証可能なソフトウェアを開発する上で形式的手法やモデルのもたらすメリット，形式的手法を用いることによるビジネス上のアドバンテージ，セーフティクリティカル

AWSがFormal Methodsを使っているというので、見てみる。分散アルゴリズムの検証に、形式手法が有効だったという話である。調べてみると、ACMの記事になる4年も前から、発表されていたらしい。 論文によると How Amazon Web Services Uses Formal Methods | April 2015 | Communications of the ACM AWSでは、2011年からFormal Methodsを使って、重要な分散システムのアルゴリズム設計を行っている。また、外部公開I/Fを単純化して提供することで、大規模な分散システムでサービスを提供できる秘訣となっている。AWSでは、顧客のデータを保護するために、フォールトトレラントな分散アルゴリズムを使っている。また、分散アルゴリズムはたくさんあるが、それらを組み合わせるのは難しい。 TLA+は、プログラマが

せっかく Chapter 1と Chapter 2を終わって動かしてみたものの、なんだかずいぶん進めにくいなー、と思って、ふとHyperbook (前回 TLA+の本、と紹介した横にあったもの。最初HTML形式のオンライン物だと思ってて、避けてた）を読んでみたら、なにこれわかりやすい。らんぱーとさんのメモ書き状態ではなく、ちゃんと人間向けに書いてある。いままでの苦労は。。 と、いうことで、Hyperbookに乗り換えて仕切りなおすことにしました。 Chapter 1は紹介、Chapter 2は 1 bit clock (0 -> 1 -> 0 -> 1 -> ... )と、前回のHour Clockより更に単純。特に面白いところもないのでさらっと流した。 Chapter 2の「ダイ・ハード」はなかなか面白い。3L入るバケツと、5L入るバケツで4Lを作る、という話。考えられる操作は以下の４通