Lilo言語

Liloは、複雑な時間依存システムの動作を記述、検証、監視するために設計された形式仕様言語です。

Liloにより以下のことができます：

時間軸にまたがる性質を定義するための強力な時相演算子を備えつつも馴染みのある構文を使用して式を記述できます。
レコードを使用してシステムのデータをモデル化するためのデータ構造を定義できます。
システムと呼ばれる機構を使用して仕様を構造化できます。