An analytical software design system arranged to receive informal system design specifications and to convert them into verified design specifications for use in creating source code and carrying out implementation testing of the source code is described. The system comprises a verified black box specification generator arranged to process the received informal system design specifications to create formal specifications; to generate from the formal specifications mathematical models representing the system behavior; to analyze the mathematical models to determine if they have the required behavior; to adjust the formal specifications until the required behavior is achieved; and to derive the required verified design specifications from the mathematical models.