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
Erschienen in:
Information Flow for Timed Automata Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Property-Preserving Parallel Decomposition

verfasst von : Bernhard Steffen, Marc Jasper

Erschienen in: Models, Algorithms, Logics and Tools

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We propose a systematic approach to generate highly parallel benchmark systems with guaranteed temporal properties. Key to our approach is the iterative property-preserving parallel decomposition of an initial Modal Transition System, which is based on lightweight assumption commitment. Property preservation is guaranteed on the basis of Modal Contracts that permit a refinement into a component and its context while supporting the chaining of dependencies that are vital for the validity of considered properties. We illustrate our approach, which can be regarded as a simplicity-oriented variant of correctness by construction, by means of an accompanying example.

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
Vorheriges Kapitel Bicategories of Markov Processes
Nächstes Kapitel A Generic Algorithm for Learning Symbolic Automata from Membership Queries
Fußnoten
1
What we mean here is that M can be conveniently model checked with state-of-the-art technology.
 
2
Our exposition focuses on the preservation of validity. It should be noted that our MTS-based approach also maintains the existence of counterexamples, which is something different for linear time temporal formulas.
 
3
The following sketch omits some details which are however elaborated on in the corresponding sections of this paper.
 
4
This definition depends on the fact that each must transition is also a may transition.
 
5
As stated in Sect. 1, we focus on a parallel composition M of MTSs because a later refinement can yield a concrete implementation (see Fig. 1).
 
6
Such a conflict can easily be detected via the determinization of the may automaton of I.
 
7
Note that within this example, \(I_1\) is also a \(\phi \)-sensitive decomposition for all \(\phi \in \varPhi \).
 
8
This definition again depends on the fact that each must transition is also a may transition.
 
9
This definition is similar to the notion of cut points in Floyd’s inductive assertion method.
 
Literatur
1.
Bauer, S.S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., Wąsowski, A.: Moving from specifications to contracts in component-based design. In: Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43–58. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28872-2_​3 CrossRef
2.
Bauer, S.S., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: A modal specification theory for components with data. Sci. Comput. Program. 83, 106–128 (2014)CrossRef
3.
Beneš, N., Delahaye, B., Fahrenberg, U., Křetínský, J., Legay, A.: Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 76–90. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40184-8_​7 CrossRef
4.
Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275–289. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-24372-1_​20 CrossRef
5.
Benveniste, A., Caillaud, B.: Synchronous interfaces and assume/guarantee contracts. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Larsen Festschrift. LNCS, vol. 10460, pp. 233–248. Springer, Cham (2017)
6.
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.​1007/​10722167_​15 CrossRef
7.
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.​1007/​BFb0025774 CrossRef
8.
Cleaveland, R., Steffen, B.: A preorder for partial process specifications. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 141–151. Springer, Heidelberg (1990). doi:10.​1007/​BFb0039057 CrossRef
9.
Fahrenberg, U., Legay, A.: A linear-time–branching-time spectrum of behavioral specification theories. In: Steffen, B., Baier, C., Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds.) SOFSEM 2017. LNCS, vol. 10139, pp. 49–61. Springer, Cham (2017). doi:10.​1007/​978-3-319-51963-0_​5 CrossRef
10.
Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebraic Program. 77(1–2), 20–39 (2008)MathSciNetCrossRefMATH
11.
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40, 110–121 (2005)CrossRefMATH
12.
Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 787–803. Springer, Cham (2016). doi:10.​1007/​978-3-319-47169-3_​59 CrossRef
13.
14.
Graf, S., Steffen, B.: Compositional minimization of finite state processes. Comput.-Aided Verification 90, 57–73 (1990)MATH
15.
Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Form. Asp. Comput. 8(5), 607–616 (1996)CrossRefMATH
16.
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 843–871 (1994)CrossRef
17.
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not. 37(1), 58–70 (2002)CrossRefMATH
18.
19.
Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 608–614. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-34026-0_​45 CrossRef
20.
Hüttel, H., Larsen, K.G.: The use of static constructs in a model process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163–180. Springer, Heidelberg (1989). doi:10.​1007/​3-540-51237-3_​14 CrossRef
21.
Jonsson, B., Larsen, K.G.: On the complexity of equation solving in process algebra. In: Abramsky, S., Maibaum, T.S.E. (eds.) CAAP 1991. LNCS, vol. 493, pp. 381–396. Springer, Heidelberg (1991). doi:10.​1007/​3-540-53982-4_​21 CrossRef
22.
Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A.,Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Tri.nh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http://​mcc.​lip6.​fr/​2016/​results.​php
23.
Kordon, F., et al.: Report on the model checking contest at petri nets 2011. In: Jensen, K., Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169–196. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-35179-2_​8 CrossRef
24.
25.
Křetínskỳ, J.: Modal transition systems: extensions and analysis. Ph.D. thesis, Masarykova univerzita, Fakulta informatiky (2014)
26.
Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition systems. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 17–40. Springer, Heidelberg (1995). doi:10.​1007/​3-540-60630-0_​2 CrossRef
27.
Larsen, K.G., Steffen, B., Weise, C.: The methodology of modal constraints. In: Broy, M., Merz, S., Spies, K. (eds.) Formal Systems Specification. LNCS, vol. 1169, pp. 405–435. Springer, Heidelberg (1996). doi:10.​1007/​BFb0024437 CrossRef
28.
Larsen, K.G., Thomsen, B.: Partial specifications and compositional verification. Theoret. Comput. Sci. 88(1), 15–32 (1991)MathSciNetCrossRefMATH
29.
30.
Guldstrand Larsen, K.: Ideal specification formalism = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33–56. Springer, Heidelberg (1990). doi:10.​1007/​BFb0039050 CrossRef
31.
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 108–117. IEEE (1990)
32.
Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. Computer 43(6), 90–92 (2010)CrossRef
33.
34.
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)
35.
Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundamenta Informaticae 108(1–2), 119–149 (2011)MathSciNetMATH
36.
Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 723–732. Springer, Heidelberg (1989). doi:10.​1007/​BFb0035794 CrossRef
37.
Steffen, B., Ingólfsdóttir, A.: Characteristic formulas for processes with divergence. Inf. Comput. 110(1), 149–163 (1994)CrossRefMATH
38.
Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer 16(5), 465–479 (2014)CrossRef
39.
Steffen, B., Jasper, M., van de Pol, J., Meijer, J.: Property-preserving generation of tailored benchmark petri nets. In: Proceedings of ACSD 2017. IEEE Computer Society (2017, to appear)
40.
41.
Metadaten
Titel
Property-Preserving Parallel Decomposition
verfasst von
Bernhard Steffen
Marc Jasper
Copyright-Jahr
2017
Buch
Models, Algorithms, Logics and Tools

Print ISBN: 978-3-319-63120-2

Electronic ISBN: 978-3-319-63121-9

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63121-9_7