verifyに関するmasterqのブックマーク (363)
-
masterq 2019/01/09
-
List of model checking tools - Wikipedia
This article lists model checking tools and gives an overview of the functionality of each. The following table includes model checkers that have a web site from which it can be downloaded, a declared license, a description published in archived literature, and a Wikipedia article describing it. In the below table, the following abbreviations are used: Equivalences: SB: Strong Bisimulation WB: Wea
-
-
-
NuSMVによるモデル検査入門 (1) ステートマシンを定義する - Qiita
この前書いた記事はあまりにもやっつけだったので整理してみる。 概要 この記事は、シンボリックモデルチェッカNuSMV (http://nusmv.fbk.eu/) を使って、モデル検査を行うチュートリアルである。 NuSMVのバージョンはv2.6.0とする。バージョンによって機能がobsoleteされたり変更されたりするので、古いバージョン用の資料を読むときには注意されたい。 基礎知識 知ってるならスキップしてください。 モデル検査 (Model Checking) とは 状態遷移系が論理式を満たすかどうかを検査すること。 より正確には、あるKripke構造がある時相論理式を満たすか否かを検査することである。 一般に数理論理学で、データ構造 $M$ が論理式 $\phi$ を成り立たせる場合に $M\models\phi$ と書き「$M$ は $\phi$ のモデルである」と呼ぶことから、
-
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
-
-
-
-
The TLA+ Home Page
You'll miss a lot on this web site unless you enable Javascript in your browser. This is the home page of the TLA+ web site. TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design e
-
-
-
-
-
NetBSD Blog
I have presented the state of NetBSD sanitizers during two conferences in the San Francisco Bay Area: Google Summer of Code Mentor Summit (Mountain View) and MeetBSDCa (Santa Clara, Intel Campus SC12). I've also made progress in upstreaming of our local patches to LLVM sanitizers and introducing generic NetBSD enhancements there. The Bay Area I took part (together with William Coldwell - cryo@) in
-
TLA+ 入門 – Mile Zero
TLA+は、MicrosoftやAmazonがミドルウェアの設計に利用しているステートマシンの記述言語です。実際、Azure Cosmos DBやAmazon DynamoDB, S3, EBSはTLA+を使って設計、検証を行っていると公式に発表されています。 AmazonはどのようにTLA+を利用しているか Azure Cosmos DBの設計・開発におけるTLA+の貢献 IDEのダウンロードとインストール TLA+はTLA ToolboxというIDEが用意されており、シンタックスチェックや、作成したステートマシンの検証を行うことが可能です。TLA Toolboxは下記のGitHubのリンクからダウンロードが可能で、利用するにはJava 1.8以上が必要です。 ダウンロード先 ステートマシンの記述 TLA+は、JavaやPythonなどでのプログラミングと以下の点で異なります。 数学的な
-
Amazon.com: Formal Development of a Network-Centric RTOS: Software Engineering for Reliable Embedded Systems: Verhulst, Eric, Boute, Raymond T., Faria, José Miguel Sampaio, Sputh, Bernhard H.C., Mezhuyev, Vitaliy: Books
公式Twitter
- @HatenaBookmark
リリース、障害情報などのサービスのお知らせ
- @hatebu
最新の人気エントリーの配信
キーボードショートカット一覧
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
