Automated Test Case Generation using Coloured Petri Nets

In our efforts to develop a CPN-based library for model-based test case generation, we focus at the moment on Gorums [3], a novel framework for building fault tolerant distributed systems. We have already successfully modelled a simple quorum system with a number distributed servers in CPN Tools and use our library to record test cases from either state space exploration or simulation [1]. The left picture below shows the architecture of the Gorums framework. The right picture shows the overall testing architecture using CPN Tools and our library.

Gorums architecture Testing architecture

You can download the corresponding CPN Tools [2] model here: singlePaxos.cpn.
Also, here we list some colour set declarations (mainly appear in figures of our paper [4]) for this model:

colset ServerID = INT;
colset Value = STRING;
colset ReplicaIDxValue = product ServerID * Value;
colset Rnd = INT;
colset CallId = INT;
colset AcceptedMessage = Rnd * Value;
colset PrepareMsgs = product CallId * Rnd;
colset PromiseMsgs = product CallId * Rnd * AcceptedMessage;
colset AcceptMsgs = product CallId * Rnd * Value;
colset LearnMsgs = product CallId * Rnd * Value;
colset EmptyMsgs = CallId;
colset Message = union Prepare : PrepareMsgs + Promise : PromiseMsgs + Accept : AcceptMsgs + Learn : LearnMsgs + Empty : EmptyMsgs;
colset ReplicaIDxMessage = product ServerID * Message;
colset LeaderID = INT;
colset ReplicaIDxLeaderID = product ServerID * LeaderID;
colset ReplicaIDxRndxAcceptedMessage = product ServerID * Rnd * AcceptedMessage;
colset PrepareReplies = list PromiseMsgs;
colset CxRndxPrepareReplies = product CallId * Rnd * PrepareReplies;
colset QFPrepareResult = product Message * BOOL;
colset CxQFPrepareResult = product CallId * QFPrepareResult;

References

  1. Wang R, Kristensen LM, Meling H, Stolz V. Application of Model-based Testing on a Quorum-based Distributed Storage . CEUR Workshop Proceedings. 2017
  2. CPN Tools homepage
  3. Tormod Erevik Lea, Leander Jehl, and Hein Meling. Towards New Abstractions for Implementing Quorum-based Systems. In 37th International Conference on Distributed Computing Systems (ICDCS), Jun 2017.
  4. R. Wang, L. M. Kristensen, H. Meling, V. Stolz. Automated Test Case Generation for the Paxos Single-decree Protocol using a Coloured Petri Net Model. Journal of Logical and Algebraic Methods in Programming (JLAMP), 2018. (Invited for Journal of Logic and Algebraic Programming, under revision.)