最近では、地図サービスを使ったマッシュアップが全盛で、世界各地の路線図や運行状況までもがリアルタイムでウェブブラウザから見て 取れる。しかし、これはまだ完成形では無いと感じている。では何が足りないのだろう。そのヒントを一枚の路線図に著者は見いだした。

一色で塗られた地図

その地図は、フランスのClearSy 社によりB-Methodと呼ばれる開発手法を適用した国だけに色を付けた路線図だった。まずパリ市街地の一部そして、フランス国内、EU諸国、北アフリカ、北米、南米の複数の都市、そして香港の一部 に色が付けられていた。B-Methodとは形式手法(Formal methods)という技術に類されるソフトウェア開発方法論であり、 数学的な理論に基づいた仕様記述、開発、検証の手法である。

このような路線図は前例が無いように感じる。というのも、通常路線図とは多様な方式を同時に含むものと予想されるからである。事実、新 幹線の例を取って考えてみると、近年ブラジルや中国では各国から新幹線のシステムを導入しているが、その形式は、日本式、ドイ ツ式、フランス式など何通りかが存在している。従って、世界各地の陸地にいずれかの方式の新幹線の路線が、入り組んで存在しているという様 相が想像 できる。

著者にとってClearSy社による路線図は目新しいものであり、しかもたった数十人規模の 会社がこれを実現したということが驚きであった。

鉄道などの信頼性を要求されるシステムを作るにあたり、ClearSy社は形式手法を用いた点が注目に値する。

形式手法によるシステムの信頼性

一般に、システム開発には安全性のために様々な規制がかけられる傾向にある。例えばセキュリティ評価基準のCommon Criteria（CC)への準拠が要求されるシステムが増えている。CCでは、一定水準以上の高信頼性システムと認定するために形 式手法の利用を必須事項としている。現在 は軍用途の信頼性水準を確保する場合のみの必須事項だが、ClearSy社などの実績により、鉄道などの重要インフラでも形式手法の利用が同様に必須となって いくだろう。

形式手法の効果として、ClearSy社が過去に手がけた鉄道案件のソフトウェアの多くがバージョン1.0のまま、つまりバグを含んで いな いことを彼らは 誇らしげに話してい た。

今後、鉄道システムの信頼性を語る上で形式手法は重要な一側面となっていくに違いない。

定刻発車というシステムの信頼性

フランスの会社が形式手法を武器として世界進出しているルーツを探るべく、フランスで形式手法が強い理由をフランス人の研究者に聞いたところ、 「完璧さ」を追求する性質が昔からあるという答えをもらった。ブルバキなどで有名な数学や哲学に昔から高い人気があることが関連しているのではないか、とのことだった。

一方、一人の利用者の視点に立ったとき、鉄道が定時運行することもまた、シス テムが信頼を得るための重要な要素であろう。

日本の鉄道が世界的に見ても時間に正確であることは見逃せない。そのルーツについて、日本の鉄道の正確さについて分析した書籍「定刻発車」では “参勤交代、土木技術、鈴なりの都市群”など、江戸時代にまでさかのぼっている。同書籍によると2003年度のデータとして、一列車の遅 れは新幹線が平均僅か0.3分、在来線で平均0.8分とある。

「定刻発車」でも指摘されているように、鉄道のシステムへの要求はさらに高度化し、システム開発・運用もそれに呼応して高度化していく。これに対し、将来的に信頼性に関する情報を含んだ路線図をマッシュアップで作ることはできないだろうか。そのような路線図では、利用者は、その路線が形式手法を用いて作られていること、さ らに定刻発車が実現されていることを認識できるようになる。日本は定刻発車に関しては既に定評があるのだから、日本のその路線図への貢献度は高くなるだろう。

著者は、この路線図のように信頼性向上に貢献している人たちの仕事を世に伝える仕組みを模索したい。