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
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 2/2013

01.10.2013

A compositional modelling and analysis framework for stochastic hybrid systems

verfasst von: Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, Joost-Pieter Katoen

Erschienen in: Formal Methods in System Design | Ausgabe 2/2013

Einloggen

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

search-config
loading …

Abstract

The theory of hybrid systems is well-established as a model for real-world systems consisting of continuous behaviour and discrete control. In practice, the behaviour of such systems is also subject to uncertainties, such as measurement errors, or is controlled by randomised algorithms. These aspects can be modelled and analysed using stochastic hybrid systems. In this paper, we present HModest, an extension to the Modest modelling language—which is originally designed for stochastic timed systems without complex continuous aspects—that adds differential equations and inclusions as an expressive way to describe the continuous system evolution. Modest is a high-level language inspired by classical process algebras, thus compositional modelling is an integral feature. We define the syntax and semantics of HModest and show that it is a conservative extension of Modest that retains the compositional modelling approach. To allow the analysis of HModest models, we report on the implementation of a connection to recently developed tools for the safety verification of stochastic hybrid systems, and illustrate the language and the tool support with a set of small, but instructive case studies.
Vorheriger Artikel Model checking for probabilistic timed automata
Nächster Artikel Computable fixpoints in well-structured symbolic model checking

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
Our implementation also supports fixed-size arrays and user-defined data structures, which are technical extensions but not conceptually relevant for this paper.
 
2
Since we omitted the details of the expression syntax, we assume type correctness in assignments, guards, weights etc. instead of providing the (standard) type checking rules in detail.
 
3
The semantics of par { ::Tank()::Controller() } itself contains additional locations because the two process calls are not syntactically equal to the behaviours of the processes called. The semantics shown above can be obtained as the semantics of the entire model by replacing the do construct in the Controller process by a (tail-)recursive process call and the call Tank() in the parallel composition by a direct call to TankOff().
 
5
Computations were performed on an AMD Athlon II X4 620 system with 4 GB RAM.
 
6
Computations were performed on an Intel Core i7 860 system with 8 GB RAM.
 
7
Computations were performed on an Intel Core i7 860 system with 8 GB RAM.
 
Literatur
1.
Abate A, Katoen J, Lygeros J, Prandini M (2010) Approximate model checking of stochastic hybrid systems. Eur J Control 16(6):624–641 MathSciNetCrossRefMATH
2.
Abate A, Prandini M, Lygeros J, Sastry S (2008) Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11):2724–2734 MathSciNetCrossRefMATH
3.
Altman E, Gaitsgory V (1997) Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process. SIAM J Control Optim 35(6):2070–2085 MathSciNetCrossRefMATH
4.
Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3–34 CrossRefMATH
5.
Alur R, Dang T, Esposito JM, Hur Y, Ivancic F, Kumar V, Lee I, Mishra P, Pappas GJ, Sokolsky O (2003) Hierarchical modeling and analysis of embedded systems. Proc IEEE 91(1):11–28 CrossRef
6.
Alur R, Dang T, Ivancic F (2006) Predicate abstraction for reachability analysis of hybrid systems. ACM Trans Embed Comput Syst 5(1):152–199 CrossRef
7.
8.
Baró Graf H, Hermanns H, Kulshrestha J, Peter J, Vahldiek A, Vasudevan A (2011) A verified wireless safety critical hard real-time design. In: IEEE int symp on a world of wireless, mobile and multimedia networks (WoWMoM). IEEE Press, New York
9.
van Beek DA, Man KL, Reniers MA, Rooda JE, Schiffelers RRH (2006) Syntax and consistent equation semantics of hybrid Chi. J Log Algebr Program 68(1–2):129–210 MathSciNetCrossRefMATH
10.
Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems (SFM-RT). LNCS, vol 3185. Springer, Berlin, pp 200–236 CrossRef
11.
Berendsen J, Jansen DN, Katoen JP (2006) Probably on time and within budget: on reachability in priced probabilistic timed automata. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 311–322
12.
Bernadsky M, Sharykin R, Alur R (2004) Structured modeling of concurrent stochastic hybrid systems. In: Formal modelling and analysis of timed systems, and formal techniques in real-time and fault-tolerant systems (FORMATS/FTRTFT). LNCS, vol 3253. Springer, Berlin, pp 309–324 CrossRef
13.
Berrang P, Bogdoll J, Hahn EM, Hartmanns A, Hermanns H (2012) Dependability results for power grids with decentralized stabilization strategies. Reports of SFB/TR 14 AVACS 83, SFB/TR 14 AVACS, ISSN: 1860-9821. www.​avacs.​org
14.
Blom H, Lygeros J (2006) Stochastic hybrid systems: theory and safety critical applications. Lecture notes in control and information sciences, vol 337. Springer, Berlin CrossRef
15.
Bogdoll J, David A, Hartmanns A, Hermanns H (2012) mctau: bridging the gap between Modest and UPPAAL. In: Model checking software—19th international workshop, SPIN 2012, Oxford, UK, July 23–24. LNCS, vol 7385. Springer, Berlin. ISBN 978-3-642-31758-3 CrossRef
16.
Bogdoll J, Fioriti LMF, Hartmanns A, Hermanns H (2011) Partial order methods for statistical model checking and simulation. In: Formal techniques for distributed systems (FMOODS/FORTE). LNCS, vol 6722. Springer, Berlin, pp 59–74 CrossRef
17.
Bohnenkamp HC, D’Argenio PR, Hermanns H, Katoen JP (2006) MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812–830 CrossRef
18.
Bohnenkamp HC, Gorter J, Guidi J, Katoen JP (2005) Are you still there?—A lightweight algorithm to monitor node presence in self-configuring networks. In: Dependable systems and networks (DSN). IEEE Comput Soc, Los Alamitos, pp 704–709
19.
Brinksma E, Krilavicius T, Usenko YS (2005) A process-algebraic approach to hybrid systems. In: 16th IFAC world congress. IFAC, Laxenburg
20.
Bujorianu ML (2004) Extended stochastic hybrid systems and their reachability problem. In: Hybrid systems: computation and control (HSCC). LNCS, vol 2993. Springer, Berlin, pp 234–249 CrossRef
21.
Bujorianu ML, Lygeros J, Bujorianu MC (2005) Bisimulation for general stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). LNCS, vol 3414. Springer, Berlin, pp 198–214 CrossRef
22.
Clarke E, Fehnker A, Han Z, Krogh B, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 2619. Springer, Berlin, pp 192–207 CrossRef
23.
24.
Dang T, Maler O (1998) Reachability analysis via face lifting. In: Hybrid systems: computation and control (HSCC). LNCS, vol 1386. Springer, Berlin, pp 96–109 CrossRef
25.
D’Argenio PR, Wolovick N, Terraf PS, Celayes P (2009) Nondeterministic labeled Markov processes: bisimulations and logical characterization. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 11–20
26.
27.
28.
Edwards S, Lavagno L, Lee EA, Sangiovanni-Vincentelli A (1997) Design of embedded systems: formal models, validation, and synthesis. Proc IEEE 85(3):366–390 CrossRef
29.
Fränzle M, Hahn EM, Hermanns H, Wolovick N, Zhang L (2011) Measurability and safety verification for stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). ACM, New York, pp 43–52
30.
Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1(3–4):209–236
31.
Frehse G (2008) Phaver: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transf 10(3):263–279 MathSciNetCrossRef
32.
Frehse G, Guernic CL, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) Spaceex: scalable verification of hybrid systems. In: Computer-aided verification (CAV). LNCS, vol 6806. Springer, Berlin, pp 379–395 CrossRef
33.
Giry M (1982) A categorical approach to probability theory. In: Categorical aspects of topology and analysis. Springer, Berlin, pp 68–85 CrossRef
34.
Groß C, Hermanns H, Pulungan R (2007) Does clock precision influence Zigbee’s energy consumptions? In: Principles of distributed systems (OPODIS). LNCS, vol 4878. Springer, Berlin, pp 174–188 CrossRef
35.
Grosu R, Stauner T (2002) Modular and visual specification of hybrid systems: an introduction to HyCharts. Form Methods Syst Des 21(1):5–38 CrossRefMATH
36.
Hartmanns A (2010) Model-checking and simulation for stochastic timed systems. In: FMCO. LNCS, vol 6957. Springer, Berlin, pp 372–391
37.
Hartmanns A, Hermanns H (2009) A Modest approach to checking probabilistic timed automata. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 187–196
38.
Henzinger TA (1996) The theory of hybrid automata. In: IEEE symp on logic in computer science (LICS), pp 278–292
39.
Henzinger TA, Ho PH, Wong-Toi H (1997) HYTECH: a model checker for hybrid systems. Int J Softw Tools Technol Transf 1(1–2):110–122 CrossRefMATH
40.
Herde C, Eggers A, Fränzle M, Teige T (2008) Analysis of hybrid systems using HySAT. In: International conference on systems (ICONS). IEEE Comput Soc, Los Alamitos, pp 196–201 CrossRef
41.
42.
Hillston J (1994) A compositional approach to performance modelling. PhD thesis, Univ of Edinburgh
43.
Hu J, Lygeros J, Sastry S (2000) Towards a theory of stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). LNCS, vol 1790. Springer, Berlin, pp 160–173 CrossRef
44.
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification (CAV’11). LNCS, vol 6806. Springer, Berlin, pp 585–591 CrossRef
45.
Kwiatkowska M, Norman G, Segala R, Sproston J (2000) Verifying quantitative properties of continuous probabilistic timed automata. In: Concurrency theory (CONCUR’00). LNCS, vol 1877. Springer, Berlin, pp 123–137
46.
Kwiatkowska MZ, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282(1):101–150 MathSciNetCrossRefMATH
47.
Lee EA (2002) Embedded software. In: Zelkowitz M (ed) Advances in computers, vol 56. Academic Press, San Diego
48.
Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: Runtime verification (RV). LNCS, vol 6418. Springer, Berlin, pp 122–135 CrossRef
49.
50.
Mader A, Bohnenkamp HC, Usenko YS, Jansen DN, Hurink J, Hermanns H (2010) Synthesis and stochastic assessment of cost-optimal schedules. Int J Softw Tools Technol Transf 12(5):305–318 CrossRef
51.
Meseguer J, Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). LNCS, vol 3927. Springer, Berlin, pp 460–475 CrossRef
52.
Panangaden P (2008) Labelled Markov processes. World Scientific, Singapore
53.
Penna GD, Intrigila B, Melatti I, Tronci E, Zilli MV (2006) Finite horizon analysis of Markov chains with the Murphy verifier. Int J Softw Tools Technol Transf 8(4–5):397–409 CrossRef
54.
Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: Bjørner N, Sofronie-Stokkermans V (eds) CADE. LNCS, vol 6803. Springer, Berlin, pp 446–460
55.
Preußig J, Kowalewski S, Wong-Toi H, Henzinger T (1998) An algorithm for the approximative analysis of rectangular automata. In: Formal techniques in fault tolerant and real time systems (FTRTFT). LNCS, vol 1486. Springer, Berlin, pp 228–240 CrossRef
56.
Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8 CrossRef
57.
Segala R (1995) Modelling and verification of randomized distributed real-time systems. PhD thesis, MIT, Cambridge, MA, USA
58.
Segala R, Lynch NA (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2):250–273 MathSciNetMATH
59.
Sproston J (2000) Decidable model checking of probabilistic hybrid automata. In: Formal techniques in real-time and fault-tolerant systems (FTRTFT). LNCS, vol 1926. Springer, Berlin, pp 31–45 CrossRef
60.
Strubbe S, van der Schaft A (2006) Compositional modelling of stochastic hybrid systems. In: Cassandras CG, Lygeros J (eds) Stochastic hybrid systems. Control engineering series. Taylor & Francis, London, pp 47–77 CrossRef
61.
Wolovick N (2012) Continuous probability and nondeterminism in labeled transition systems. PhD thesis, FaMAF, UNC, Córdoba, Argentina
62.
Yue H, Bohnenkamp HC, Kampschulte M, Katoen JP (2011) Analysing and improving energy efficiency of distributed slotted aloha. In: Smart spaces and next generation wired/wireless networking (NEW2AN). LNCS, vol 6869. Springer, Berlin, pp 197–208 CrossRef
63.
Zhang L, She Z, Ratschan S, Hermanns H, Hahn E (2010) Safety verification for probabilistic hybrid systems. In: Computer aided verification. LNCS, vol 6174. Springer, Berlin, pp 196–211 CrossRef
Metadaten
Titel
A compositional modelling and analysis framework for stochastic hybrid systems
verfasst von
Ernst Moritz Hahn
Arnd Hartmanns
Holger Hermanns
Joost-Pieter Katoen
Publikationsdatum
01.10.2013
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 2/2013
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0167-z

Weitere Artikel der Ausgabe 2/2013

Formal Methods in System Design 2/2013 Zur Ausgabe

OriginalPaper

Algorithmic probabilistic game semantics

OriginalPaper

Analyzing probabilistic pushdown automata

OriginalPaper

On-the-fly verification and optimization of DTA-properties for large Markov chains

EditorialNotes

Preface to the special issue on Probabilistic Model Checking

OriginalPaper

A survey of partial-observation stochastic parity games

OriginalPaper

Model checking for probabilistic timed automata