動的ソフトウェア進化

どんな研究?

システムが稼働中に,デバッグや改良などのためにソフトウェアを変更すること,すなわちソフトウェアの保守は,従来はシステムを一旦停止して行っていました.しかし近年は,システムへの要求や動作環境が急速に変化するため,必要な保守の頻度もますます高まっています.したがって保守のたびにシステムを停止していては,システムの適切な使用が不可能になってしまいます.また膨大な利益を上げるネット上のサービスや,医療システムのような信頼性が重要な場合は,そもそもシステムの停止は望ましくありません.そこでシステムを停止せずにソフトウェアの変更を実施する技術の研究が進められています.このような技術を動的ソフトウェア進化と呼びます.

なにがわかる?

動的ソフトウェア進化においては,システムの稼働を継続しながらソフトウェアを変更するため,変更のタイミングによる不具合の発生が起こりえます.しかしあらゆる変更のタイミングを考慮してテストすることは難しいため,そのような不具合の発見は困難です.そこでソフトウェアの正しさを数学的理論に基づいて厳密に保証するような先進的な手法が必要です.本研究では,モデル検査・制御器合成といった先端技術を応用し,不具合のない動的ソフトウェア進化の実現を目指しています.

研究内容

モデル検査:本手法は,ソフトウェアの振舞いとソフトウェアが満たすべき性質を,それぞれ状態遷移モデルと論理式という数学的な対象で表し,振舞いの動作系列を網羅的に調べることにより,ソフトウェアが性質を満たすことを検証するものです.しかし動的ソフトウェア進化においては,振舞いのモデルの作成は困難です.本研究では,ソフトウェア進化の振舞いのモデルを適切に作成する手法を検討しています.

制御器合成:前述のように,不具合のない動的ソフトウェア進化を実現するためには,ソフトウェア変更のタイミングを適切に制御することが重要です.本研究では,与えられた性質を満たすように変更のタイミング制御の仕様を,数学的理論に基づいて自動合成する手法を検討しています.