Sponsor: Motorola Inc.
The rapid development of high-reliability systems is a dominant software engineering problem in the 1990's. Obtaining complete, consistent, and correct requirements is crucial for successful systems and software development. Studies have repeatedly shown that most of the cost of software development stems from requirements defects. Undiscovered errors in requirements specifications can cost ten or more times to fix them in programming or maintenance phases. This project investigates methodologies and supporting algorithms for detecting errors early in the requirements phase through formal verification.
