Modelling Systems: Practical Tools and Techniques in Software Development

, by John Fitzgerald , Peter Gorm Larsen

Note: Supplemental materials are not guaranteed with Rental or Used book purchases.

ISBN: 9780521899116 | 0521899117
Cover: Hardcover
Copyright: 7/27/2009

Rent

(Recommended)

$45.41

Term

Due

Price

Semester

Dec 13

$50.46

Quarter

Aug 19

$47.94

Short Term

Jul 26

$45.41

*This item is part of an exclusive publisher rental program and requires an additional convenience fee. This fee will be reflected in the shopping cart.
Buy New

Special Order: 1-2 Weeks

$68.94
eBook

Available Instantly

Online: 180 Days

Downloadable: 180 Days

$63.00

How can we make sure that the software we build does what it is supposed to? This book provides an insight into established techniques which help developers to overcome the complexity of software development by constructing models of software systems in early design stages. It uses one of the leading formal methods, VDM (Vienna Development Method), and combines training in the formalism with industry-strength tool support and examples derived from real industrial applications. The principles taught here also apply to many of the current generation of formal methods. This second edition has been updated to include advanced online tool support for formal modelling as well as up-to-date reports on real commercial applications in areas as diverse as business information systems and firmware design.

Foreword	p. ix
Preface	p. xi
Introduction	p. 1
Software	p. 1
Modelling and analysis	p. 2
This book	p. 3
VDM-SL	p. 4
The structure of a VDM-SL model	p. 4
Analysing a model	p. 9
Constructing a Model	p. 13
Introduction	p. 13
Requirements for an alarm system	p. 13
Constructing a model from scratch	p. 14
Reading the requirements	p. 15
Extracting possible types and functions	p. 16
Sketching type representations	p. 16
Sketching function signatures	p. 22
Completing the type definitions	p. 23
Completing the function definitions	p. 24
Reviewing requirements	p. 29
VDMTools Lite	p. 35
Introduction	p. 35
Installing VDMTools Lite	p. 36
Configuring the alarm example	p. 36
Syntax and type checking models	p. 38
Interpreting and debugging models	p. 42
Test coverage	p. 48
Integrity checking	p. 49
Setting options	p. 50
Describing System Properties Using Logical Expressions	p. 55
Introduction	p. 55
The temperature monitor	p. 55
Logical expressions	p. 57
Presenting and evaluating predicates	p. 64
Using quantifiers	p. 66
Coping with undefinedness	p. 71
The Elements of a Formal Model	p. 77
Introduction	p. 77
A traffic light control kernel	p. 78
Union and basic types	p. 81
Basic type constructors	p. 83
Record types	p. 84
Invariants	p. 85
Explicit function definitions	p. 87
Functions for changing signals	p. 88
Reviewing the safety requirements	p. 96
Optional types: modelling failure behaviour	p. 96
Sets	p. 99
Introduction	p. 99
The set type constructor	p. 100
Defining sets	p. 101
Modelling with sets	p. 103
Distributed set operators	p. 115
Summary	p. 118
Sequences	p. 121
Introduction	p. 121
The sequence type constructor	p. 122
Defining sequences	p. 122
Modelling with sequences	p. 125
Further operators on sequences	p. 132
Abstraction lesson: choosing abstraction levels	p. 135
Mappings	p. 137
Introduction	p. 137
The mapping type constructor	p. 139
Defining mappings	p. 139
Modelling with mappings	p. 140
Summary	p. 154
Recursive Structures	p. 157
Recursive data structures: trees	p. 157
Abstract syntax trees	p. 161
Directed graphs	p. 164
An application of directed graphs: code optimisation	p. 167
Abstraction lesson: executability	p. 169
Validating Models	p. 171
Introduction	p. 171
Internal consistency: proof obligations	p. 173
Visualisation of a model	p. 180
Interfacing to legacy code	p. 182
Systematic testing	p. 183
Using proofs	p. 184
Choosing a validation technique	p. 187
State-Based Modelling	p. 189
Introduction	p. 189
State-based modelling	p. 190
A state-based model of the explosives store controller	p. 191
A state-based model of the trusted gateway	p. 196
Validation of state-based models	p. 199
Large-Scale Modelling	p. 203
Introduction	p. 203
A structure for the tracker model	p. 204
Information hiding	p. 212
Object-oriented structuring	p. 214
Using VDM in Practice	p. 217
Introduction	p. 217
Development activities and processes	p. 218
Common development problems	p. 219
Advantages of VDM technology	p. 220
Getting started	p. 223
VDM and its extensions	p. 226
Industrial applications of VDM	p. 227
Moving on: information resources	p. 232
Language Guide	p. 235
Identifiers	p. 235
Type definitions	p. 236
Basic data types and type constructors	p. 236
Data type operator overview	p. 237
Expressions	p. 246
Patterns	p. 248
Bindings	p. 249
Explicit function definition	p. 249
Implicit functions	p. 250
Operations	p. 250
The state definition	p. 251
Syntax overview	p. 252
Solutions to Exercises	p. 263
Solutions for Chapter 2 Exercises	p. 263
Solutions for Chapter 3 Exercises	p. 263
Solutions for Chapter 4 Exercises	p. 264
Solutions for Chapter 5 Exercises	p. 265
Solutions for Chapter 6 Exercises	p. 266
Solutions for Chapter 7 Exercises	p. 268
Solutions for Chapter 8 Exercises	p. 268
Solutions for Chapter 9 Exercises	p. 270
Solutions for Chapter 10 Exercises	p. 273
Solutions for Chapter 11 Exercises	p. 275
Bibliography	p. 277
Subject Index	p. 283
Definitions Index	p. 287
Table of Contents provided by Ingram. All Rights Reserved.

Please wait while the item is added to your bag...

FREE SHIPPING

Amazon no longer offers textbook rentals. We do!

Modelling Systems: Practical Tools and Techniques in Software Development

Summary

Table of Contents

Supplemental Materials