计算机科学
水准点(测量)
实施
概率逻辑
代表(政治)
煤气表校准仪
理论计算机科学
软件实现
程序设计语言
模型检查
软件
算法
自动定理证明
人工智能
数学
数学证明
几何学
大地测量学
政治
政治学
法学
地理
作者
Arnd Hartmanns,Bram Kohlen,Peter Lammich
标识
DOI:10.1007/978-3-031-45329-8_9
摘要
High-performance probabilistic model checkers like the Modest Toolset’s mcsta follow the topological ordering of an MDP’s strongly connected components (SCCs) to speed up the numerical analysis. They use hand-coded and -optimised implementations of SCC-finding algorithms. Verified SCC-finding implementations so far were orders of magnitudes slower than their unverified counterparts. In this paper, we show how to use a refinement approach with the Isabelle theorem prover to formally verify an imperative SCC-finding implementation that can be swapped in for mcsta ’s current unverified one. It uses the same state space representation as mcsta, avoiding costly conversions of the representation. We evaluate the verified implementation’s performance using an extensive benchmark, and show that its use does not significantly influence mcsta ’s overall performance. Our work exemplifies a practical approach to incrementally increase the trustworthiness of existing model checking software by replacing unverified components with verified versions of comparable performance.
科研通智能强力驱动
Strongly Powered by AbleSci AI