Formal Development of a Washing Machine Controller Model Based on Formal Design Patterns

摘要

Formal methods approach to software construction can significantly increase the reliability and correctness of the resulting software. Formal methods users are given sophisticated languages and tools for constructing software models, but they often lack some systematic methodological measures to help. Formal design patterns can help formal methods users speed up the development process by re-using and incorporating some pre-defined proved and refined models, as design patterns do in object-oriented software. Some formal design patterns are presented and applied to the development of a washing machine controller model in Event-B that is a formal method for modeling and reasoning about complex discrete system.