A correct system is only derived from a correct implementation of a correct specification. Unfortunately, this imposes a heavy burden in the development process, especially for complex, distributed system ranging from machine room computing and storage services as well as large-scale P2P applications. A specification, if authored in formal language such as TLA+, Spec#, SPIN etc., is ready for model checking. The state explosion problem, however, prohibits all specification states to be thoroughly traversed. Often ad hoc heuristics are applied to drastically reduce the scale so as to make the model checking phase tractable. A correct implementation can be even more challenging, especially when we encounter non-deterministic bugs that are hard to reproduce. The gap between spec and implementation often leaves one to wonder whether the implementation or the spec is faulty, or even both. Motivated by our experiences in developing several complete large scale distributed systems, we are designing and implementing a suite of testing and debugging facility on top of our previously developed WiDS platform.
展开▼
