|
ソフトウェアは我々の生活に深く入り込んでいる。大変便利であるが、複雑であればあるほど潜在的不具合が存在する可能性は大きい。顕在化すると、財政的損失ばかりでなく人命にも危険が及ぶ可能性すらある。このため、潜在的不具合は可能な限り取り除いたほうが良い。そのための有望な技術にモデル検査がある。しかし、ソフトウェア産業界において日常業務での使用に耐えうるようにするには解決すべき課題がある。状態空間爆発の緩和と実行速度の改善だ。状態空間を複数の空間に分割することで状態空間爆発を緩和し、複数の部分状態空間を並列にモデル検査することで実行速度を改善した。ソフトウェア産業界での実用化に向けて前進できた。
|
