こんにちは、チェシャ猫です。 今回、技術書典 16 にて、新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』を頒布します。 techbookfest.org どんな本？ ただツールを使うだけの形式手法から、君の手でつくる形式手法へ。Go 言語でモデル検査器を実装しながら学ぼう！ 書名の通り、Go でモデル検査器を実装する本です。Pramo 言語と名づけた本書オリジナルのモデリング言語を定義し、その可視化器と検査器を作成します。 Pramo 言語は、ある種のマルチスレッドをサポートするプログラミング言語であり、Go の埋め込み DSL として記述されます。例えば有名な「食事する哲学者」は以下のように実装されます。 func badPhilosopher(name procName, right, left lockName, hold varName) process { retur
こんにちは、チェシャ猫です。 先日開催された 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 ソルバ用にエンコーディングする方針について解説します
こんにちは、チェシャ猫です。 先日開催された July Tech Festa 2021 で、AWS のアクセス制御検査ツール Zelkova について発表してきました。公募 CFP 枠です。 techfesta.connpass.com 講演概要 www.youtube.com 一般に、AWS 上のリソース設定を変更したときに何が起こるのかを事前に検査するのは難しい作業です。特に、複数の設定がマージされた結果として最終的なアクセス許可が決まるような場合、単独の項目をルールベースでチェックするだけでは限界があります。 今回の発表中では、インフラに対する検査の水準を以下の 3 つのレベルに分けて定式化しました。 Level 1：構文論的な検査。テンプレートが文法的に正しいかどうかを確かめる Level 2：ヒューリスティックな検査。意図した性質が成り立つかどうかを、特定の設定項目に関する条件と
SWETの仕様分析サポートチーム所属のtakasek（@takasek）です。 仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています（形式手法 カテゴリーの記事一覧）。 当記事は、Kuniwak（@orga_chem）により社内開催されたAlloyガイダンスを元に再構成した記事です。よく知られたデータ構造であるStackを形式仕様記述しビジュアライズすることで、Alloyの使い方と利点を実感できます。Alloy未経験者でもステップバイステップで試せるように構成しました。是非、お手元にAlloyをインストールして読み進めてください。環境はAlloy 5.1.0を想定しています。 https://github.com/AlloyTools/org.alloytools.alloy/release
こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 講演概要 CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。 強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。 このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、
Abstract 本セッションでは、形式手法 (formal methods) を用いた分散システムの設計および実装について解説します。形式手法は、数学的な表現を用いて対象となるシステムを定式化することにより、システムの挙動の「正しさ」を厳密に保証するための方法論です。受講対象は予備知識を持たない初心者を想定しており、具体例を通して形式手法の基本的なアイデアを知ることを目標とします。 分散システムのメリットとデメリット 近年、複数のコンポーネントが非同期的に連携して動作する分散システムは決して珍しいものではなくなりました。正しく設計された分散システムは、集中システムとは比較にならないフレキシビリティとスケーラビリティを発揮します。人気 OSS の中にも分散型の設計を取るものは多数見られ、一昔前のように一部の専門家だけに任せておくだけでなく、すべてのエンジニアにとって一種の基礎教養になってい
AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる 以下は、読んでいる途中で書きだした要点。 AWSでは2011年以降形式仕様とモデル検査を使用している 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレス
先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。 前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です。 後半のソースコード紹介が散文的な感じになってしまって、いまいちメリットが伝わらない感じだったので、次回があればもっとエモいスライドにしようと思います。 分散アルゴリズムの形式化 定理証明による検証 今回の話の流れとして「分散システムにはモデル検査が有効」と述べていますが、必ずしも定理証明が分散システムの検証に向かないという趣旨ではありません。 例えば、定理証明器 Coq によって分散システムを証明するためのフレームワークとして Verdi が開発されています。 github.com さらに、Coq は実行可能なコードも
July Tech Festa 2018 で使用したスライドです。二相コミットを例として、分散アルゴリズムの検証にモデル検査を使用する手法について解説しています。また、代表的なモデル検査ツールである SPIN、TLA+、P について、同じシステムを各ツールで記述してみることでその特定の違いについて学びま…
ライトウェイトな形式手法で高品質な仕様をこの手に！：誰でも使える形式手法（1）（1/3 ページ） 近年、組み込みソフトウェアは高機能・多機能化により複雑さを増し、開発規模が著しく増大しています。 こうした厳しい状況の中、ソフトウェア開発の現場では、以下のような問題に直面するケースが多く見られます。 出荷前に仕様の不具合が発見され、対応に追われた 修正をしたら思わぬ個所に不具合が発生した 外部に依頼したソフトウェアの品質がなかなか上がらない ソースコードしかなく、仕様書が残っていないため、どこを修正すればよいのか分からない 仕様をレビューすることの限界を感じる では、なぜこのような問題が起こるのでしょうか？ その原因の1つは“仕様の不確かさ”にあります。読者の皆さんの中にも、『仕様（の不確かさ）が原因で痛い目を見た』という経験をお持ちの方がたくさんいらっしゃるのではないでしょうか？ そこで本
先日行われた JAWS FESTA 東海道 2016 で登壇してきました。 形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta from y_taka_23 www.slideshare.net テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 分の LT だったのに比べて今回は 25 分の枠を頂きました。そこで、形式手法を用いる動機を中心に据えた前回と比較して、以下のような実践的なトピックを充実させてあります。 Alloy を使うためにの最低限必要な言語機能を知る シンプルな Web サーバ周りのネットワークについて、仕様から設計を導出する ちなみに前回の AWS Summit 2016 での発表に関してはこちらから。 ccvanishing.hateblo.jp 寄せられた質問 発表後に頂いたいくつか
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く