Distributed Testing is something we are still in the opening days of. Cloud computing makes it possible to innovate: you can bring up virtual clusters with different system configs, use SDN to create networks and even inject faults. At the same time, they make life hard, as the time you come in to work the VMs of a test run which have failed the test have already been recycled, and all you have are the logs of 8 services running on ten machines; you get to open up the likely ones in your text editor and using timestamps try and work out what was happening.
Some of the best work there comes from telecom
My 2015 thoughts on the matter.
My view is that reporting the results could be radically improved, diagnostics, and even automating the generation of complex configurations. A "configuration space" is one of those Hilbert Space thingys, where every time someone goes "hey, add a new config option!", you've added another dimension. The key point is that only some regions in the configuration space are valid for successful system behavior. Some of the work of a good tester is to identify those areas where the system fails to work, yet it is within the space of areas where customers expect to run the system.
Some reading from a list of a local directory
1999_ulrich_siemens_Test Architectures for Testing Distributed Systems.pdf
2001_long_DOA_ A case study in testing distributed systems.pdf
2006_rutherford_phd_Adequate System-Level Testing of Distributed Systems.pdf
2009_Hierons-_brunel_TAROT09_Testing Distributed Systems.pdf
2014_suny_IST_Model-Based Testing of Global Properties on Large-Scale Distributed Systems.pdf
2015_riesco_madrid_sparkTest_A Lightweight Tool for Random Testing of Stream Processing Systems.pdf
Ulrichs is a good intro from telecoms; focused on state machines, and building the aggregate test from smaller stes. The others follow on.
In my current work I've been exploring a concept which doesn't appear to have anything written up from an academic perspective: Metrics first testing. Here we add more system metrics to the application, essentially exposing some of the internal state. I can then make assertions about the state of parts of the system in unit tests. In larger system tests: collect those metrics and use them to help understand what happened.
Early days there, for unit/integration tests it's good, albeit brittle to changes in what is now a "grey box" system under test: optimise performance and tests counting the number of times something happened fail, you get to decide whether its a false negative or legit.
Regarding Formal Specs and verification, I have actually written the Formal Filesystem Specification for the Hadoop FS API, albeit working backwards from what was implemented in HDFS. Here the specification language used is Python, which works well for one key reason: it is understood by developers, who can grasp the declarative filesystem model as some tuples, lists and hash tables. It all maps 1:1 to the set theoretic calculus of Spivey's Z language, it's just disguised as python. In doing so, we have a spec which is broadly understood and maintained —and from there, we derive the Filesystem contract tests.
The limitations we have there is that it doesn't do temporal logic/concurrency, and there's no automated parsing/validation of the spec. I've been playing with TLA+, but that language just scares everyone off.
Anyway, hope I haven't scared you off, but I can assure you that there are PhDs to be had in this area. And, as so much of this work is being done as Open Source, you can even get to see how some of it works development communities,