本記事は、形式検証 / 形式手法 Advent Calendar 2021 の 19 日目の記事です。 Amazon S3が形式手法を採用した論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" を読みました。 論文全体については、yohei-aさん…

AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメ…

これはFormal Method Advent Calendar 2016の25日目の記事です。今年6月、国立情報学研究所で「恊働ロボットCOROの開発における形式的仕様の適用事例」というタイトルで形式手法の適用事例について発表しました。資料はこちらです。http://www.slideshare.ne…

さて、ようやく最終回です。前回は、仕様と実装を比較して、実装が仕様を満たすことを確認したものの、実は発散が含まれているという話でした。今回はこの発散を取り除いて改めて仕様との比較を行います。まずもう一度発散を確認しましょう。発散検査を行い…

前回までは通信路に歪みがないことを仮定してましたが、今回から通信路に歪みを考慮に入れます。つまり、送信した値と異なる値が相手に届くことがあると状況をつくります。 チャネルのモデリング これまではSyncStitchのチャネルをそのまま使用していました…

前回は通信路に歪みがないと仮定して、その上で 0, 1 をやり取りする送信者と受信者をモデル化してデッドロック検査を行いました。今回は仕様を状態遷移図で表し、その仕様との比較を試してみます。さて、その仕様ですが、今回のABPの設計で確認したい事は「…

以前いっしょに仕事していた先輩がSyncStitchという設計ツールを開発したので試用してみました。SyncStitchの特徴は、状態遷移図で書いたモデルの振る舞いをシミュレーションしたり検証できたりします。さらに複数の状態遷移図を組み合わせときの振る舞いに…

私は形式手法にはソフトウェアの品質を高める力があると信じている。一方、プロジェクトの進め方に関して言えばアジャイルのようなやり方が有効だと思っている。しかし、私が形式手法とアジャイルの両方に興味を持つ事に関して、そういう人は珍しいと言う意…

前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。１冊目。VDM++によるオブジェクト指向システムの高品質設計と検証…

後輩に形式手法を学び始めたときに読んだ本を紹介すると約束したので、せっかくなのでブログに書くことにした。 形式手法を学び始めたのは2004年だから、今から始める場合はまた違ったラインナップになるだろうけど。 ※「2012年に形式手法を学び始めるならこ…

とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。 問題 あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフ…