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

1996 | Buch

Introduction Kapitel lesen Erstes Kapitel lesen

The B Language and Method

A Guide to Practical Formal Development

verfasst von: Kevin Lano, BSc, MSc, PhD

Verlag: Springer London

Buchreihe : Formal Approaches to Computing and Information Technology

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

B is one of the few formal methods which has robust, commercially-available tool support for the entire development lifecycle from specification through to code generation. This volume provides a comprehensive introduction to the B Abstract Machine Notation, and to how it can be used to support formal specification and development of high integrity systems. A strong emphasis is placed on the use of B in the context of existing software development methods, including object-oriented analysis and design. The text includes a large number of worked examples, graduated exercises in B AMN specification and development (all of which have been class-tested), two extended case studies of the development process, and an appendix of proof techniques suitable for B. Based on material which has been used to teach B at postgraduate and undergraduate level, this volume will provide invaluable reading a wide range of people, including students, project technical managers and workers, and researchers with an interest in methods integration and B semantics.

Inhaltsverzeichnis

Frontmatter
Chapter 1. Introduction
Abstract
The B Abstract Machine Notation specification language, originally developed in the early and mid 1980s by J.R. Abrial and by research groups at BP Research, MATRA and GEC Alsthom, is currently attracting increasing interest in both industry and academia. It is one of the few “formal methods” which has robust, commercially available tool support for the entire development lifecycle from specification through to code generation, and it also inherits the advantages of its predecessor, Z, in being based on familiar and well-understood mathematical foundations.
Kevin Lano
Chapter 2. The Foundations of B AMN
Abstract
In this chapter we will give a comprehensive description of the B AMN language, building up from the level of elementary mathematics and “generalised substitutions” (the means by which B AMN specifies state transformations) to the level of machines and the visibility relationships induced between machines by the structuring mechanisms (USES, INCLUDES, EXTENDS, etc.).
Kevin Lano
Chapter 3. Analysis and Specification
Abstract
In this chapter we will examine each of the life cycle stages of B AMN development from requirements analysis through to the creation of a complete specification. A number of case studies and examples are used to illustrate these stages and the choices that can be made in expressing the semantics of a system using B. We will emphasise a particular approach using translation from diagrammatic models to inspire the choice of features of the formal specification, however it is quite feasible to directly write formal specifications without prior analysis or such a translation process (people have been writing Z or VDM specifications this way for years). For complex systems a loss of quality is nevertheless likely to result from omitting analysis.
Kevin Lano
Chapter 4. Design and Implementation
Abstract
This chapter will cover the stages of development from a complete and validated specification through successive stages of refinement, involving design decisions about how certain specification elements should be expressed in a more code-oriented manner, until a stage is reached which corresponds to an immediately executable system. This process is a key advantage of B over earlier formal methods, particularly Z, which were designed mainly for use at the specification and requirements capture stages.
Kevin Lano
Chapter 5. Case Studies
Abstract
This chapter will provide three case studies in the B development method. The first gives an example of the refinement of entity-relationship-attribute models, the second is a standard reactive system example, and the third is a detailed development of the vending machine case study. The first is an example of the “monolithic” approach to implementation structuring, the second an example of “separate decomposition” and the third an example of “continuity of structure”.
Kevin Lano
Chapter 6. Conclusions
Abstract
At present, by far the largest use of formal methods in industry is in the specification of software components, rather than in later development stages. Further, when we take into consideration the lack of methodological support for refinement of such specifications it is clear that many “formal developments” are nothing more than “formally contrived developments”. The result is that implementations, quite often, behave in a manner that is non-congruent with respect to their specifications. This causes many problems for the users and eventual maintainers of such systems. The B method avoids these problems because it allows developers to develop systems in a rigorous/verifiable way.
Kevin Lano
Backmatter
Metadaten
Titel
The B Language and Method
verfasst von
Kevin Lano, BSc, MSc, PhD
Copyright-Jahr
1996
Verlag
Springer London
Electronic ISBN
978-1-4471-1494-9
Print ISBN
978-3-540-76033-7
DOI
https://doi.org/10.1007/978-1-4471-1494-9