Abstract
The book summarizes results of DEPLOY research project on engineering methods for dependable systems. A formal method is not the main engine of a development process, its contribution is to improve system dependability by motivating formalisation where useful. This book summarizes the results of a major research project on engineering methods for dependable systems through the industrial deployment of formal methods in software development in applications such as automotive, space, railway and business systems, and microprocessor design. The project plan was to introduce a formal method -- Event-B -- into some industrial organisations working in different application domains, while its larger aim was to learn lessons from the experience. The contributing authors report on pilot projects and lessons learned from these experiences. For the academic and research partners and the tool vendors, necessary improvements in the formal method and its supporting tools were identified. For the industrial partners, much was learned about the value of formal methods in general and of Event-B in particular, A particular feature of the book is the frank assessment of the related managerial and organisational challenges and the deficiencies in the methods and supporting tools. The book will be of value to academic researchers, systems and software engineers developing critical systems, industrial managers, policymakers, and regulators. Rodin Tools is a Not for Profit Company taking over responsibility for the the Rodin toolset at the end of the EU funded Deploy Project. The Rodin platform provides a range of features to support formal refinement-based development using Event-B. It has been applied in developing a wide range of applications in the aerospace, transportation, business information, automotive and microprocessor domains.