The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic.
http://alloy.mit.edu/
謝罪 この記事の方法ではうまく動きません。 記事をまとめた後の検証フェーズに入ったタイミングでお仕事的な拘束があり見直す時間がありませんでした。 見直してみたもののうまく動かずに、再度方法を検討し、動作確認まで済んだものがこの記事になります。 はじめに SyslogのViewerを作るために紆余曲折した以下の記事を手順書の様にまとめたものです。 サーバはUbuntu24.04を利用しています。 システムの構成 SyslogをWebUIで閲覧する仕組みを作ります。 rsyslogで受け取り、alloyに渡し、lokiに溜め、grafanaで表示します。
趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう? と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。 形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジックに基づいている。その中でも厳密な仕様定義を求める方向と自動検証を求める方向とあるらしいが、Alloy はその後者に位置づけられ、軽量形式手法と呼ばれるもののひとつだということらしい。Alloy はモデリングのための言語および実行環境で、以下のホームページから入手できる。 http://all…