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
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2015

01.04.2015 | AD-RV

Statistical model checking QoS properties of systems with SBIP

verfasst von: Ayoub Nouri, Saddek Bensalem, Marius Bozga, Benoit Delahaye, Cyrille Jegourel, Axel Legay

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2015

Einloggen

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

search-config
loading …

Abstract

Behavior–interaction–priority (BIP) is a component-based framework supporting rigorous design of embedded systems. BIP supports incremental design of large systems from atomic components that communicate via connectors and whose interactions can be described with a powerful algebra. This paper presents SBIP, an extension of BIP for stochastic systems. SBIP offers the possibility to add stochastic information to atomic component’s behaviors, and hence to the entire system. Atomic component’s semantics in SBIP is described by Markov Chains. We show that the semantics of the entire system is described by a Markov chain, showing that the non-determinism arising from system interactions is automatically eliminated by BIP. This allows us to verify systems described in SBIP with Statistical Model Checking. This paper introduces SBIP and illustrates its usability on several industrial case studies.
Vorheriger Artikel Rule-based runtime verification revisited
Nächster Artikel Schedulability of Herschel revisited using statistical 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 "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
Literatur
1.
Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: FORTE, vol 6117 of LNCS, pp. 32–46. Springer, Berlin (2010)
2.
Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an afdx infrastructure using simulations and probabilities. In: Proceedings of the First international conference on Runtime verification, RV’10, pp. 330–344. Springer-Verlag, Berlin, Heidelberg (2010)
3.
Basu, A., Bensalem, S., Gallien, M., Ingrand, F., Lesire, C., Nguyen, T.-H., Sifakis, J.: Incremental component-based construction and verification of a robotic system, In: ECAI (2008)
4.
Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: SEFM06, pp. 3–12, Sep (2006)
5.
Bensalem, S., Bozga, M., Delahaye, B., Jégourel, C., Legay, A., Nouri, A.: Statistical model checking qos properties of systems with sbip. ISoLA 1, 327–341 (2012)
6.
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-finder: A tool for compositional deadlock detection and verification. In: Proceedings of the 21st International Conference on Computer Aided Verification, CAV ’09, pp. 614–619. Springer-Verlag, Berlin, Heidelberg (2009)
7.
Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: Present and future. In: RV, vol. 6418 of LNCS. Springer, Berlin (2010)
8.
Bensalem, S., Legay, A., Nouri, A., Peled, D.: Synthesizing distributed scheduling implementation for probabilistic component-based systems. In: MEMOCODE, pp. 87–96 (2013)
9.
Bensalem, S., Silva, L., Griesmayer, A., Ingrand, F., Legay, A., Yan, R.: A formal approach for incremental construction with an application to autonomous robotic systems. In: SC’11, LNCS. Springer, Berlin (2011)
10.
11.
12.
Bliudze, S., Sifakis, J.: The algebra of connectors-structuring interaction in bip. IEEE Trans. Comput. 57(10), 1315–1330 (2008)
13.
Bogdoll, J., Fiorti, L.-M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: FORTE, LNCS. Springer, Berlin (2011)
14.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
15.
Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems. In: SEFM, pp. 204–220 (2011)
16.
Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101–127 (2004)CrossRefMATH
17.
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer Aided Verification (CAV’01). Lecture Notes in Computer Science, vol. 2102, pp. 53–65. Springer, Paris (2001)
18.
Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, ASE ’01, pp. 412. IEEE Computer Society, Washington, DC (2001)
19.
Grosu, R., Smolka, S.A.: Monte carlo model checking. In: TACAS, vol. 3440 of LNCS, pp. 271–286. Springer, Berlin (2005)
20.
Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: TACAS, LNCS, pp. 342–356. Springer, Berlin (2002)
21.
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI, pp. 73–84 (2004)
22.
23.
Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: HVC, vol. 4899 of LNCS. Springer, Berlin (2007)
24.
Jégourel, C., Legay, A., Sedwards, S.: Cross entropy optimisation of importance sampling parameters for statistical model checking. In: CAV (2012)
25.
Jégourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking-plasma. In: TACAS, LNCS, pp. 498–503. Springer, Berlin (2012)
26.
Katoen, J.-P., Zapreev, I.S.: Simulation-based ctmc model checking: an empirical evaluation. In: QEST, pp. 31–40. IEEE Computer Society, Washington, DC (2009)
27.
Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker mrmc. In: QEST, pp. 167–176. IEEE Computer Society, Washington, DC (2009)
28.
Krunz, M., Sass, R., Hughes, H.: Statistical characteristics and multiplexing of MPEG streams. In: INFOCOM, pp. 455–462 (1995)
29.
Krunz, M., Tripathi, S.K.: On the characterization of VBR MPEG streams. In: SIGMETRICS, pp. 192–202 (1997)
30.
Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322–323. IEEE (2004)
31.
Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: an approach based on property testing. ACM TCS 8(4), 20 (2007)CrossRef
32.
Legay, A., Delahaye, B.: Statistical model checking: an overview. CoRR, abs/1005.1327 (2010)
33.
Nouri, A., Legay, A., Bensalem, S., Bozga, M.: Sbip: a statistical model checking extension for the bip framework. In: First Workshop on Statistical Model Checking (2013)
34.
Parzen, E.: Stochastic Processes. Holden Day, Australia (1962)MATH
35.
Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: ATVA, vol. 5799 of LNCS, pp. 120–134. Springer, Berlin (2009)
36.
Raman, B., Nouri, A., Gangadharan, D., Bozga, M., Basu, A., Maheshwari, M., Legay, A., Bensalem, S., Chakraborty, S.: Stochastic modeling and performance analysis of multimedia socs. In: ICSAMOS, pp. 145–154 (2013)
37.
Rosu, G., Bensalem, S.: Allen linear (interval) temporal logic: translation to ltl and monitor synthesis. In: CAV, vol. 4144 of LNCS, pp. 263–277. Springer, Berlin (2006)
38.
Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV, LNCS 3114, pp. 202–215. Springer, Berlin (2004)
39.
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: CAV, pp. 266–280 (2005)
40.
Vardi, M.Y.: Alternating automata and program verification. In: In Computer Science Today. LNCS 1000, pp. 471–485. Springer-Verlag, Berlin (1995)
41.
42.
Wijesekera, D., Srivastava, J.: Quality of service (QoS) metrics for continuous media. Multimedia Tools Appl. 3(2), 127–166 (1996)CrossRef
43.
Wolper, P.: Lectures on formal methods and performance analysis. Chapter Constructing automata from temporal logic formulas: a tutorial, pp. 261–277. Springer-Verlag New York Inc, New York (2002)
44.
Ylies, F., Mohamad, J., Thanh-Hung, N., Marius, B., Saddek, B.: Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation. SOSYM, pp. 1–27 (2013)
45.
Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D thesis, Carnegie Mellon (2005)
46.
Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: SBMF, pp. 144–160 (2010)
47.
Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: HSCC, pp. 217–226. ACM (2012)
48.
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC, pp. 243–252. ACM (2010)
Metadaten
Titel
Statistical model checking QoS properties of systems with SBIP
verfasst von
Ayoub Nouri
Saddek Bensalem
Marius Bozga
Benoit Delahaye
Cyrille Jegourel
Axel Legay
Publikationsdatum
01.04.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2015
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0313-6

Weitere Artikel der Ausgabe 2/2015

International Journal on Software Tools for Technology Transfer 2/2015 Zur Ausgabe

AD-RV

Schedulability of Herschel revisited using statistical model checking

Regular Paper

APSET, an Android aPplication SEcurity Testing tool for detecting intent-based vulnerabilities

AD-RV

Rule-based runtime verification revisited

Introduction

Runtime verification: the application perspective

Regular Paper

Model-checking fair dense-time systems with propositions and events

AD-RV

On piggyback runtime monitoring of object-oriented programs