形式的仕様記述の産業界での応用例として
パリの地下鉄がよくあげられるけど
これってかなり昔の話だよね．
最近の例はないの？