Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 1/2017

26.03.2015 | Special Section Paper

Inferring physical units in formal models

verfasst von: Sebastian Krings, Michael Leuschel

Erschienen in: Software and Systems Modeling | Ausgabe 1/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel Constraint-based test generation for automotive operating systems
Nächster Artikel Introduction to the theme issue on variability modeling of software-intensive systems

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
See, however, [24].
 
2
We return to this example in Sect. 7.1 and provide further details there.
 
3
Note that this set includes not just functions but all relations between integers. In B and ProB  functions and relations have the same type; operators for relations can be applied to functions and vice versa. The fact that a relation is indeed a function is encoded as an invariant and verified for each state, i.e., it is a safety property of the system.
 
4
Note that for Event-B, the Rodin tool will produce an error message if a variable or expression’s type contains \(\top \).
 
5
For convenience, some SI derived units and units accepted for use with the SI standard (see [35]) are stored on their own rather than converting them.
 
6
Basically, which means adding the exponents of the leading 10 of each SI unit.
 
7
In contrast to TLA \(^+\), B does not support \(n < 0\) as the first argument to the modulo operator. This is taken into account by the translation from TLA \(^+\) to B.
 
8
Note that there is only experimental support for floating point numbers in B and Event-B. Hence, we currently do not support conversions like the one from seconds to minutes using \(\frac{1}{60}\) as a conversion factor. It would, however, be possible to implement this as an extension of our approach, and we will do so once real/float support stabilizes. TLA \(^+\) supports real numbers. However, at the moment, our translation does not.
 
10
Both were counted on the internal representation of the machines. Thus, the metrics include code from imported machines. Comments are not counted, as they are not in the internal representation. However, new lines used for pretty printing are counted.
 
11
The tutorial including the machines can be found at http://​www.​tools.​clearsy.​com/​wp1/​?​page_​id=​161.
 
12
The exception being variables and sets belonging to the system’s status. Here, no unit of measurement applies, and no unit was inferred.
 
13
Upon request of our industrial customers, we since added several custom units to the units included by default. Conversion rules were added as well.
 
14
A relation constructed as the set union of the two lambda expressions. Depending on the condition of the if expression, one of the lambda expressions is empty, while the other one contains exactly one element: the result of the if expression. We apply the relation to 1 to extract this element.
 
Literatur
1.
2.
Abrial, J.R.: Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
3.
Abrial, J.R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) Proceedings ICFEM’06, LNCS 4260, pp. 588–605. Springer, Berlin (2006). doi:10.​1007/​s10009-010-0145-y
4.
Abrial, J.R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Proceedings ABZ’12, LNCS 7316, pp. 178–193. Springer, Berlin (2012)
5.
Anand, M., Lee, I., Pappas, G., Sokolsky, O.: Unit & dynamic typing in hybrid systems modeling with CHARON. In: Computer Aided Control System Design, pp. 56–61. IEEE (2006)
6.
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 447–533. Elsevier Science Publishers (2001)
7.
Back, R.J., Seceleanu, C.C., Westerholm, J.: Symbolic simulation of hybrid systems. In: Proceedings APSEC’02, pp. 147–155. IEEE Computer Society (2002)
8.
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. Technical report, Department of Computer Science, University of Iowa (2010). www.​SMT-LIB.​org
9.
Boute, R.T.: The Euclidean definition of the functions div and mod. ACM Trans. Program. Lang. Syst. 14(2), 127–144 (1992)CrossRef
10.
11.
12.
Collins, J.B.: A mathematical type for physical variables. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science, vol. 5144, pp. 370–381. Springer, Berlin Heidelberg (2008)CrossRef
13.
Cousot, P.: Types as abstract interpretations. In: Conference Record of the Twentyfourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 316–331. ACM Press, New York, NY, Paris, France (1997)
14.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings POPL’77, pp. 238–252. ACM, New York (1977)
15.
Cunis, R.: A package for handling units of measure in Lisp. ACM SIGPLAN Lisp Pointers 5, 21–25 (1992)CrossRef
16.
17.
Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: Proceedings iFM’2012, LNCS 7321, pp. 24–38. Springer, Berlin (2012)
18.
Hayes, I.J., Mahony, B.P.: Using units of measurement in formal specifications. Form. Aspects Comput 7(3), 329–347 (1995)CrossRef
19.
Jiang, L., Su, Z.: Osprey: a practical type system for validating dimensional unit correctness of C programs. In: Proceedings ICSE’06, pp. 262–271. ACM (2006)
20.
Kennedy, A.: Types for units-of-measure: theory and practice. In: Horváth, Z., Plasmeijer, R., Zsók, V. (eds.) Central European Functional Programming School. Lecture Notes in Computer Science, vol. 6299, pp. 268–305. Springer, Berlin Heidelberg (2010)
21.
Knuth, D.E.: The art of computer programming, Volume 1: fundamental algorithms. Addison Wesley Longman Publishing Co., Inc, Redwood City (1997)MATH
22.
Krings, S., Leuschel, M.: Inferring physical units in B models. In: Proceedings SEFM’2013, LNCS 8137. Springer, Berlin (2013)
23.
Lamport, L.: Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Boston (2002)
24.
Lamport, L., Paulson, L.C.: Should your specification language be typed. ACM Trans. Program. Lang. Syst. 21(3), 502–526 (1999)CrossRef
25.
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Proceedings FME’03, LNCS 2805, pp. 855–874. Springer, Berlin (2003)
26.
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef
27.
Lockwood, G.: Final Report of the Board of Injury: Investigating the Circumstances of an Accident Involving the Air Canada Boeing 767 Aircraft C-GAUN that Effected an Emergency Landing at Gimli, Manitoba on the 23rd Day of July, 1983. Minister of Supply and Services Canada (1985). https://​books.​google.​de/​books?​id=​Ej5PAAAAMAAJ
28.
29.
Owre, S., Saha, I., Shankar, N.: Automatic dimensional analysis of cyber-physical systems. In: Proceedings FM’12, LNCS 7436, pp. 356–371. Springer, Berlin (2012)
30.
Platzer, A.: Logical analysis of hybrid systems: proving theorems for complex dynamics. Springer, Berlin (2010)CrossRefMATH
31.
32.
Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23–25, 1995, pp. 49–61 (1995). doi:10.​1145/​199448.​199462
33.
Roy, P., Shankar, N.: SimCheck: an expressive type system for Simulink. In: Proceedings NFM’10, pp. 149–160. NASA (2010)
34.
Stephenson, A., LaPiana, L., Mulville, D., Rutledge, P., Bauer, F., Folta, D., Dukeman, G., Sackheim, R., Norvig, P.: Mars climate orbiter—mishap investigation report—phase i report (1999)
35.
Thompson, A., Taylor, B.N.: The international system of units (SI). National Institute of Standards and Technology / U.S. Department of Commerce, Gaithersburg (2008)CrossRef
36.
Umrigar, Z.: Fully static dimensional analysis with C++. ACM SIGPLAN Not. 29, 135–139 (1994)CrossRef
37.
van Delft, A.: A Java extension with support for dimensions. Softw. Pract. Exp. 29(7), 605–616 (1999)CrossRef
38.
Wand, M., O’Keefe, P.: Automatic dimensional inference. In: Lassez, J.L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 479–483. MIT Press, Cambridge, MA (1991)
Metadaten
Titel
Inferring physical units in formal models
verfasst von
Sebastian Krings
Michael Leuschel
Publikationsdatum
26.03.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 1/2017
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-015-0458-0

Weitere Artikel der Ausgabe 1/2017

Software and Systems Modeling 1/2017 Zur Ausgabe

Theme Section Paper

The shape of feature code: an analysis of twenty C-preprocessor-based systems

Regular Paper

Analysing the cognitive effectiveness of the WebML visual notation

Regular Paper

Eugenia: towards disciplined and automated development of GMF-based graphical model editors

Theme Section Paper

Empirical assessment of two approaches for specifying software product line use case scenarios

Regular Paper

Integrating business process simulation and information system simulation for performance prediction

Guest Editorial

Introduction to the Software Engineering and Formal Methods 2013 special issue

Premium Partner

    Bildnachweise