Inferring physical units in formal models

详细信息    查看全文

• 作者：Sebastian Krings ; Michael Leuschel
• 关键词：B ; method ; Event ; B ; Physical units ; Model checking ; Abstract interpretation
• 刊名：Software & Systems Modeling
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：16
• 期：1
• 页码：25-47
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Software Engineering/Programming and Operating Systems; Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Information Systems Applications (incl.Internet);
• 出版者：Springer Berlin Heidelberg
• ISSN：1619-1374
• 卷排序：16

文摘

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 the ProB validation 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 to TLA\(^+\), an untyped formal language. We provide an in-depth empirical evaluation and demonstrate that our technique scales up to real-life industrial models.