Abstract
The first step in building a cyber-physical system is the construction of a faithful model that captures the relevant behaviors. Dimensional consistency provides the first check on the correctness of such models and the physical quantities represented in it. Though manual analysis of dimensions is used in physical sciences to find errors in formulas, this approach does not scale to complex cyber-physical systems with many interacting components. We present DimSim, a tool to automatically check the dimensional consistency of a cyber-physical system modeled in Simulink. DimSim generates a set of constraints from the Simulink model for each subsystem in a modular way, and solves them using the Gauss-Jordan elimination method. The tool depends on user-provided dimension annotations, and it can detect both inconsistency and underspecification in the given dimensional constraints. In case of a dimensional inconsistency, DimSim can provide a minimal set of constraints that captures the cause of the inconsistency. We have applied DimSim to numerous examples from different embedded system domains. Experimental results show that the dimensional analysis in DimSim is scalable and is capable of uncovering critical errors in models of cyber-physical systems.
This work was supported by NSF Grant CSR-EHCS(CPS)-0834810 and NASA Cooperative Agreement NNX08AY53A. We received useful feedback from our colleagues Bruno Dutertre and Ashish Tiwari and from Professor Martin Hofmann of LMU Munich. We are especially grateful to the anonymous reviewers for their constructive and insightful feedback.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allen, E., Chase, D., Luchangco, V., Maessen, J., Steele Jr., G.L.: Object-oriented units of measurement. In: Proceedings of OOPSLA, pp. 384–403 (2004)
Antoniu, T., Steckler, P.A., Krishnamurthi, S., Neuwirth, E., Felleisen, M.: Validating the unit correctness of spreadsheet programs. In: Proceedings of ICSE, pp. 439–448 (2004)
Astrom, K.J., Murray, R.M.: Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press (2009)
Chutinan, A., Butts, K.R.: Smart vehicle baseline report - dynamic analysis of hybrid system models for design validation. Technical report (2002)
Dreiheller, A., Mohr, B., Moerschbacher, M.: PHYSCAL: Programming Pascal with physical units. SIGPLAN Not. 21, 114–123 (1986)
Galdino, A.L., Muñoz, C., Ayala-Rincón, M.: Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 177–188. Springer, Heidelberg (2007)
Hangal, S., Lam, M.S.: Automatic dimension inference and checking for object-oriented programs. In: Proceedings of ICSE, pp. 155–165 (2009)
Hilfinger, P.N.: An ADA package for dimensional analysis. ACM Trans. Program. Lang. Syst. 10, 189–203 (1988)
Jiang, L., Su, Z.: Osprey: A practical type system for validating dimensional unit correctness of C programs. In: Proceedings of ICSE, pp. 262–271 (2006)
Kennedy, A.: Dimension Types. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, pp. 348–362. Springer, Heidelberg (1994)
Kennedy, A.: Types for Units-of-Measure: Theory and Practice. In: Horváth, Z., Plasmeijer, R., Zsók, V. (eds.) CEFP 2009. LNCS, vol. 6299, pp. 268–305. Springer, Heidelberg (2010)
Petty, G.W.: Automated computation and consistency checking of physical dimensions and units in scientific programs. Softw. Pract. Exper. 31, 1067–1076 (2001)
Roche, J.J.: The Mathematics of Measurement: A Critical History. Springer (1998)
Roy, P., Shankar, N.: SimCheck: A contract type system for Simulink. ISSE 7(2), 73–83 (2011)
Sandberg, M., Persson, D., Lisper, B.: Automatic dimensional consistency checking for simulation specifications. In: Proceedings of SIMS (2003)
Strang, G.: Introduction to Linear Algebra, 3rd edn. Wellesley-Cambridge Press (2003)
The MathWorks. Simulink - Demos, http://www.mathworks.com/products/simulink/demos.html
Umrigar, Z.D.: Fully static dimensional analysis with C++. SIGPLAN Not. 29, 135–139 (1994)
Valiant, L., Vazirani, V.: NP is as easy as detecting unique solutions. Theoretical Computer Science, 85–93 (1986)
Van Delft, A.: A Java extension with support for dimensions. Softw. Pract. Exper. 29, 605–616 (1999)
Wand, M., O’Keefe, P.: Automatic dimensional inference. In: Computational Logic-Essays in Honor of Alan Robinson, pp. 479–483 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Owre, S., Saha, I., Shankar, N. (2012). Automatic Dimensional Analysis of Cyber-Physical Systems. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-32759-9_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32758-2
Online ISBN: 978-3-642-32759-9
eBook Packages: Computer ScienceComputer Science (R0)