Design Driven Development using the Spin Verifier.

The Problem: Currently, the NetBSD sources are inherited from historic research, and maintained by a small, but committed group of volunteers. Often, the role of the NetBSD developer is to implement or port the design and implementation of a research project, and this involves buildup of design understanding and interpretation within the memory of a few “experts” within the community. This poses a few problems, especially for newcomers to the project:

1. Documentation and reading code alone, is insufficient to capture design nuances.
2. The “experts” can become a point of gated access or failure.
3. Design discussions with new developers often occur informally in the form of socratic questioning, or Q&A with an “expert” oracle.
4. Design and implementation may drift, simply due to the lack of a canon for design, and more importantly a way to mechanically check it for consistency.

In this talk, I demonstrate DDD, compare it with industry’s “Model Based System Development” approaches, and show how the tech- nique may be used to help architects and developers (who may often be the same person), to separate concerns.

For architects, it takes off the burden of having to rely on their memory, random tests and bespoke models to keep state. For developers, it provides a clear ”source of truth” and a process based mechanism to verify their implementation based on this source. And for project managers, there’s much better visibility over the entire Q&A, analogous to but much more powerful than a simple TDD style development process.