CSCI 8970 – Colloquium Series – fall 2010 – Thirteenth Event
Analysis Engines
Monday, December 6, 2010
Presenter: Mike Whalen – University of Minnesota Software Engineering Center
During the most recent colloquium Mike Whalen, a professor and researcher at the Software Engineering Center spoke about the need to debug or look for errors within programs through a more holistic and comprehensive approach. While traditional debugging will detect many flaws, so flaws are hard to differentiate from properly written code. During his lecture he decided not to talk specifically about medical devices. He currently receives support from NASA, the Air Force, Lockheed as well as other major corporations.
One of the first issues that Dr. Whalen addressed was an in-depth overview regarding how software is traditionally developed. He outlined the following parts in the design: concept formation, requirements specification, design, implementation, integration, system. Within traditional software developing a large portion of the costs are allocated to testing, where the unit test, the integration test, and the system test can account for up to 75% of the budget.
A reason for the high costs of testing is that when that it can be as difficult as finding a needle in a haystack. In addition emerging software size and complexity has increased over time. Sometimes the problem with an application may be a simple number improperly entered, a simply line of code with an improper conception. A particularly devastating example was what happened to Zune players built before 2008 which all became bricks as a result of an error within the initialization code after December 31, 2008. Beneath is a description of the code and its malfunction.
Year = originyear; /* = 1980 */
While (days > 365) {
If (isleapyear(year)) {
If (days > 366) { (((((if changed to days > 365) — it would not crash, but it is still incorrect))))
Days -= 366;
Year += 1;
}
} else {
Days -= 365;
Year += 1;
What are some ways in which testing can be improved? Testing even using a rigorous structural coverage metric such as MCDC , is very unlikely to catch this bug. Using MCDC + boundary value testing would likely catch it. What can be done is to change the process? Modify the concept formation -> (Requirements / analysis [properties]) -> Model / code -> object code -> integration -> system ->. Symbolic evaluation may also provide paths through the code. If you work with programs with loops – how do you know when you should stop looping? Symbolic evaluation does not do termination.
[P ^ B ^ t = z] S [P ^ t < z] / [P] while B do S done [⌐B ^ P]
Invariant Generation, Hoare logic / weakest precondition reasoning require loop invariants. Transition Relations describe behavior of systems by describing changes of variable values across a series of computational steps. Many things can be model in this manner. Can model lots of things this way: hardware, comm. protocols, dataflow languages, state machines, system architectures, programs (with some caveats), and more. Commercial vendors also use these tools.
Temporal logic (TL) is often used for model reasoning. TL describes the evolution of the model from some current state. There have been many different variants. CTL (computational temporal logic) describes the evolution of a tree of traces (views the world (its nodes) as a tree). LTL (linear temporal logic) describes the evolution of individual paths. (views the world (its nodes) as a line)
Model checkers were a breakthrough technology of the 1990s. There are several different types of Model Checkers. They are easy to use but they have limitations. How do they work? Even small models include millions of states. Symbolic Model Checking improves on Model Checkers. The main idea was to represent sets of system states symbolically as Boolean propositions. Each proposition describes a characteristic function for a set of states. Illustrating what is possible, Dr. Whale provided an example. While many individuals play and struggle solving Sudokus Empty Sudoku board has 9^81 = ~10^77 possible states. To solve them and any other Sudoku, Dr. Whalen applied the concepts of Model Checkers. The short program he wrote solved a hard Sudoku in one or two seconds. The concept was also used for the ADGS 2100 Adaptive Display and Guidance System – Checked 573 properties and found 98 errors in early design models. Dr. Whalen’s lectures provide an insight about the need for changes within the field of software engineering and the need for software to be tested by different methods to increase the reliability of the software and diminish the time that needs to be allocated to efficiently allocate time and resources. It has been a pleasure to listen to and learn from the CSCI colloquium series. Thank you!
