We have been building complex software systems for over 40 years . And yes, we have struggled and had our share of failures, but we have also achieved an extraordinary degree of success: online trading, the Internet, desktop productivity tools, lifesaving medical equipment, and safe power plants, to name a few.
It's clear that we have somehow managed to move from the world of requirements to the world of design and implementation. We have implemented many complex systems that conform to their requirements. However, when it comes to building complex systems that require a high degree of safety or reliability assurance, it hasn't always been a pretty (or at least a rigorously scientific) matter. The reason is that requirements do not lend themselves to being readily exposed for inspection within the implementation. Proving that any particular requirement is fulfilled in the code is a nontrivial matter. In this chapter, we explore this particular problem to see if we can gain some insights into a potential solution.