|
研究代表者(小川)はリアルタイムソフトウェアの構造検証のための基礎技術として、(重み付)プッシュダウンモデル検査のスケーラビリティのためのインクリメンタルアルゴリズム、文脈についての条件記述の拡張について研究を進めた。前者はモデル検査の手法でしばしば問題になるメモリオーヴァーフローなどを抑制するのに大きな効果がある。ここでは、ケーススタディとして、Javaの文脈依存points-to解析を取り上げ、現状で20万行程度(2万メソッド程度)のスケーラビリティを得ている。これらはシングルスレッドであるが、現在、マルチスレッドへの拡張(ナイーブに行うと決定不能問題)としてrelationalな抽象化のアプローチや、実行列の制限によるアプローチを検討中である。
研究分担者(小野)はソフトリアルタイムソフトウェアの構想検証のための非同期処理のケースタディとして、webサーバを取り上げ、並列処理環境における非同期処理の高いスケーラビリティの実証と、同期処理におけるボトルネックを明示する実験を行った。具体的には、代表的なWebサーバであるApacheサーバに対し、同期的処理(モノリシックな実装方法)ならびに非同期処理による応答処理を実装し、過負荷試験による応答速度低下の測定実験を行った。さらにwebアプリケーションにおけるロール(セキュリティレベル)に応じたアクセス制御モデルを構築し、複数のアクセスが競合する環境下におけるSpinを用いた形式検証手法のケーススタディを進めた。
|
