Autor: |
Ahmed Al-Brashdi, Michael Butler, Abdolbaghi Rezazadeh |
Jazyk: |
angličtina |
Rok vydání: |
2018 |
Předmět: |
|
Zdroj: |
Electronic Proceedings in Theoretical Computer Science, Vol 271, Iss Proc. IMPEX 2017 and FM&MDD 2017, Pp 34-47 (2018) |
Druh dokumentu: |
article |
ISSN: |
2075-2180 |
DOI: |
10.4204/EPTCS.271.3 |
Popis: |
Correct operation of many critical systems is dependent on the data consistency and integrity properties of underlying databases. Therefore, a verifiable and rigorous database design process is highly desirable. This research aims to investigate and deliver a comprehensive and practical approach for modelling databases in formal methods through layered refinements. The methodology is being guided by a number of case studies, using abstraction and refinement in UML-B and verification with the Rodin tool. UML-B is a graphical representation of the Event-B formalism and the Rodin tool supports verification for Event-B and UML-B. Our method guides developers to model relational databases in UML-B through layered refinement and to specify the necessary constraints and operations on the database. |
Databáze: |
Directory of Open Access Journals |
Externí odkaz: |
|