Name
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. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/s10270-015-0458-0 | Software and Systems Modeling (SoSyM) |
Keywords | Field | DocType |
B-method, Event-B, Physical units, Model checking, Abstract interpretation | Units of measurement,Model checking,Formal language,Programming language,Abstract interpretation,Computer science,Theoretical computer science,B-Method,Animation,Formal methods | Journal |
Volume | Issue | ISSN |
16 | 1 | 1619-1366 |
Citations | PageRank | References |
0 | 0.34 | 23 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sebastian Krings | 1 | 25 | 8.93 |
| Michael Leuschel | 2 | 2156 | 135.89 |