FMSE

SBTC makes use of a Formal Methods Software Engineering (FMSE) process to ensure quality and process control for our software development activities. FMSE is the application of mathematical and logical properties to the development of software in order to provide leverage for reasoning about the software in question. The formal methods approach used by SBTC is based on the Cleanroom software engineering practices described by Dr. Harlan Mills, and our process is based on the process model documented by the Software Engineering Institute.

The process begins by gathering initial requirements that describe the functionality of the desired system. The requirements are then divided so as to separate the functionality of the system into individual executable increments, with each increment building to the final completed system. Requirements for a single increment are then refined through a systematic process that yields a formal specification. The specification is formed in such a way to ensure that it is mathematically complete, consistent, and traceably correct with respect to the requirements. This formal specification is then transformed into a software implementation through a series of stepwise refinements with each transformation being verified to ensure that the specified function is preserved. The final transformation results in an executable implementation of the increment functionality. Statistical testing is then performed on the executable increment to measure the quality of the implementation and to identify any design flaws. Along the way, questions are raised, recorded, tracked, and resolved to ensure that the specified system correctly addresses the problem to be solved and that the proper people are consciously making the necessary design decisions.