分散合意アルゴリズム Raft を TLA+ で検証する - 俺の Colimit を越えてゆけ
はじめに 分散合意アルゴリズム Raft とは 分散合意アルゴリズムとは Raft の特徴 Raft が満たす性質 Election Safety Leader Append-Only Log Matching Leader Completeness State Machine Safety TLA+ とは TLA+ による Raft の形式的仕様 TLA+ による Raft の検証方法 TLA+ Toolbox のインストール 新規 Spec の作成 Model の作成と実行 補足: コマンドラインでの検証 Raft の拡張について Leadership Transfer Membership Change Log Compaction Client Interaction おわりに Raft 理解度を調べるクイズ 参考資料 Raft に関する資料 TLA+ に関する資料 はじめに この
PlusCal: 証明アプローチ - MOXBOX #PlusCal #TLA+
\( \def\ldef{≜} \) \( \def\globally{□} \) \( \def\eventually{◇} \) \( \def\openleftarrowplus{\overset{+}{⇾}} \) \( \def\equalv{⫤} \) 概要 このページでは PlusCal を使って記述したシステムが正しいことをどのように証明するかについて説明する。サンプルを実行するための環境セットアップは環境設定と検証の実行を参照。 Table of Contents 概要 TLA+ は何を証明するのか? Safety 特性 Liveness 特性 スタッターリング 公平性特性 終了の検査 例: 信号機と歩行者 歩行者用信号の故障 歩行者の青信号見逃し 歩行者用と自動車用の信号を青にする TLA+ は何を証明するのか? 一般的なプログラミング言語のアサーションが「ある時点での
[TLA+] PlusCal on VSCode コトハジメ (1) - Qiita
はじめに モデルを発見・検討するのに向く Alloy と異なり、TLA+ / PlusCal は少し先のステップである処理の原理確認やマルチスレッドでの問題発見に役立つアルゴリズム言語（≠プログラミング言語）である。 どちらも有用なので、自分以外のプログラマーにとっても「コメントがあれば読めそうに見える」PlusCal を使えるようになりたい。 実際のところPlusCalを読むのも難しいが、対抗として考えられる SPIN, VDM, Event-B といったモノ達よりは読めそうな雰囲気を持つ。 また、MITライセンスであることや、Amazon, Microsoft, DropBox といった採用実績から、習得するならこれがよいだろうと考える。 環境設定 さて、VSCode で PlusCal を使ってみよう。 VSCode に Extention TLA+ をインストールすればとりあえずO
![[TLA+] PlusCal on VSCode コトハジメ (1) - Qiita](https://cdn-ak-scissors.b.st-hatena.com/image/square/8fd6f54174ec0364a318e215cfdc8ebacb3d2c16/height=288;version=1;width=512/https%3A%2F%2Fqiita-user-contents.imgix.net%2Fhttps%253A%252F%252Fcdn.qiita.com%252Fassets%252Fpublic%252Farticle-ogp-background-412672c5f0600ab9a64263b751f1bc81.png%3Fixlib%3Drb-4.0.0%26w%3D1200%26mark64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTk3MiZoPTM3OCZ0eHQ9JTVCVExBJTJCJTVEJTIwUGx1c0NhbCUyMG9uJTIwVlNDb2RlJTIwJUUzJTgyJUIzJUUzJTgzJTg4JUUzJTgzJThGJUUzJTgyJUI4JUUzJTgzJUExJTIwJTI4MSUyOSZ0eHQtY29sb3I9JTIzMjEyMTIxJnR4dC1mb250PUhpcmFnaW5vJTIwU2FucyUyMFc2JnR4dC1zaXplPTU2JnR4dC1hbGlnbj1sZWZ0JTJDdG9wJnM9ODg1ODUwYzM5ZTY4MjczMzM3NDFkZGZiNzk4MmUyZTE%26mark-x%3D142%26mark-y%3D57%26blend64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZoPTc2Jnc9NzcwJnR4dD0lNDBqcHdnYWQmdHh0LWNvbG9yPSUyMzIxMjEyMSZ0eHQtZm9udD1IaXJhZ2lubyUyMFNhbnMlMjBXNiZ0eHQtc2l6ZT0zNiZ0eHQtYWxpZ249bGVmdCUyQ3RvcCZzPTM4Yjk4MTAyMDQ3NzFlMzJmMTM5OTNmZmM5NDNmYTc0%26blend-x%3D142%26blend-y%3D486%26blend-mode%3Dnormal%26s%3Dcdb1abc4d2505090d91124f072508880)
Using TLA+ in the Real World to Understand a Glibc Bug
Using TLA+ in the Real World to Understand a Glibc Bug by Malte Skarupke TLA+ is a formal specification language that you can use to verify programs. It’s different from other formal verification systems in that it’s very pragmatic. Instead of writing proofs, it works using the simple method of running all possible executions of a program. You can write assertions and if they’re not true for any p
Introduction to TLA+ Model Checking in the Command Line
I started playing around with TLA+ and its more programmer friendly variant PlusCal about a year ago. At that time the amount of documentation that was understandable to people like me who do not enjoy reading white papers full of mathematical notation was slim to none. (Today you can buy Hillel Wayne’s excellent book Practical TLA+) So I started reading other people’s code (errr…specs) and began
kernel/git/cmarinas/kernel-tla.git - Kernel TLA+ specs
index : kernel/git/cmarinas/kernel-tla.git Kernel TLA+ specsCatalin Marinas aboutsummaryrefslogtreecommitdiffstats BranchCommit messageAuthorAge masterasidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskCatalin Marinas4 years AgeCommit messageAuthorFilesLines 2021-09-10asidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskHEADmasterCatalin Marinas1-17/+19 2021-08-05asid
AWSにおける形式手法 - masateruk’s blog
AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる 以下は、読んでいる途中で書きだした要点。 AWSでは2011年以降形式仕様とモデル検査を使用している 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレス
TLA+ Video Course
The TLA+ Video Course Last modified 23 October 2021 This is a series of video lectures to teach programmers and software engineers how to write their own TLA+ specifications. It assumes a basic understanding of programming concepts. Some knowledge of elementary mathematics, such as might be taught in a beginning university math course for computer scientists, would also be helpful. A Word of War
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Learn TLA+ — Learn TLA+
Security
GitHub - awakesecurity/spectacle: Embedded specification language & model checker in Haskell
What are the differences between Alloy and TLA+? - Quora
Programming Language - MOXBOX
GitHub - ratish-punnoose/tla-mode: tla-mode for emacs
Summary of TLA+
TLA+ as an Isabelle object logic
<no title> — Learn TLA+
https://lamport.azurewebsites.net/video/video5.html
TLA+
https://lamport.azurewebsites.net/video/intro.html