The Refinement Validation of UML-B Pattern The Refinement Validation of ATM Model by Using UML-B |
|
| Author:
| El-Sayed, Eman |
| ISBN: | 978-1-4912-2746-6 |
| Publication Date: | Jul 2013 |
| Publisher: | CreateSpace Independent Publishing Platform
|
| Book Format: | Paperback |
| List Price: | USD $75.00 |
Book Description:
|
Event-B is a formal method to develop the computer software in modeling level and analysis of dependable applications. It is based on abstract machine notation. It is supported by an open and extendable Eclipse-based tool set called Rodin. In recent years, Event-B and Rodin have been used to model complex real world systems and also prove consistency properties of them. However, refinement that kind of systems which have difficult proofs is not an easy task, so Event-B design pattern...
More DescriptionEvent-B is a formal method to develop the computer software in modeling level and analysis of dependable applications. It is based on abstract machine notation. It is supported by an open and extendable Eclipse-based tool set called Rodin. In recent years, Event-B and Rodin have been used to model complex real world systems and also prove consistency properties of them. However, refinement that kind of systems which have difficult proofs is not an easy task, so Event-B design pattern just another model used to the formalization of a typical problem.