Download PDFOpen PDF in browser

Designing and Verifying Microservices Using CSP

EasyChair Preprint 5390

4 pagesDate: April 25, 2021

Abstract

Microservices Architecture is a popular pattern used for building complex IT systems in an incremental, sustainable and scalable fashion. However, compared with traditional monolithic solution architectures, it introduces a higher degree of concurrency which might result in subtle bugs arising, such as race conditions, deadlocks and lack of data consistency. I shall illustrate this with a worked example of an automated insurance claims payment service which exhibits a bug whereby a particular claim may be settled twice. I shall use the CSP formal modelling language and the FDR refinement checker to prove some results about this bug and how to fix it.

Keyphrases: CSP, Microservices, concurrency, model checking, race conditions

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:5390,
  author    = {Jeremy Martin},
  title     = {Designing and Verifying Microservices Using CSP},
  howpublished = {EasyChair Preprint 5390},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser