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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 2/2012

01.10.2012

Probabilistic contracts for component-based design

verfasst von: Gregor Gössler, Dana N. Xu, Alain Girault

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

Einloggen

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

search-config
loading …

Abstract

We define a framework of probabilistic contracts for constructing component-based embedded systems, based on the formalism of discrete-time Interactive Markov Chains. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Probabilistic transitions represent allowed uncertainty in the component behavior, for instance, to model internal choice or reliability. Action transitions are used to model non-deterministic behavior and communication between components. An interaction model specifies how components interact with each other.
We provide the ingredients for a component-based design flow, including (1) contract satisfaction and refinement, (2) parallel composition of contracts over disjoint, interacting components, and (3) conjunction of contracts describing different requirements over the same component. Compositional design is enabled by congruence of refinement.
Vorheriger Artikel A formal hierarchy of weak memory models

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
Literatur
1.
Aho AV, Sethi R, Ullman JD (1986) Compilers—principles, techniques, and tools. Addison-Wesley, Reading
2.
Caillaud B, Delahaye B, Larsen KG, Legay A, Pedersen ML, Wasowski A (2010) Compositional design methodology with constraint Markov chains. In: International conference on the quantitative evaluation of systems, QEST’10, pp 123–132
3.
de Alfaro L, Henzinger TA, Jhala R (2001) Compositional methods for probabilistic systems. In: Larsen KG, Nielsen M (eds) Proc CONCUR 2001—concurrency theory, 12th international conference. LNCS, vol 2154. Springer, Berlin, pp 351–365
4.
Delahaye B, Caillaud B, Legay A (2011) Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects. Form Methods Syst Des 38(1):1–32 MATHCrossRef
5.
Doyen L, Petrov T, Henzinger TA, Jobstmann B (2008) Interface theories with component reuse. In: International conference on embedded software, EMSOFT’08. ACM, New York, pp 79–88
6.
Fecher H, Leucker M, Wolf V (2006) Don’t know in probabilistic systems. In: International workshop on model checking software, SPIN’06. LNCS, vol 3925. Springer, Berlin, pp 71–88 CrossRef
7.
Gössler G, Raclet J-B (2009) Modal contracts for component-based design. In: International conference on software engineering and formal methods, SEFM’09. IEEE, New York, pp 295–303
8.
Gössler G, Sifakis J (2005) Composition for component-based modeling. Sci Comput Program 55(1–3):161–183 MATHCrossRef
9.
Gössler G, Xu DN, Girault A (2012) Probabilistic contracts for component-based design. Research report 7328, INRIA
10.
Hermanns H (2002) Interactive Markov chains: the quest for quantified quality. LNCS, vol 2428. Springer, Berlin MATHCrossRef
11.
Jonsson B, Larsen KG (1991) Specification and refinement of probabilistic processes. In: Symposium on logic in computer science, LICS’91. IEEE Computer Society, Los Alamitos, pp 266–277
12.
Katoen J-P, Klink D, Neuhäußer MR (2009) Compositional abstraction for stochastic systems. In: International conference on formal modeling and analysis of timed systems, FORMATS’09. LNCS, vol 5813. Springer, Berlin, pp 195–211 CrossRef
13.
Kwiatkowska MZ, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: International conference on tools and algorithms for the construction and analysis of systems, TACAS’10. LNCS, vol 6015. Springer, Berlin, pp 23–37 CrossRef
14.
Meyer B (1991) Design by contract. In: Advances in object-oriented software engineering. Prentice Hall, New York, pp 1–50
15.
Morgan C, McIver A, Seidel K (1996) Probabilistic predicate transformers. ACM Trans Program Lang Syst 18(3):325–353 CrossRef
16.
Raclet J-B, Badouel E, Benveniste A, Caillaud B, Passerone R (2009) Why modalities are good for interface theories? In: International conference on application of concurrency to system design, ACSD’09. IEEE, New York, pp 119–127 CrossRef
17.
Xu DN, Gössler G, Girault A (2010) Probabilistic contracts for component-based design. In: International symposium on automated technology for verification and analysis, ATVA’10. LNCS, vol 6252. Springer, Berlin, pp 325–340 CrossRef
18.
Yi W (1994) Algebraic reasoning for real-time probabilistic processes with uncertain information. In: Third international symposium on formal techniques in real-time and fault-tolerant systems, FTRTFT’94. LNCS, vol 863. Springer, Berlin, pp 680–693 CrossRef
Metadaten
Titel
Probabilistic contracts for component-based design
verfasst von
Gregor Gössler
Dana N. Xu
Alain Girault
Publikationsdatum
01.10.2012
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 2/2012
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0162-4

Premium Partner

    Bildnachweise