状態遷移のチェックだってできるぜ。 といいたいところだが、まぁ簡単に図を書くくらいならLTSAと同じだなぁ、 というところをやってみる。 /* LTSAのマネ.Thread Life Cycle THREAD = CREATED, CREATED = (start -> RUNNABLE |stop -> TERMINATED), RUNNING…

第6回Formal Methods 勉強会で出た、RBACのモデルのお話。 こんな感じかな。 /* Role Based Access Control ロールに階層関係を追加 */ /* ユーザアカウント */ sig User { roles: set Role } /* ロール。Admin,Guestなど */ sig Role { perms: set Permissi…