システムの仕様の誤りを形式的に見つけたい

複雑な動作条件や、多様な環境要因を予測して、仕様を書くのは難しい。

=> 仕様の誤りを見つけて、それを修正しよう

ドアの仕様例

【重要】この仕様が実現不能である

形式化してみると

G: 次の式が必ず成り立つという意味
F: 次の式がいつか成り立つという意味

※詳しくは「LTL式」で検索

式1は、「開けるボタンが押されると、いつか必ずドアは開いている状態になる」
式2は、「閉じるボタンが押されると、ドアは閉じている状態である」

ずーっと（∞）閉じるボタンが押される場合を考える。

式1だと、ずっと閉じるボタンが押されっぱなしでも、開けるボタンが押されたら、いつかドアを開けないといけない。
式2だと、押されっぱなしなら、ずっと閉じている状態でなければならない。

閉じるボタンが押されっぱなし & 開けるボタンも押された　とき、
ドアを開けても、閉めても仕様を満たすことができない

=> この仕様は実現できない

仕様を書く人が、閉じるボタンが押され続ける場合を考慮できなかった。

↓　言い換えると

いつか必ず、閉じるボタンは、押されていない状態になる。という暗黙の前提条件をつけてしまっていた。

入力が、式1, 2だと、
出力は、GF!x2となる

この導出手続きは、先行研究があります。
論文（DOI）
https://doi.org/10.1007/978-3-319-21410-8_51

理論的に、仕様が大きくなると、計算量が膨大になるので、適用できる範囲は狭いです。
研究が進み、いつか実用化されてほしいです。

★インフィニットループは札幌本社・仙台支社を物理拠点に、xRアプリ開発・ゲーム開発を中心に活動しています。

興味がある方は是非採用情報をご確認ください。

ブログ記事検索

このブログについて

このブログは、札幌市・仙台市の「株式会社インフィニットループ」が運営する技術ブログです。お仕事で使えるITネタを社員たちが発信します！

関連記事