JMLによるアプリケーションの安全性保証:Maildirフォルダライブラリの一貫性保証
スポンサーリンク
概要
- 論文の詳細を見る
我々は電子メールのメッセージをディスクに保存する形式の一つであるMaildirフォルダの形式仕様をJMLを用いてそのソースコードに埋め込み、検証を行いつつ開発を進めている。このようなメッセージを扱うライブラリは、ライブラリ自身のバグによってメッセージが失われたり、システムが異常終了した場合などにフォルダが壊れたりすることがないよう、注意深く作成する必要がある。また、このライブラリの使用者が不適切な操作によってメッセージを失うことがないよう、ライブラリの仕様を使用者に明示し、それに従うよう強制しなければならない。最終目標は、Maildirフォルダの仕様の範囲内でライブラリを操作していれば、上記のような原因でメッセージが失われることがないことが保証されるものを提供することである。また、このライブラリの使用者が仕様に基づかない操作を行わないか、検査する方法についても考察する。
- 日本ソフトウェア科学会の論文
日本ソフトウェア科学会 | 論文
- LCDと透明弾性体の光弾性を用いたユーザインタフェース (特集 インタラクティブシステムとソフトウェア)
- Bluetoothによる位置検出
- COINSにおけるSIMD並列化(最新コンパイラ技術とCOINSによる実践)
- データ型を考慮した軽量なXML文書処理系の自動生成(ソフトウェア開発を支援する基盤技術)
- 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)