Where academic tradition
meets the exciting future

Formal Verification of Stateful Services with REST APIs using Event-B

Irum Rauf, Inna Vistbakka, Elena Troubitsyna, Formal Verification of Stateful Services with REST APIs using Event-B. TUCS Technical Reports 1192, TUCS, 2018.

Abstract:

REST APIs are being increasingly used in the industry including their application in safety-critical applications and in the IoT world. They offer basic CRUD (create, retrieve, update, delete) interfaces. However, REST APIs can be used to build services with more advanced scenarios. Developing such services with REST constraints require rigorous approaches that are capable of creating services that can be trusted for their behavior. In this work, we present an approach based on formal verification technique for development of REST services and focus on deriving correct system architecture by refinement and on formal verification consistency of service design models. We use Event-B and its refinement approach for system development. We illustrate our approach on a Hotel Reservation System.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tRauf_Irum18a,
  title = {Formal Verification of Stateful Services with REST APIs using Event-B},
  author = {Rauf, Irum and Vistbakka, Inna and Troubitsyna, Elena},
  number = {1192},
  series = {TUCS Technical Reports},
  publisher = {TUCS},
  year = {2018},
}

Belongs to TUCS Research Unit(s): Embedded Computer and Electronic Systems (ECES)

Edit publication