Currently available tools and methods for system development that start with a formal model of a system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The "gap" that such tools and methods leave unfilled is that the formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the classes of complex systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements expressed in restricted natural language, or appropriate graphical notations, into a provably equivalent formal model that can be used as the basis for code generation and other transformations. The same approach may be applied to address computer science aspects of bioinformatics problems. Many software tools for bioinformatics have been developed using scripting languages such as Perl and Python. Scripts are developed based on a set of requirements that can be expressed using English-like statements. Using our approach, these may be used to automatically generate and validate scripts rather than write them from scratch.