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:
Labeled Transition Systems and Their Refinement Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

7. State-Based Languages: Z and B

verfasst von : John Derrick, Eerke Boiten

Erschienen in: Refinement

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

This chapter defines refinement in Z, and shows how it derives from the relational model in Chap. 4. It discusses the similarities and differences with refinement in B. The approach taken in a state-based specification language is very different in emphasis from that in a process algebra. Process algebras stress the interaction between independent components (processes), so that communication and concurrency are key. State is implicit in such a description. A different approach is taken by a state-based language which, as the name suggests, considers the specification of state as the primary focus in a description. In this chapter we illustrate the approach to state-based specification by briefly introducing the Z and B notations, and showing how we can apply our theory of refinement to them.

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 Process Algebra
Nächstes Kapitel State-Based Languages: Event-B and ASM
Literatur
1.
Smith G (2000) The Object-Z specification language. Kluwer Academic Publishers, BostonCrossRef
2.
Potter B, Sinclair J, Till D (1996) An introduction to formal specification and Z. International series in computer science, 2nd edn. Prentice Hall, New York (1991)
3.
Ratcliff B (1994) Introducing specification using Z: a practical case study approach. McGraw-Hill, London
4.
Bottaci L, Jones J (1995) Formal specification using Z: a modelling approach. International Thomson Publishing, London
5.
Bowen JP (1996) Formal specification and documentation using Z: a case study approach. International Thomson Computer Press, London
6.
Jacky J (1997) The way of Z: practical programming with formal methods. Cambridge University Press, Cambridge
7.
Hayes IJ (ed) (1987) Specification case studies. International series in computer science, 2nd edn. Prentice Hall, New York (1993)
8.
Spivey JM (1992) The Z notation: a reference manual. International series in computer science, 2nd edn. Prentice Hall, New York
9.
ISO/IEC (2002) International standard 13568:2002 Information technology – Z formal specification notation – Syntax, type system and semantics
10.
Spivey JM (1988) Understanding Z: a specification language and its formal semantics. Cambridge University Press, CambridgeMATH
11.
Barden R, Stepney S, Cooper D (1994) Z in practice. BCS practitioner series, Prentice Hall, New YorkMATH
12.
Woodcock JCP, Davies J (1996) Using Z: specification, refinement, and proof. Prentice Hall, New YorkMATH
13.
Derrick J, Smith G (2004) Linear temporal logic and Z refinement. In: Rattray C, Maharaj S, Shankland C (eds) AMAST. Lecture notes in computer science, vol 3116. Springer, Berlin, pp 117–131
14.
Derrick J, Smith G (2012) Temporal-logic property preservation under Z refinement. Form Asp Comput 24(3):393–416MathSciNetCrossRef
15.
Derrick J, Boiten EA (2014) Refinement in Z and Object-Z, 2nd edn. Springer, BerlinCrossRef
16.
Derrick J, Wehrheim H Using coupled simulations in non-atomic refinement. In: Bert et al [39], pp 127–147
17.
Derrick J, Wehrheim H Non-atomic refinement in Z and CSP. In: Treharne et al [40], pp 24–44
18.
19.
Derrick J, Boiten EA, Bowman H, Steen MWA Weak refinement in Z. In: Bert et al [39], pp 369–388
20.
Derrick J, Boiten EA, Bowman H, Steen MWA (1998) Specifying and refining internal operations in Z. Form Asp Comput 10:125–159CrossRef
21.
Derrick J, Wehrheim H (2007) On using data abstractions for model checking refinements. Acta Inf 44(1):41–71MathSciNetCrossRef
22.
Derrick J, North S, Simons T (2006) Issues in implementing a model checker for Z. In: Liu Z, He J (eds) ICFEM. Lecture notes in computer science, Springer, Berlin, pp 678–696
23.
Smith G, Derrick J (2006) Verifying data refinements using a model checker. Form Asp Comput 18(3):264–287CrossRef
24.
Smith G, Derrick J (2005) Model checking downward simulations. Electron Notes Theor Comput Sci 137(2):205–224CrossRef
25.
Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, New YorkCrossRef
26.
Schneider S (2001) The B-method: an introduction. Palgrave Macmillan, London
27.
Wordsworth JB (1996) Software engineering with B. Addison-Wesley, Longman Publishing Co., Inc., Boston
28.
Lano K (1996) The B language and method: a guide to practical formal development. FACIT series, Springer, BerlinCrossRef
29.
Sekerinski E, Sere K (eds) (1999) Program development by refinement - case studies using the B method. FACIT, Springer, BerlinMATH
30.
Abrial J-R, Mussat L (1997) Specification and design of a transmission protocol by successive refinements using B. In: Broy M, Schieder B (eds) Mathematical methods in program development. NATO ASI series F: computer and systems sciences, vol 158. Springer, Berlin, pp 129–200
31.
Nicholls JE (ed) (1990) Z user workshop, Oxford 1990. Workshops in computing, Springer, Berlin
32.
Bowen JP, Nicholls JE (eds) (1992) Seventh annual Z user workshop. Springer, London
33.
Bowen JP, Hall JA (eds) (1994) ZUM’94. Z user workshop. Workshops in computing, Springer, Cambridge
34.
Bowen JP, Hinchey MG (eds) (1995) ZUM’95: The Z formal specification notation. Lecture notes in computer science, vol 967. Springer, Limerick
35.
Bowen JP, Hinchey MG, Till D (eds) (1997) ZUM’97: The Z formal specification notation. Lecture notes in computer science, vol 1212. Springer, Berlin
36.
Bowen JP, Fett A, Hinchey MG (eds) (1998) ZUM’98: The Z formal specification notation. Lecture notes in computer science, vol 1493. Springer, Berlin
37.
Bowen JP, Dunne S, Galloway A, King S (eds) (2000) ZB2000: Formal specification and development in Z and B. Lecture notes in computer science, vol 1878. Springer, Berlin
38.
Bert D, Bowen JP, Henson MC, Robinson K (eds) (2002) ZB 2002: formal specification and development in Z and B, 2nd international conference of B and Z users. Lecture notes in computer science, vol 2272. Springer, Berlin
39.
Bert D, Bowen JP, King S, Waldén MA (eds) (2003) ZB 2003: formal specification and development in Z and B, third international conference of B and Z users. Lecture notes in computer science, vol 2651. Springer, Berlin
40.
Treharne H, King S, Henson MC, Schneider SA (eds) (2005) ZB 2005: formal specification and development in Z and B, 4th international conference of B and Z users, Guildford, UK, 13–15 April 2005, proceedings. Lecture notes in computer science, vol 3455. Springer, Berlin
41.
Börger E, Butler MJ, Bowen JP, Boca P (eds) (2008) ABZ 2008. Lecture notes in computer science, vol 5238. Springer, Berlin
42.
Frappier M, Glässer U, Khurshid S, Laleau R, Reeves S (eds) (2010) ABZ 2010. Lecture notes in computer science, vol 5977. Springer, Berlin
43.
Derrick J, Fitzgerald JA, Gnesi S, Khurshid S, Leuschel M, Reeves S, Riccobene E (eds) (2012) Abstract state machines, Alloy, B, VDM, and Z - third international conference, ABZ 2012. Lecture notes in computer science, vol 7316. Springer, Berlin
44.
Smith G (1997) A semantic integration of Object-Z and CSP for the specification of concurrent systems. In: Fitzgerald J, Jones CB, Lucas P (eds) FME’97: industrial application and strengthened foundations of formal methods. Lecture notes in computer science, vol 1313. Springer, Berlin, pp 62–81
45.
Smith G, Derrick J Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Hinchey and Liu [50], pp 293–302
46.
Smith G, Derrick J (2001) Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Form Methods Syst Des 18:249–284CrossRef
47.
Smith G, Derrick J, George C, Miao H (eds) (2002) Abstract specification in Object-Z and CSP. Formal methods and software engineering. Lecture notes in computer science, vol 2495. Springer, Berlin, pp 108–119
48.
Derrick J, Smith G (2003) Structural refinement of systems specified in Object-Z and CSP. Form Asp Comput 15(1):1–27CrossRef
49.
Butler M An approach to the design of distributed systems with B AMN. In: Bowen et al [35], pp 223–241
50.
Hinchey MG, Liu S (eds) (1997) First international conference on formal engineering methods (ICFEM’97). IEEE Computer Society Press, Hiroshima, Japan
Metadaten
Titel
State-Based Languages: Z and B
verfasst von
John Derrick
Eerke Boiten
Copyright-Jahr
2018
Buch
Refinement

Print ISBN: 978-3-319-92709-1

Electronic ISBN: 978-3-319-92711-4

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-319-92711-4_7