Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Correctness for CQRS Systems – Elicitation and validation.
KTH, School of Computer Science and Communication (CSC).
2012 (English)Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Building distributed systems is a complex task, especially when new design patterns appear. Command Query Responsibility Segregation is one of these new patterns, which in its core aims to separate the read and write side in the system. As it happens to be this pattern meshes very well with some other common patterns like event sourcing, eventual consistency and Domain Driven Design. This adds to the complexity of the system, which makes it more difficult to deem if it is correct or not. This thesis aims to find critical properties that when they are applied to a system then it can be said to be correct. The presence of these properties is showed with a verification model written in Promela and then verified in the tool SPIN. The system however proved to be to complex to prove exhaustively, i.e. mathematical correctness, and an approximation method had to be employed. The results shows that the tool indeed was able to show the presence of these critical properties in the model. By using this model as a specification for how messages are passed in the CQRS system makes the system correct. Also this leads to that the correctness properties are present in that system. This thesis has thus helped to reduce the gap between a written specification of a system and a real implementation.

Abstract [sv]

Att implementera distribuerade system är en komplicerad uppgift, speciellt när nya designmönster dyker upp. Command Query Responsibility Segregation är ett av de här nya designmönstren, som har som mål att separera läs- från skrivsidan i systemet. Det råkar vara så att CQRS passar väldigt bra tillsammans med några andra designmönster så som event sourcing, eventual consistency och Domain Driven Design. Det här leder till att systemen oftast blir komplexa och det blir svårt att avgöra om systemet ifråga är korrekt eller ej. Det här examensarbetet har som mål att finna kritiska egenskaper som när de är applicerade på ett riktigt system så kan detta system sägas vara korrekt. Närvaron av dessa egenskaper visas med hjälp av en verifikationsmodell som sedan verifieras av verktyget SPIN. Det visade sig dock att verifikationsmodellen var för komplex för att bevisas matematiskt genom en fullständig sökning, så en approximationsmetod blev nödvändig. Resultaten visar att modellen innehöll de utlovade egenskaperna. Använder man sedan denna modell som mall för ett riktigt CQRS-system så kan man kalla det riktiga systemet för korrekt. Detta eftersom alla korrekthetskrav som finns i modellen också kommer att finnas i det riktiga systemet. Examensarbetet har med andra ord reducerat gapet mellan en skriven specifikation och en verklig implementering.

Place, publisher, year, edition, pages
2012.
Series
Trita-CSC-E, ISSN 1653-5715 ; 2012:072
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-130944OAI: oai:DiVA.org:kth-130944DiVA: diva2:654390
Educational program
Master of Science in Engineering - Computer Science and Technology
Uppsok
Technology
Supervisors
Examiners
Available from: 2013-10-07 Created: 2013-10-07

Open Access in DiVA

No full text

Other links

http://www.nada.kth.se/utbildning/grukth/exjobb/rapportlistor/2012/rapporter12/hakim_kamil_12072.pdf
By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 717 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf