Memory State Verification Based on Inductive and Deductive Reasoning [li21]

  • 提案: メモリの状態をメモリブロックのリストとして抽象化し、これに対する操作(遷移関数)としてアロケータの振る舞いを有限状態遷移機械として形式化・検証する

    • この枠組みを用いてTLSFの検証・runtime verificationへの応用

    • フットプリントの小さなシステムを仮定した上で、メモリ状態を表す表現を工夫して状態爆発を防いでいる

    • runtime verification: 実際に動作中のシステムのメモリ状態を、提案の表現に変換し、検証に用いた不変条件を満たすか検証

A verified specification of TLSF memory management allocator using State Monads [zhang19]

  • TLSFの形式仕様をIsabelleで形式化・状態モナドによる意味論を与えた擬似言語による実装を検証

  • メモ

Towards formal verification of dynamic memory allocator properties using BIP framework [lu21]

Formal Development of a Real-Time Operating System Memory Manager [abrial15]

  • Event-B/Rodinと段階的詳細化による検証と実装

本研究との差分

  • 既存のbattle-testedな実装を対象に(code-level)、(要検証: 許容可能なオーバヘッドで)定理証明による高信頼な検証を行った

    • 既存の実装を対象にした難しさ: パラメータの自由度・ビット演算など

  • [lu21]は、メモリモデルの詳細を考慮していないため、実際に動作する実装とのギャップが大きい

  • [li21]もcode-levelではない

  • [abrial15]はコード生成による、また証明の量で差別化できる?

bibliography

  • [zhang19] Y. Zhang, Y. Zhao, D. Sanan, L. Qiao, and J. Zhang, “A verified specification of TLSF memory management allocator using State Monads,” Lecture Notes in Computer Science, pp. 122–138, 2019. doi:10.1007/978-3-030-35540-1_8

  • [lu21] X. Lu et al., “Towards formal verification of dynamic memory allocator properties using BIP framework,” Proceedings of the 5th International Conference on Computer Science and Application Engineering, pp. 1–7, Oct. 2021. doi:10.1145/3487075.3487122

  • [li21] S. Li, L. Qiao and M. Yang, "Memory State Verification Based on Inductive and Deductive Reasoning," in IEEE Transactions on Reliability, vol. 70, no. 3, pp. 1026-1039, Sept. 2021, doi: 10.1109/TR.2021.3074709.

  • [abrial15] W. Su, J. -R. Abrial, G. Pu and B. Fang, "Formal Development of a Real-Time Operating System Memory Manager," 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), Gold Coast, QLD, Australia, 2015, pp. 130-139, doi: 10.1109/ICECCS.2015.24.

  • [li23] Qiming Li, Xia Yang, Haiyong Sun, and Zhe Yan. 2023. Automatic Generation of Formal BIP Models for C Programs. In Proceedings of the 7th International Conference on Computer Science and Application Engineering (CSAE '23). Association for Computing Machinery, New York, NY, USA, Article 52, 1–7. https://doi.org/10.1145/3627915.3628026