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
Erschienen in:
Exploring an Interface Model for CKA Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

On Rely-Guarantee Reasoning

verfasst von : Stephan van Staden

Erschienen in: Mathematics of Program Construction

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Many semantic models of rely-guarantee have been proposed in the literature. This paper proposes a new classification of the approaches into two groups based on their treatment of guarantee conditions. To allow a meaningful comparison, it constructs an abstract model for each group in a unified setting. The first model uses a weaker judgement and supports more general rules for atomic commands and disjunction. However, the stronger judgement of the second model permits the elegant separation of the rely from the guarantee due to Hayes et al. and allows refinement-style reasoning. The generalisation to models that use binary relations for postconditions is also investigated. An operational semantics is derived and both models are shown to be sound with respect to execution. All proofs have been checked with Isabelle/HOL and are available online.

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 Exploring an Interface Model for CKA
Nächstes Kapitel A Relation-Algebraic Approach to Multirelations and Predicate Transformers
Fußnoten
1
The prefix ‘J’ in the names of inference rules stands for ‘Jones’ in tribute to [8].
 
2
Note the Galois connection \({ steps ({P})} \subseteq G \Leftrightarrow P \subseteq { traces ({G})}\).
 
3
Because of the equivalence \({{S}\{P\}{S^\prime }} \Leftrightarrow {{S}\{P\}{S\!\!\times \!\!S^\prime }}\), it is also possible to go in the opposite direction, i.e., one can define the usual triple in terms of the triple where postconditions are relations.
 
4
The prefix ‘R’ in the names of inference rules stands for ‘relation’.
 
5
When postconditions are sets of states, one can always change a precondition \(S\) into \({R}^*(S)\) where \(R\) is the rely condition. This is invalid when postconditions are relations between input and output states, so (Rstren) does not change the precondition.
 
6
The prefix ‘P’ in the names of inference rules stands for ‘Plotkin’ in tribute to [12].
 
Literatur
1.
Armstrong, A., Gomes, V.B.F., Struth, G.: Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 78–93. Springer, Heidelberg (2014) CrossRef
2.
Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely/guarantee rules. J. Log. Comput. 17(4), 807–841 (2007). Comments refer to the revised version which appeared as technical report CS-TR-1029, University of Newcastle, June 2007MathSciNetCrossRefMATH
3.
Dingel, J.: A refinement calculus for shared-variable parallel and distributed programming. Formal Asp. Comput. 14(2), 123–197 (2002)CrossRefMATH
4.
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 287–300. ACM, New York (2013)
5.
Hayes, I.J., Jones, C.B., Colvin, R.J.: Refining rely-guarantee thinking. Technical report CS-TR-1334, School of Computing Science, Newcastle University, May 2012
6.
Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene Algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009) CrossRef
7.
8.
Jones, C.B.: Development Methods for Computer Programs including a Notion of Interference. Ph.D. thesis, Oxford University, June 1981. printed as: Programming Research Group, Technical Monograph 25
9.
Jones, C.B., Hayes, I.J., Colvin, Rj: Balancing expressiveness in formal approaches to concurrency. Formal Aspects Comput. 27(3), 475–497 (2015)MathSciNetCrossRefMATH
10.
Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. 10, 403–419 (1988)CrossRefMATH
11.
Prensa Nieto, L.: The rely-guarantee method in Isabelle/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348–362. Springer, Heidelberg (2003) CrossRef
12.
Plotkin, G.D.: A structural approach to operational semantics. Technical report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981
13.
de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, Cambridge (2001) MATH
14.
van Staden, S.: Constructing the views framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 62–83. Springer, Heidelberg (2015)
15.
Stirling, C.: A generalization of Owicki-Gries’s Hoare logic for a concurrent while language. Theor. Comput. Sci. 58, 347–359 (1988)MathSciNetCrossRefMATH
16.
Vafeiadis, V.: Modular fine-grained concurrency verification. Technical report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory, July 2008
17.
Wickerson, J., Dodds, M., Parkinson, M.: Explicit stabilisation for modular rely-guarantee reasoning. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 610–629. Springer, Heidelberg (2010) CrossRef
18.
Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2), 149–174 (1997)CrossRefMATH
Metadaten
Titel
On Rely-Guarantee Reasoning
verfasst von
Stephan van Staden
Copyright-Jahr
2015
Verlag
Springer International Publishing
Buch
Mathematics of Program Construction

Print ISBN: 978-3-319-19796-8

Electronic ISBN: 978-3-319-19797-5

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-19797-5_2

Premium Partner

    Bildnachweise