Incremental Database Design using UML-B and Event-B

被引：1

作者：

Al-Brashdi, Ahmed ^{[1
]}

Butler, Michael ^{[1
]}

Rezazadeh, Abdolbaghi ^{[1
]}

机构：

[1] Univ Southampton, Southampton, Hants, England

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2018年 / 271期

关键词：

EXECUTABLE CODE; MODEL;

D O I：

10.4204/EPTCS.271.3

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：34 / 47

页数：14

共 21 条

[1]

Abrial J., 2010, Modeling in Event-B: System and Software Design, DOI DOI 10.1017/CBO9781139195881

[2] Rodin: An open toolset for modelling and reasoning in Event-B [J].

Abrial J.-R. ;

Butler M. ;

Hallerstede S. ;

Hoang T.S. ;

Mehta F. ;

Voisin L. .

International Journal on Software Tools for Technology Transfer, 2010, 12 (06) :447-466

[3]

Al-Brashdi Ahmed, 2017, CAS STUD

[4]

Al-Brashdi Ahmed, 2016, FM MDD WORKSH ICFEM, P1

[5]

Al-Brashdi Ahmed, 2015, THESIS

[6]

[Anonymous], 2005, B BOOK ASSIGNING PRO

[7]

Butler M, 2013, ENG DEPENDABLE SOFTW, P49, DOI DOI 10.3233/978-1-61499-207-3-49

[8]

CODD EF, 1970, COMMUN ACM, V13, P377, DOI 10.1145/357980.358007

[9]

Connolly T.M., 2005, DATABASE SYSTEMS PRA, V4th

[10]

Davies J., 2006, 11th IEEE International Conference on Engineering of Complex Computer Systems, DOI 10.1109/ICECCS.2006.1690374

← 1 2 3 →