SPECIFICATION IN B: AN INTRODUCTION USING THE B TOOLKIT
by Kevin Lano (Imperial College)
&
Howard Haughton (J P Morgan Corp, London)
Kevin Lano is a research fellow at Imperial College. He has extensive experience in formal development and has published over 40 papers on the theory and practice of formal specification and refinement, and three books on software engineering and specification. He has presented tutorials and training courses on B to industrial audiences, and carries out consultancy in B AMN. He is a committee member of the BCS FACS and the Z User Group. Howard Haughton has extensive experience in the use of B AMN, and in the specification and development of industial systems using formal methods. He was the technical manager of the B User Trials project and has published papers on B at the FME and Refinement Workshop conferences.
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 practitioners. Extensive examples of all development life-cycle stages are given, including animation, proof, design and code generation in C. Two large case studies and exercises with solutions are provided.
The authors have extensive experience in teaching B and in its industrial application to high integrity systems. The book uses the B Toolkit to support the text, but it is also relevant to users of alternative toolsets for B.
|
