Post a Comment
FROM EDN EUROPE: Formal-verification tools for embedded software development
By Graham Prophet -- EDN, 12/7/2000
Users of iLogix's Rhapsody and Statemate Magnum software-development tools can now use formal methods to assist with verification of their code. Statemate is a high-level tool for project specification and validation; Rhapsody is a software-design-support tool that spans requirements analysis through test, with automatic code generation and iterative code refinement. The new software, which the company has added through a cooperative arrangement with Offis Systems and Consulting GmbH (OSC), covers model checking and automatic test generation for embedded software projects. Model checking verifies that a design model conforms to a formally expressed requirements specification; that is, that it behaves in exactly the same way and enters all the required states—no less and, importantly, no more. The simple example OSC quotes is that in vehicle-control software, you could confirm that the statement "The steering wheel can never be locked while the ignition is on" is true in every possible case; that is, it can guarantee that your software has no path to enter a particular state other than the ones you have already envisaged, and therefore no unexpected behaviour should arise in operation.
With the automatic test generation, you can develop test cases from the design models and improve code quality by more comprehensively covering a broader range of test scenarios. According to OSC co-founder Dr Werner Damm, test is the weak link in conventional embedded code development because of human inability to envisage and test for the unexpected case; formal methods allow you to comprehensively explore all possible paths through the software. Formal methods have been used in hardware development for some time, largely in equivalence checking to verify that a set of data has the same function before and after a transformation, such as logic synthesis. These methods have been hard to apply to software because of the large number of degrees of freedom that software allows. To handle software, you must be able to rapidly classify and dismiss sectors of the problem, and it appears to be in this area that OSC has made progress. Damm says that you can completely analyse large state spaces (10100 to 10300 ) in minutes.
The company will introduce formal verification for Statemate and Rhapsody in the first and second half of 2001, respectively. According to iLogix chief executive officer, Gene Robinson, iLogix will price the tool to allow its use by every Rhapsody user.
