Deleted articles cannot be recovered. Draft of this article would be also deleted. Are you sure you want to delete this article? はじめに みなさん形式手法をご存知でしょうか？ 名前くらいは聞いたことあるけどいまいち何かわからないという方が多いのではないでしょうか。 その通りです。形式手法はアカデミアではそれなりに研究されているものの、 一般の（特にWeb系）ソフトウェア開発者が携わることはなかなかないのではないかと思います。 この記事ではソフトウェア開発に形式手法が導入されないのはなぜなのかを考察します。 この記事ではアジャイルソフトウェア開発において形式手法を導入する際のハードルについて考察します。 追記 本記事について、「形式手法は流行っていない」というのは
それはそうと、軽量な形式手法たる型システム含む形式手法は記号の世界の中での正気はちゃんと証明してくれるが、人間様が頭を捻って作られた、自然言語で書かれた仕様とやらは一体何の正気を保証してくれるんだろう
CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech Festa 2021 winter
July Tech Festa 2021 winter で使用したスライドです。 バグのない分散システムの設計は果たして可能でしょうか？ この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。 形式手法はシステ…
はじめに 皆さん、SQLチューニングしてますか？（唐突） 私は仕事柄RDBMSのSQLチューニングをすることが多いのですが、たまにチューニングの一環で SQL文の書き換え をすることがあります。 その際に問題になるのが、書き換えたSQL文が等価であるかどうかの確認が大変なことです。 SQL文を書き換えた場合には、想定通りの結果を取得できるか確認するために、テストをやり直す必要があります。 これが開発早期のフェーズならまだましなのですが、結合テスト以降だと手戻りも多くかなりコストがかかりますし、既に本番運用が始まったシステムともなると、テスト自体が困難なこともあります。 また、複雑なSQL文だと網羅的なテストケースを作成すること自体が困難であるため、完全に正しいと確信することはできません。 なので、SQL文の書き換えの正しさを証明する良い手段はないかと考えていました。 SQLチューニングとは
Exploring Java OSS with LLMs - A New Way to Approach Open-Source Code Reading
本記事は、形式検証 / 形式手法 Advent Calendar 2021 の 19 日目の記事です。 Amazon S3が形式手法を採用した論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" を読みました。 論文全体については、yohei-aさんがブログ記事で主要な部分を訳してくれています。本記事では自分なりのまとめに加えて、自分の形式手法導入の経験から思うところについても書いてみます。 論文は、Amazon S3の新しいKey ValueストレージのShardStoreの正当性を軽量形式手法で検証した話です。論文の主張をまとめると、 実装に使用した言語（Rust）と同じ言語で仕様となるリファレンスモデルを記述した。 検証したい性質によってツールを使い分けた。機能的
実践TLA+ | 翔泳社
設計だってテストしたい！ 【本書の内容】 本書は Hillel Wayne, "Practical TLA+", Apress, 2018 の邦訳版です。 複雑精緻なシステムを構築する際に、設計そのもの、仕様そのものにバグがないかをテストできたら、もう少し幸せな開発人生を送れそうな気がします。 本書は送金システムの小規模な仕様からTLA+を使ってヤバいバグを発見するところから始まります。この小さなサンプルをもとに、より良いアプリケーションの設計・テスト・構築に、どのようにTLA+を使えばよいかを理解し、実際のプロジェクトに援用できるよう、TLA+の演算子、論理、関数、PlusCal、モデル、および同時実行の基礎を学びます。 設計図の整理の仕方、分散システムや最終的な整合性の指定の仕方を学んだら、アルゴリズムのパフォーマンスやデータ構造、ビジネスコードやMapReduceなど、さまざまな実用
こんにちは、チェシャ猫です。 Alloy は関係論理を用いた形式手法ツールの一種です。本記事では、2021 年 11 月にリリースされた Alloy 6 の新機能、Mutable Field を用いた検査について解説します。この機能を使用することで、時間発展するタイプのシステムをよりシンプルに記述できるようになりました。 なお、本記事は従来の v5 以前の Alloy に触ったことがある読者を想定しています。したがって Alloy のツールとしての位置付けや基本的な文法・機能については説明しません。興味のある読者には『抽象によるソフトウェア設計ーAlloy ではじめる形式手法』（以下 Jackson 本）をお勧めします。 それでは早速、Alloy 6 をダウンロードして始めましょう。 TL;DR Mutable Field が導入され、時刻に従って変化するような関係が記述可能になった それ
SWETの仕様分析サポートチーム所属のtakasek（@takasek）です。 仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています（形式手法 カテゴリーの記事一覧）。 当記事は、Kuniwak（@orga_chem）により社内開催されたAlloyガイダンスを元に再構成した記事です。よく知られたデータ構造であるStackを形式仕様記述しビジュアライズすることで、Alloyの使い方と利点を実感できます。Alloy未経験者でもステップバイステップで試せるように構成しました。是非、お手元にAlloyをインストールして読み進めてください。環境はAlloy 5.1.0を想定しています。 https://github.com/AlloyTools/org.alloytools.alloy/release
こんにちは、SWETの鈴木穂高（@hoddy3190）です。 現在SWETチームにて仕様の欠陥をなるべく早くみつける取り組みにチャレンジしています。 欠陥をみつけるタイミングが早ければ早いほど、開発中の手戻りに伴うコストを抑えられます。 たとえば、仕様作成フェーズ、実装フェーズ、QAフェーズの順で開発が進んでいくときに、仕様の欠陥が実装フェーズやQAフェーズでみつかると実装やQAのやり直しを引き起こしかねません。 そうした大きな手戻りを抑えるために仕様の欠陥をなるべく仕様作成フェーズでみつけることを目指します。 対象領域に出てくる要素をモデリングすることは、仕様に潜む欠陥を開発の早い段階でみつけるための、有効な手段のひとつです。 要素には、開発者がこれから作るシステムや、そのシステムのユーザー、そのシステムと直接的または間接的に相互作用する外部のシステムが含まれます。 単に図を書くというモ
序 この記事、ちょっと、というかかなり感覚が古くね？ qiita.com と思っていたら、炎上目的だったようで。 autotaker on Twitter: "「形式手法はなぜ流行っていないのか？」という記事を書いて炎上させたい" autotaker on Twitter: "形式手法をこき下ろすと見せかけて最終的に出身研究室のステマに成功した" 一連の言い訳も見苦しい。 autotaker (@autotaker1984) | Twitter 故意に不正確な情報をばら撒く形でしか自分の"小さな得意分野"をアピールできないとは、エンジニアとして不誠実極まりないし、ミジメだ。 本題 ということで。 形式手法は80年代から本格的に開発が始まっているが、最初に大規模に報道されたのは90年代のIntelの不動小数点ユニットのバグ対策に形式手法が導入された件だろう。 つまりチップレベルでの導入。それ
July Tech Festa 2021 winter で CockroachDB と TLA+ について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 インフラ技術のカンファレンス July Tech Festa 2021 winter で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 www.youtube.com 今回の登壇は、昨年の CloudNative Days Tokyo 2020 と同じ題材を扱っています。ただ、前回より持ち時間が長くなった分、前回のスライドで説明不足だった部分を拡充してあります。特に、CockroachDB 以外の TLA+ 採用事例や、分散システムにおける Chaos Engineering の位置付けについて解説を追加しました。 なお、前回の登壇報告は以下の記事をご参照ください。 ccvanishing.hateblo.jp 当日出た質問 実時間を含む性質 今回の時相論理では「いつか成り立つ」と
Go を書きながら定理を書く安心開発スタイル【DeNA TechCon 2021】/techcon2021-13
Go では slice の capacity を宣言できますが、この指定に悩む時があります。例えば直感では入力の slice より短いはず、と思っても本当にそうなのか不安な時があるでしょう。 このとき、定理証明支援系 Isabelle を開発で併用していると自分の仮説を証明しながら安心して開発できます…
こんにちは、チェシャ猫です。先日行われた第 7 回 Web System Architecture 研究会で形式手法について発表してきました。 普段、形式手法について登壇する際は具体例な検証例を出すことが多いですが、今回は理論側に寄せたサーベイになっています。 はじめに 本セッションでは、安全性-活性分解 (safety-liveness decomposition) と呼ばれる一連の結果について解説する。安全性-活性分解は、システムの仕様が与えられた時、それを安全性 (safety) および活性 (liveness) と呼ばれる、よりシンプルな特徴付けを持つクラスに分解して扱うための方法論である。さらにセッションの後半では、安全性と活性の組み合わせ以外にも提案されている派生的な特徴付けについても述べる。 Web アプリケーションと形式手法 システムやプログラムの性質を何らかの数学的な対象
CloudNative Days Tokyo 2020 で CockroachDB と TLA+ について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 講演概要 CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。 強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。 このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、
こんにちは、チェシャ猫です。 先日開催された AWS Dev Day Online Japan 2021 で、AWS の VPC Reachability Analyzer とそのバックエンドである Tiros について発表してきました。公募 CFP 枠です。 www.youtube.com 講演概要 このプレゼンの大きな目標は、VPC Reachability Analyzer のバックエンドである検査エンジン Tiros の論文 [Bac19] を解説することです。そのための道筋として、Section 1 で VPC Reachability Analyzer の機能を簡単に紹介した後、Section 2 でその要素技術である SMT ソルバの仕組みを解説し、最後に Section 3 として VPC ネットワークの意味論を SMT ソルバ用にエンコーディングする方針について解説します
GitHub - subsetpark/pantagruel: A program specification language with a formal syntax and ad-hoc semantics.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
#技術書典 16 で Go を使って #自作モデル検査器 をつくる本を頒布します - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 今回、技術書典 16 にて、新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』を頒布します。 techbookfest.org どんな本？ ただツールを使うだけの形式手法から、君の手でつくる形式手法へ。Go 言語でモデル検査器を実装しながら学ぼう！ 書名の通り、Go でモデル検査器を実装する本です。Pramo 言語と名づけた本書オリジナルのモデリング言語を定義し、その可視化器と検査器を作成します。 Pramo 言語は、ある種のマルチスレッドをサポートするプログラミング言語であり、Go の埋め込み DSL として記述されます。例えば有名な「食事する哲学者」は以下のように実装されます。 func badPhilosopher(name procName, right, left lockName, hold varName) process { retur
This article began life as a talk I gave in late 2024. I love formal methods—I should say that to begin with, because this article is mostly about what doesn’t work when trying to do FM projects. Over the last 20 years, formal methods have grown and grown, and I’m proud to say that Galois has made its own contributions to this success. I made a lot of mistakes when I was scoping and running formal
July Tech Festa 2021 で IAM Access Analyzer と Zelkova について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 先日開催された July Tech Festa 2021 で、AWS のアクセス制御検査ツール Zelkova について発表してきました。公募 CFP 枠です。 techfesta.connpass.com 講演概要 www.youtube.com 一般に、AWS 上のリソース設定を変更したときに何が起こるのかを事前に検査するのは難しい作業です。特に、複数の設定がマージされた結果として最終的なアクセス許可が決まるような場合、単独の項目をルールベースでチェックするだけでは限界があります。 今回の発表中では、インフラに対する検査の水準を以下の 3 つのレベルに分けて定式化しました。 Level 1：構文論的な検査。テンプレートが文法的に正しいかどうかを確かめる Level 2：ヒューリスティックな検査。意図した性質が成り立つかどうかを、特定の設定項目に関する条件と
会社のイベントで1週間何しててもいい期間があったので、大学時代に研究していた形式手法の1分野であるLTL仕様からオートマトン合成の分野に触れていました。 タイムライン 以前使っていたAcacia+というツールがリンク切れになっていたことに驚く LTLからオートマトン合成のコンペティションが2014年から開催されており使いやすく高性能なLTL合成ツールの発展に貢献していた TLSFという生のLTLをラップした仕様形式がベンチマークの共通形式として普及していた。入出力のシグナルとオプションがLTLとセットで管理できる。 Strixというツールが2019年のコンペで1位になっていたのでOnlineでもページで遊んでみる Strixが良さそうなのでDockerfile作ってインストールして触ってみる Strixの内部でowlというLTLパースとωオートマトン変換をやるJavaライブラリ使っていて、
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
形式手法はなぜ流行っていないのか - Qiita
「せっかく記号を使った形式手法があるのに自然言語に戻るのか」というツイート - tkgshn
SQL等価性検証ツールCosetteを使ってみた - Qiita
AIと共に進化する開発手法： 形式手法と関数型プログラミングの可能性
Amazon S3の軽量形式手法 - masateruk’s blog
Alloy 6 の新機能 Mutable Field と線形時相論理
形式手法でデータ構造を記述・検査してみよう：Alloy編 - DeNA Testing Blog
時間を加味したモデリング - DeNA Testing Blog
「形式手法はなぜ流行っていないのか」に対する異論 - interdb’s blog
安全性-活性分解定理とその関連研究 - チェシャ猫の消滅定理
https://dl.acm.org/doi/10.1145/3477132.3483540
VPC Reachability Analyzer と形式手法 - チェシャ猫の消滅定理
What Works (and Doesn't) Selling Formal Methods
- YouTube
10日間大学時代の気分に戻ってLTLで仕様を書いてみた - cloverrose's blog