この間、Let's Encryptがバグで300万近くの証明書を失効させたというニュース流れました。 事の詳しい顛末は以下のBlogにかかれています。かなり詳しく書かれており、どのようなコードでバグが出たのか？というところまで解説されています。 jovi0608.hatena…
TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。 そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思う…
Raftを使ってDFSを作るという仕事を数年前ぐらいから続けています。そのためか最近、形式仕様記述（特にTLA+）とかModel checkingとかTheorem provingとかが私の中でアツいです。TLA+とかAlloyとかVDM++とかSpin周りのやつです。 ソフトウェアの仕様を形式仕…
principia.connpass.com Twitter眺めてたら面白そうなセミナーがあったので申し込んだ。 私はオブジェクトストレージではないPOSIX IFな分散ファイルシステムを作るという面白い仕事をもう数年間ぐらい続けている。 その関係で最近TLA+とTLC Model Checkerを…
踏んだのでメモ Scalaにはtraitという機能があります。 traitは「それ単体で動作することはなく、他classを拡張（mixin）するか、他classから継承されることによって動作するエンティティ」と定義して良いと思います。 JavaのInterfaceにたとえられることも…
時代はﾃﾝｼﾞｰ 8年前ぐらいにQNAP社のTS-439 Pro II+を購入してから、ずっとこれで満足してました。しかし、システム領域のFlashが不穏なエラーを吐き出しはじめたのでそろそろ買い替え時かと思い立ちました。容量もそろそろいっぱいになってきましたし。。。 …
