Formal methods are helpful in validating and verifying embedded systems, but they are hard to use and are resource-intensive. A Computer-Aided, Cost-Effective Validation (CACEV) system has most of the advantages of formal methods but is easier to use and takes advantages of automated tools to make rigorous validation of safety-critical systems more efficiently.;CACEV transforms informal requirements for a system to a more formal representation that can be validated against an operational specification of that system. It has been applied to the design of a voting module in a software testbed developed by NASA to show that the critical requirements are preserved at all times by the design.
展开▼
