Specification in B an introduction using the B toolkit /
This book gives a practical introduction to the B specification language and method, an approach to the development of high-quality software using rigorous CASE techniques. It is suitable for both undergraduate and postgraduate courses, in addition to being an introduction for industrial practitione...
| Основен автор: | Lano, K. |
|---|---|
| Други автори: | Haughton, H. |
| Формат: | Електронен |
| Език: | English |
| Публикувано: |
London : Singapore ; River Edge, NJ :
Imperial College Press ; Distributed by World Scientific Pub.,
℗♭1996.
|
| Предмети: | |
| Онлайн достъп: |
http://search.ebscohost.com/login.aspx?direct=true&scope=site&db=nlebk&AN=491518 |
| Подобни документи: |
Print version::
Specification in B. |
Съдържание:
- 1. Abstract machines. 1.1. Software development lifecycles. 1.2. Specification using abstract machines. 1.3. Semantics of abstract machines. 1.4. Internal consistency. 1.5. Animation. 1.6. Exercises 1
- 2. Constructing specifications. 2.1. Machine composition mechanisms. 2.2. Structuring mechanisms and proof. 2.3. Translation of analysis models. 2.4. Renaming. 2.5. Exercises 2
- 3. Design and refinement. 3.1. The layered development paradigm. 3.2. Refinement. 3.3. Implementation. 3.4. System construction. 3.5. Implementation example
- Vending machines. 3.6. Exercises 3
- 4. Proof. 4.1. The B tool. 4.2. Proof of internal consistency obligations. 4.3. Proof listings. 4.4. Animation. 4.5. Refinement proof. 4.6. Refinement proof example
- Vending system. 4.7. Exercises 4
- 5. Implementation. 5.1. Prototype generation. 5.2. Implementing complex data. 5.3. Base generation. 5.4. Coding and integration. 5.5. Exercises 5
- 6. Case studies. 6.1. Real-time communication protocol. 6.2. Dependability evaluation of B AMN developments. 6.3. Case study: Radar track-former system. 6.4. Safety analysis techniques for B. 6.5. Timing analysis of B AMN specifications. 6.6. Conclusions.