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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Mobile Networks and Applications
Erschienen in: Mobile Networks and Applications 1/2016

01.02.2016

SMT-Based Symbolic Encoding and Formal Analysis of HML Models

verfasst von: Huixing Fang, Huibiao Zhu, Jifeng He

Erschienen in: Mobile Networks and Applications | Ausgabe 1/2016

Einloggen

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

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.
Vorheriger Artikel Social Networking Ontology Engineering Walkthrough: Practical Approach for Non-Expert User Learning
Nächster Artikel Two Fuzzy-Based Systems for Selection of Actor Nodes inWireless Sensor and Actor Networks: A Comparison Study Considering Security Parameter Effect

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 "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

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
Weitere Produktempfehlungen anzeigen
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
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
 
Literatur
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.
Frehse G (2008) PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. Int J Softw Tools Technol Transfer 10(3):263–279MathSciNetCrossRefMATH
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
Metadaten
Titel
SMT-Based Symbolic Encoding and Formal Analysis of HML Models
verfasst von
Huixing Fang
Huibiao Zhu
Jifeng He
Publikationsdatum
01.02.2016
Verlag
Springer US
Erschienen in
Mobile Networks and Applications / Ausgabe 1/2016
Print ISSN: 1383-469X
Elektronische ISSN: 1572-8153
DOI
https://doi.org/10.1007/s11036-015-0671-7

Weitere Artikel der Ausgabe 1/2016

Mobile Networks and Applications 1/2016 Zur Ausgabe

EditorialNotes

Editorial: Advances on Bio-inspired Information, Communication and Computational Systems

OriginalPaper

Epistatic Signaling and Minority Games, the Adversarial Dynamics in Social Technological Systems

OriginalPaper

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

OriginalPaper

Base Station Location -Aware Optimization Model of the Lifetime of Wireless Sensor Networks

OriginalPaper

Social Networking Ontology Engineering Walkthrough: Practical Approach for Non-Expert User Learning

OriginalPaper

Dependable Traffic Control Strategies for Urban and Freeway Networks

Neuer Inhalt

    Bildnachweise