Bibliographic Details
| Title: |
Inferring physical units in formal models. |
| Authors: |
Krings, Sebastian1 krings@cs.uni-duesseldorf.de, Leuschel, Michael1 leuschel@cs.uni-duesseldorf.de |
| Source: |
Software & Systems Modeling. Feb2017, Vol. 16 Issue 1, p25-47. 23p. |
| Subjects: |
B method (Computer science), Formal languages, Units of measurement, Technical specifications, Semantics |
| Abstract: |
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. [ABSTRACT FROM AUTHOR] |
|
Copyright of Software & Systems Modeling is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
