Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Mobile Networks and Applications
Published in: Mobile Networks and Applications 1/2016

01-02-2016

SMT-Based Symbolic Encoding and Formal Analysis of HML Models

Authors: Huixing Fang, Huibiao Zhu, Jifeng He

Published in: Mobile Networks and Applications | Issue 1/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Hybrid system is a dynamic system that involves continuous, discrete behaviors, and the interactions between continuous physical components and discrete controllers. In this paper a hybrid modeling language (called HML) for hybrid systems is extended with templates to achieve code reuse. For the formal analysis of the corresponding hybrid system models in this modeling language, these models are translated into SMT (satisfiability modulo theories) formulas as the input to an SMT solver dReal which retains the capability of bounded reachability analysis for non-linear hybrid systems. Moreover, dReal can produce data for potential traces of hybrid systems, thus it can be employed to simulate on hybrid systems. In this paper the simulation and reachability analysis are integrated in a prototype tool (open source). We present a case study for an inverted pendulum with PID (Proportional-Integral-Derivative) controllers and a rod reactor system for temperature control, both are verified to demonstrate the efficiency of the prototype tool. We conclude that, this modeling language is capable of modeling and verification of hybrid systems based on simulation and bounded reachability analysis.
previous article Social Networking Ontology Engineering Walkthrough: Practical Approach for Non-Expert User Learning
next article Two Fuzzy-Based Systems for Selection of Actor Nodes inWireless Sensor and Actor Networks: A Comparison Study Considering Security Parameter Effect

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Show more products
Appendix
Available only for authorised users
Footnotes
1
https://​github.​com/​fanghuixing/​HML. The main task of this tool is translating HML models into SMT formulas which can be checked w.r.t. the satisfiability of properties based on dReal. The syntax of HML was expressed and encoded based on Terence Parr’s tool ANTLRv4. The checking result was stored in a JSON file which consists of the states of the corresponding hybrid system. The JSON file was analyzed and filtered, then sent to JfreeChart for graphical demonstration of system states and behaviors
 
Literature
1.
Alur R, Courcoubetis C, Henzinger TA, Ho PH (1993) Hybrid Automata: An Algorithmic Approach to the Specification and Analysis of Hybrid Systems. In: Hybrid Systems, LNCS, vol 736. doi:10.​1007/​3-540-57318-6_​30. Springer, pp 209–229
2.
Åström KJ, Hägglund T (2006) Advanced PID control. ISA-The Instrumentation, Systems, and Automation Society, Research Triangle Park, NC 27709
3.
Baeten JCM, Weijland WP (1990) Process Algebra. Cambridge University Press
4.
Barrett C, Stump A, Tinelli C (2010) The SMT-LIB Standard: Version 2.0. Tech. rep., Department of Computer Science, The University of Iowa, available at www.​SMT-LIB.​org
5.
Berz M (1999) Modern Map Methods in Particle Beam Physics. ADV IMAG ELECT PHYS, vol 108. Elsevier
6.
Berz M, Makino K (1998) Verified Integration of ODEs and Flows Using Differential Algebraic Methods on High-Order Taylor Models. Reliab Comput 4(4):361–369MathSciNetCrossRefMATH
7.
Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT Solver. In: Proceedings of TACAS, LNCS, vol 6015. Springer, Berlin, pp 150–153
8.
Chang WD, Shih SP (2010) PID Controller Design of Nonlinear Systems Using an Improved Particle Swarm Optimization Approach. Commun Nonlinear Sci 15(11):3632–3639CrossRefMATH
9.
Chen X, Ábrahám E, Sankaranarayanan S (2013) Flow*: An Analyzer for Non-linear Hybrid Systems. In: Proceedings of CAV, LNCS, vol 8044. Springer, pp 258–263
10.
Chen X, Schupp S, Makhlouf I, Ábrahám E, Frehse G, Kowalewski S (2015) A Benchmark Suite for Hybrid Systems Reachability Analysis. In: NASA Formal Methods, LNCS, vol 9058. Springer, pp 408–414
11.
12.
13.
Frehse G, Han Z, Krogh B (2004) Assume-Guarantee Reasoning for Hybrid I/O-Automata by Over-Approximation of Continuous Interaction. In: Proceedings of CDC. IEEE, pp 479–484
14.
Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: Scalable Verification of Hybrid Systems. In: Proceedings of CAV, LNCS, vol 6806. Springer, pp 379–395
15.
Fritzson P, Engelson V (1998) Modelica–A Unified Object-Oriented Language for System Modeling and Simulation. In: Proceedings of ECOOP, LNCS, vol 1445. Springer, pp 67–90
16.
Gao S, Avigad J, Clarke EM (2012) Delta-Decidability Over the Reals. In: Proceedings of LICS. IEEE, pp 305–314
17.
Gao S, Kong S, Clarke EM (2013a) dReal: An SMT Solver for Nonlinear Theories Over the Reals. In: Proceedings of CADE. Springer, pp 208–214
18.
Gao S, Kong S, Clarke EM (2013b) Satisfiability Modulo ODEs. In: Proceedings of FMCAD. IEEE, pp 105–112
19.
Granvilliers L, Benhamou F (2006) Algorithm 852: RealPaver: An Interval Solver Using Constraint Satisfaction Techniques. ACM T Math Software 32(1):138–156MathSciNetCrossRef
20.
Guernic CL, Girard A (2010) Reachability Analysis of Linear Systems Using Support Functions. Nonlinear Analysis: Hybrid Systems 4(2):250–262MathSciNetMATH
21.
Guo X, Hernndez-Lerma O (2009) Continuous-time markov decision processes. Stochastic Modelling and Applied Probability, vol 62. Springer, Berlin, pp 9–18
22.
23.
He J (1994) From CSP to Hybrid Systems. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, Prentice Hall International, pp 171–189
24.
He J (2013) Hybrid Relation Calculus. In: Proceedings of ICECCS. IEEE, p 2
25.
Henzinger TA (1996) The Theory of Hybrid Automata. In: Proceedings of LICS. IEEE, pp 278–292
26.
Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech : A Model Checker for Hybrid Systems. Int J Softw Tools Technol Transfer 1(1–2):110–122CrossRefMATH
27.
Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What’s Decidable about Hybrid Automata? Journal of Computer and System Sciences 57:94–124MathSciNetCrossRefMATH
28.
Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall
29.
30.
Kong S, Gao S, Chen W, Clarke E (2015) dReach: Delta-Reachability Analysis for Hybrid Systems. In: Proceedings of TACAS, Springer-Verlag, LNCS, vol 9035, pp 200–205
31.
Lynch N, Segala R, Vaandrager F, Weinberg H (1996) Hybrid I/O Automata. In: Hybrid Systems III, LNCS, vol 1066. Springer, pp 496–510
32.
Lynch N, Segala R, Vaandrager F (2001) Hybrid I/O Automata Revisited. In: Proceedings of HSCC, LNCS, vol 2034. Springer, pp 403–417
33.
Maler O, Manna Z, Pnueli A (1992) From Timed to Hybrid Systems. In: Real-Time: Theory in Practice, LNCS, vol 600. Springer, Berlin, pp 447–484CrossRef
34.
35.
36.
Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). J ACM 53(6):937–977MathSciNetCrossRefMATH
37.
38.
Platzer A (2010) Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer
39.
Von Mohrenschildt M (2001) Symbolic Verification of Hybrid Systems: An Algebraic Approach. Eur J Control 7(5):541–556CrossRefMATH
40.
Weihrauch K (2000) Computable Analysis: An Introduction. Springer
41.
Yi J, Yubazaki N (2000) Stabilization Fuzzy Control of Inverted Pendulum Systems. Artif Intell Eng 14(2):153–163CrossRef
42.
Zhou C, Wang J, Ravn AP (1996) A Formal Description of Hybrid Systems. In: Hybrid Systems III, LNCS, vol 1066. Springer, pp 511–530
Metadata
Title
SMT-Based Symbolic Encoding and Formal Analysis of HML Models
Authors
Huixing Fang
Huibiao Zhu
Jifeng He
Publication date
01-02-2016
Publisher
Springer US
Published in
Mobile Networks and Applications / Issue 1/2016
Print ISSN: 1383-469X
Electronic ISSN: 1572-8153
DOI
https://doi.org/10.1007/s11036-015-0671-7

Other articles of this Issue 1/2016

Mobile Networks and Applications 1/2016 Go to the issue

OriginalPaper

The Structural Role of Feed-Forward Loop Motif in Transcriptional Regulatory Networks

OriginalPaper

Evolutionary Multiobjective Optimization for the Pickup and Delivery Problem with Time Windows and Demands

OriginalPaper

An Ontology-Based Multi-Agent System for Active Software Engineering Ontology

OriginalPaper

Autonomous Ant-based Public Key Authentication Mechanism for Mobile Ad-hoc Networks

OriginalPaper

Exploring Social Networks and Improving Hypertext Results for Cloud Solutions

EditorialNotes

Nature of Computation and Communication