Inferring physical units in formal models.
Saved in:
| 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 121251698 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Inferring physical units in formal models. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Krings%2C+Sebastian%22">Krings, Sebastian</searchLink><relatesTo>1</relatesTo><i> krings@cs.uni-duesseldorf.de</i><br /><searchLink fieldCode="AR" term="%22Leuschel%2C+Michael%22">Leuschel, Michael</searchLink><relatesTo>1</relatesTo><i> leuschel@cs.uni-duesseldorf.de</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Software+%26+Systems+Modeling%22">Software & Systems Modeling</searchLink>. Feb2017, Vol. 16 Issue 1, p25-47. 23p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22B+method+%28Computer+science%29%22">B method (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Formal+languages%22">Formal languages</searchLink><br /><searchLink fieldCode="DE" term="%22Units+of+measurement%22">Units of measurement</searchLink><br /><searchLink fieldCode="DE" term="%22Technical+specifications%22">Technical specifications</searchLink><br /><searchLink fieldCode="DE" term="%22Semantics%22">Semantics</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=121251698 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10270-015-0458-0 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 23 StartPage: 25 Subjects: – SubjectFull: B method (Computer science) Type: general – SubjectFull: Formal languages Type: general – SubjectFull: Units of measurement Type: general – SubjectFull: Technical specifications Type: general – SubjectFull: Semantics Type: general Titles: – TitleFull: Inferring physical units in formal models. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Krings, Sebastian – PersonEntity: Name: NameFull: Leuschel, Michael IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 02 Text: Feb2017 Type: published Y: 2017 Identifiers: – Type: issn-print Value: 16191366 Numbering: – Type: volume Value: 16 – Type: issue Value: 1 Titles: – TitleFull: Software & Systems Modeling Type: main |
| ResultId | 1 |
