安全性-活性分解定理とその関連研究 - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。先日行われた第 7 回 Web System Architecture 研究会で形式手法について発表してきました。 普段、形式手法について登壇する際は具体例な検証例を出すことが多いですが、今回は理論側に寄せたサーベイになっています。 はじめに 本セッションでは、安全性-活性分解 (safety-liveness decomposition) と呼ばれる一連の結果について解説する。安全性-活性分解は、システムの仕様が与えられた時、それを安全性 (safety) および活性 (liveness) と呼ばれる、よりシンプルな特徴付けを持つクラスに分解して扱うための方法論である。さらにセッションの後半では、安全性と活性の組み合わせ以外にも提案されている派生的な特徴付けについても述べる。 Web アプリケーションと形式手法 システムやプログラムの性質を何らかの数学的な対象
「厳密な共通言語」としての形式手法 #devsumi / Developers Summit 2020
Developers Summit 2020 で使用したスライドです。 言葉というものは曖昧です。複数人が「ともにつくる」システムにおいて、メンバ間で仕様を正しく共有することは非常に重要ですが、一方で言葉の裏側に隠された「暗黙の仮定」を見抜くことは簡単ではありません。このような仕様の曖昧性への対抗手段として、本セッションでは「形式手法」を紹介します。形式手法ではシステムの挙動を数学的に記述することにより、自然言語の持つ曖昧性を排除し、仕様が満たされるかどうかを厳密に検証することが可能になります。あなたの頭の中にある仕様がどのように「数学的な記述」に変換されるのか、具体例を通して体験してみませんか？ イベント概要：https://event.shoeisha.jp/devsumi/20200213/session/2380/
形式手法による分散システムの検証 #builderscon / builderscon tokyo 2019
builderscon tokyo 2019 で使用したスライドです。 本セッションでは、形式手法 (formal methods) を用いた分散アルゴリズムの検証について解説しました。形式手法は、数学的な表現を用いて対象となるシステムを定式化することにより、システムの挙動の「正しさ」を厳密に保証するための方法論です。 なお解説として取り上げたのは、AWS による事例論文でも有名なモデル検査器 TLA+ です。講演前半で形式手法の一般論に触れたのち、後半では分散トランザクションを実現するための TCC (Try-Confirm/Cancel) Pattern のモデリングと検証を行いました。 講演概要：https://builderscon.io/tokyo/2019/session/fa356ee3-6be9-4850-ac9e-037bd34aabaa 録画：https://www.y
AWSにおける形式手法 - masateruk’s blog
AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる 以下は、読んでいる途中で書きだした要点。 AWSでは2011年以降形式仕様とモデル検査を使用している 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレス
アジャイルと形式手法
協働ロボットCOROの開発において形式的仕様記述を適用した事例について解説した資料です。 2016年6月30日（木）国立情報学研究所において開催された『第1回 ソフトウェア工学勉強会』で発表しました。
形式手法とテスト、そして、その先について
Ver. 2を公開しました: https://speakerdeck.com/nnchiba/point-cloud-deep-learning-survey-ver-2 PointNet前後～ECCV2018の点群深層学習関連の論文についてまとめました． 間違いなどあればご指摘頂けるとありがたいです．
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
分散システム、本当に「正しく」開発できますか？ #JTF2018 / July Tech Festa 2018
