Inferring physical units in formal models
Inferring physical units in formal models
复制标题
推断正式模型中的物理单位
DOI：
10.1007/s10270-015-0458-0
复制
发表时间：
2017
影响因子：
2
通讯作者：
Michael Leuschel
中科院分区：
文献类型：
--
作者：
Sebastian Krings;Michael Leuschel
大多数基于状态的形式化方法，如B、Event-B或Z，都支持静态类型。但是，这些方法和相关工具缺乏对使用（物理）测量单位注释变量的支持。因此，没有明显的方法来推理这些单位的正确或不正确的用法。我们提出了一种技术，分析整个B和事件-B机器的物理单元的使用情况，推断丢失的单元，并通知用户错误处理的单元。该技术将抽象解释与经典动画、约束求解和模型检查相结合，并已集成到ProB验证工具中，适用于经典B和Event-B。它提供关于模型中检测到的错误的源代码级反馈。我们还描述了如何将我们的方法扩展到TLA，一种无类型的形式语言。我们提供了深入的实证评估，并证明我们的技术可扩展到现实生活中的工业模型。
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated tools lack support for annotating variables with (physical) units of measurement. There is thus no obvious way to reason about correct or incorrect usage of such units. We present a technique that analyzes the usage of physical units throughout B and Event-B machines infers missing units and notifies the user of incorrectly handled units. The technique combines abstract interpretation with classical animation, constraint solving and model checking and has been integrated into theProBvalidation tool, both for classical B and for Event-B. It provides source-level feedback about errors detected in the models. We also describe how to extend our approach toTLA, an untyped formal language. We provide an in-depth empirical evaluation and demonstrate that our technique scales up to real-life industrial models.
登录
查看更多内容
使用 C 进行完全静态尺寸分析
影响因子：
--
作者：
Zerksis D. Umrigar
通讯作者：
Zerksis D. Umrigar
在正式规范中使用测量单位
影响因子：
1
作者：
I. Hayes;Brendan P. Mahony
通讯作者：
Brendan P. Mahony
将 TLA 转换为 B 以使用 ProB 进行验证
DOI：
--
发表时间：
2012
期刊：
International Conference on Integrated Formal Methods
影响因子：
--
作者：
Dominik Hansen;M. Leuschel
通讯作者：
M. Leuschel
Lisp 中处理测量单位的包
DOI：
--
发表时间：
1992
期刊：
LIPO
影响因子：
--
作者：
R. Cunis
通讯作者：
R. Cunis
信息物理系统的自动维度分析
DOI：
--
发表时间：
2012
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
S. Owre;I. Saha;N. Shankar
通讯作者：
N. Shankar