Designing and Verifying Microservices Using CSP

EasyChair Preprint 5390

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

@booklet{EasyChair:5390,
  author    = {Jeremy Martin},
  title     = {Designing and Verifying Microservices Using CSP},
  howpublished = {EasyChair Preprint 5390},
  year      = {EasyChair, 2021}}