Premium
A specification case study using the B‐methodology
Author(s) -
Storey Andrew
Publication year - 1992
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.4370020404
Subject(s) - b method , computer science , programming language , notation , formal methods , formal specification , software engineering , process (computing) , specification language , code (set theory) , mathematical notation , simple (philosophy) , development (topology) , software development , software , mathematics , arithmetic , mathematical analysis , philosophy , set (abstract data type) , epistemology
The B‐Method is a complete formal development process for mathematically transforming software systems from specification through to code. This article provides the reader with an overview of the process including a description of the language used for specifying systems (Abstract Machine Notation) and demonstrates its application by a simple, real‐life case study. The method has tool support in the form of a tool‐kit which is described here and applied to the case study. The results of the case study show how a system can be validated and verified in the early stages of its development through proof of the mathematical specification and an animating tool.