Skip to main content
SpringerLink
Log in
Book cover

Models, Algorithms, Logics and Tools pp 125–145Cite as

Property-Preserving Parallel Decomposition

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10460))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    What we mean here is that M can be conveniently model checked with state-of-the-art technology.

  2. 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. 3.

    The following sketch omits some details which are however elaborated on in the corresponding sections of this paper.

  4. 4.

    This definition depends on the fact that each must transition is also a may transition.

  5. 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. 6.

    Such a conflict can easily be detected via the determinization of the may automaton of I.

  7. 7.

    Note that within this example, \(I_1\) is also a \(\phi \)-sensitive decomposition for all \(\phi \in \varPhi \).

  8. 8.

    This definition again depends on the fact that each must transition is also a may transition.

  9. 9.

    This definition is similar to the notion of cut points in Floyd’s inductive assertion method.

References

  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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  11. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40, 110–121 (2005)

    Article  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  13. Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). doi:10.1007/3-540-60761-7

    MATH  Google Scholar 

  14. Graf, S., Steffen, B.: Compositional minimization of finite state processes. Comput.-Aided Verification 90, 57–73 (1990)

    MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  16. Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 843–871 (1994)

    Article  Google Scholar 

  17. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not. 37(1), 58–70 (2002)

    Article  MATH  Google Scholar 

  18. Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, Heidelberg (1978). doi:10.1007/978-1-4757-3472-0_16

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  24. Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer Science & Business Media, Berlin (2012). doi:10.1007/978-3-642-27919-5

    Book  MATH  Google Scholar 

  25. Křetínskỳ, J.: Modal transition systems: extensions and analysis. Ph.D. thesis, Masarykova univerzita, Fakulta informatiky (2014)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  28. Larsen, K.G., Thomsen, B.: Partial specifications and compositional verification. Theoret. Comput. Sci. 88(1), 15–32 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  29. Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). doi:10.1007/3-540-52148-8_19

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  32. Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. Computer 43(6), 90–92 (2010)

    Article  Google Scholar 

  33. Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_34

    Chapter  Google Scholar 

  34. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)

    Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  37. Steffen, B., Ingólfsdóttir, A.: Characteristic formulas for processes with divergence. Inf. Comput. 110(1), 149–163 (1994)

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  40. Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991). doi:10.1007/3-540-53863-1_36

    Chapter  Google Scholar 

  41. Wei, O., Gurfinkel, A., Chechik, M.: Mixed transition systems revisited. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 349–365. Springer, Heidelberg (2008). doi:10.1007/978-3-540-93900-9_28

    Chapter  Google Scholar 

Download references

Acknowledgement

We are very grateful to Axel Legay and Maximilian Fecke for their suggestions and remarks regarding this paper.

Author information

Authors and Affiliations

  1. TU Dortmund University, 44221, Dortmund, Germany

    Bernhard Steffen & Marc Jasper

Authors
  1. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marc Jasper
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bernhard Steffen .

Editor information

Editors and Affiliations

  1. Reykjavik University, Reykjavik, Iceland

    Luca Aceto

  2. Aalborg University, Aalborg, Denmark

    Giorgio Bacci

  3. Aalborg University, Aalborg, Denmark

    Giovanni Bacci

  4. Reykjavík University, Reykjavik, Iceland

    Anna Ingólfsdóttir

  5. Inria Campus Beaulieu, Rennes, France

    Axel Legay

  6. Aalborg University, Aalborg, Denmark

    Radu Mardare

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Steffen, B., Jasper, M. (2017). Property-Preserving Parallel Decomposition. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds) Models, Algorithms, Logics and Tools. Lecture Notes in Computer Science(), vol 10460. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_7

Download citation

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

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-63121-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation