Download PDFOpen PDF in browser

Designing and Verifying Microservices Using CSP

EasyChair Preprint no. 5390

4 pagesDate: April 25, 2021


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: concurrency, CSP, Microservices, model checking, race conditions

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Jeremy Martin},
  title = {Designing and Verifying Microservices Using CSP},
  howpublished = {EasyChair Preprint no. 5390},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser