概率线性时段不变式的统计模型检验

Statistical Model Checking of Probabilistic Linear Duration Invariants

模型检验是软件工程形式化方法的一个重要组成部分,线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法,该方法针对不带有不确定性的概率模型,运用统计模型检验的方法,基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。

Model Checking is a very important formal method in software engineering. Linear Duration Invariants are important safety properties of real-time systems, which form a decidable subclass of Duration Calculus formulas. In this paper, we propose a verification method for model checking the probabilistic linear duration invariants, based the stochastic models which do not have any nondeterminism. As the results, a model checking tools based on UPPAAL has been developed.