Runtime-Error Verification via All-Path Reachability Problems of Constrained Rewriting
2023年度研究会推薦博士論文速報
［プログラミング研究会］
小嶋 美咲
（名古屋大学 日本学術振興会特別研究員）
邦訳：制約付き書換えの全パス到達可能性問題への帰着による実行時エラー検証
■キーワード
項書換え系／プログラム検証／形式手法
【背景】書換え理論を用いたプログラムの検証技術
【問題】並行システムの実行時エラー検証
【貢献】全パス到達可能性への帰着による検証法の提案
現在，ソフトウェアは日常生活のあらゆる場面で利用されており，ソフトウェア開発においてプログラムが正しいかどうかの検証作業は非常に重要なタスクである．検証する性質はさまざまで，他のプログラムと同じ振る舞いをすること（等価性）や，プログラムを実行した際にその実行が停止すること（停止性），プログラムの実行時にエラーが発生しないことなどがある．近年，プログラムを論理制約付き項書換え系（LCTRS）に変換をして，停止性などの性質を検証するという研究が進められている．実行中の関数の状態や変数の値などを関数記号の引数として保持させることで，プログラムの環境を項で表し，その項を書換え規則によって書換えていくことで，LCTRSはプログラムの計算をシミュレーションすることができる．
LCTRSを使ったプログラム検証の研究は，実用的なプログラムの検証への応用が期待されている．特に現実のコンピュータの利用状況を考えると，複数のプロセスが並行に実行されるシステムに対して，実行時にエラーが発生しないことを検証することが強く求められている．ソフトウェアにエラーが発生すると，経済的な損失や人命にかかわる重大な結果につながる恐れがある．したがって，開発の初期段階で，プログラムに理論上はエラーが発生しないことを保証することは大きな意味がある．そこで本研究では，並行プログラムからLCTRSへの変換法と，全パス到達可能性問題という決定問題を利用したエラー検証法の2つを提案した．
並行プログラムからLCTRSへの変換については，1つのプロセスのみが実行される逐次プログラムからLCTRSへの変換を拡張する形で実現した．プロセスの環境を表す項の引数を増やすことで複数のプロセスの状態を表現し，逐次プログラムでは扱われない，セマフォを利用した排他制御をLCTRSで表現した．
エラー検証については，プログラムの実行時にエラーが発生するかどうかを，全パス到達可能性問題という決定問題に置き換えることで検証する方法を提案した．全パス到達可能性問題とは，出発地点となる状態の集合Pと，目的地となる状態の集合Qが与えられたとき，Pに含まれる状態からどのような経路をたどっても，Qに含まれる状態にたどり着くことが可能かどうかを判定する問題である．Pを「プログラムの初期状態」，Qを「エラーが発生していない正常な状態」とすると，エラーが発生するかどうかは「初期状態からどのように実行しても，エラーが発生していない正常な状態のみにたどり着くか」という全パス到達可能性問題として捉えることができる．この方法は，停止性を持たずにループし続けるプログラムに対しても有用であり，プログラムの初期状態からたどることができるあらゆるパスについて検証することができる．本研究では全パス到達可能性問題を解くツールを実装し，競合状態やスタベーションが発生しないことを証明する実験を実施した．
（2024年5月28日受付）
（2024年8月15日note公開）
ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー
取得年月：2024年3月
学位種別：博士（情報学）
大学：名古屋大学
正会員
ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー
推薦文［コンピュータサイエンス領域］プログラミング研究会
ソフトウェアにエラーが発生すると人の命にかかわる恐れがあります．開発の初期段階に抽象モデルやプログラムに理論上はエラーが発生しないことを保証することは大きな意味があります．本論文は論理制約付き項書換えシステムという計算モデルを利用して実行時にエラーが発生しないことを保証する技術を提案しています．
研究生活 並行プログラムの検証という研究テーマは，学部生時代から継続して取り組んできたものです．研究室で続けられてきたプログラム検証の研究において，逐次プログラムの検証を並行プログラムに拡張する転換期に，ちょうど研究室に配属されたことがきっかけでした．私は理論研究の中でも，現実社会に直結して役立つ研究をしたいと志しており，このテーマがピッタリだと感じました．結果的には，このテーマを追求し，博士論文を書くにまで至りました．
研究が本格化するタイミングでコロナ禍が重なったことで研究の進め方が大きく変わってしまい，大変なことも多々ありました．しかし研究を進めていく上で何かを新たに発見をする喜びや，その成果を認めてもらえる喜びも多く経験しました．