Scribble - Proving a Distributed Design
As our interconnected world becomes ever more complex, designing reliable distributed solutions, where components running on networked computers coordinate their actions by exchanging messages, becomes exponentially harder to prove. At present, we rely on visual inspection of design artefacts and run test cases against stub or real services; however, the proving of the design is only as good as the people checking artefacts or creating test scenarios. There is no in-built mathematical rigour to either approach and therefore no guarantees that the design will not results in deadlocks or livelocks. The cost of discovering this downstream during testing (or, worse, live) can be huge. We have a better approach, based on mathematical proofs of distributed design, which allows us to check not only the UML artefacts for design flaws, but also to monitor the running implementation.
Three ways of proving a distributed design – only one provides the rigour we need for the complexities we currently face
Our approach uses Scribble, a formal and unambiguous machine-processable and human-readable language for describing the exchange of information between two or more participants – a choreography. It has firm mathematical roots, derived from the Pi-Calculus of Robin Milner and the Multi-Party Session Type of Honda, Yoshida and Carbone, as well as the work of W3C in developing WS-CDL (Web Services Choreography Description Language). The reason this works is that Scribble has all the description you need to build a model and perform the reasoning required to ensure that model is correct.
Think of the model as a union of the existing artefacts. By creating this union, we enforce a consistency check against each new artefact (such as a sequence diagram), ensuring the new behaviour the artefact expresses does not break the existing types described in the model. The Scribble type system, part of the Scribble compiler, performs this type-checking to ensure freedom from livelocks, deadlocks, race conditions and other unintended consequences. Further, the model can later be used to monitor (and even enforce) the running process against both functional and non-functional behaviours.
We produce an initial Scribble model early in the project. This allows us to run a “design proof” – checking that the choreography does not result in design problems – which we review with the customer’s design authority. We then use the model to generate the ‘local’ types (the end-points), expressed as Java microservice stubs embodying a finite state machine (FSM). Our implementation adds key features such as logging (using OpenTracing), role-based “wait times” (to simulate time taken to execute a manual process), and validation of inputs against outputs using Schematron.
Design-time view shows how the model is built and checked
We deploy these microservices in OpenShift, an opensource PaaS based on Docker and Kubernetes. This means we can add functionality to the stub implementations, or swap them out completely for the real implementations, simply by changing end-point bindings within OpenShift. We also generate test scenarios directly from the Scribble model, using the business flow of events described in sequence diagrams and BPMN. As we run these tests, we check that the choreography was followed (by comparing the model against the the OpenTracing logs); whether expected inputs match expected outputs; and how long each scenario takes, including the wait times for each process step.
Run-time view shows how implementation is checked against model via OpenTracing
Our future vision compares the design artefacts in the design tool which reflect the business perspective (the “Voice of the Business”) with the behaviour observed in the live environment (the “Voice of the Machine”). This helps us understand if the live business process (and choreography) is the way the business thinks it is and how it could be improved. This is especially important when looking at legacy systems for which designs are unreliable or unavailable.
By using the same OpenTracing framework to understand both design artefacts and instances through the live system, we can check if the process is working as expected.
Find out More
Our approach is unique and the result of partnership across a number of leading universities including Imperial College, Edinburgh and Glasgow. Scribble provides a powerful platform for proving a distributed design. We have taken this further to infer the model from the design artefacts and then both check and enforce the run-time choreography against the expected behaviour described in the model.
Call us today on 0208 012 8599 or email email@example.com and find out how Scribble can work in your business.