Software faults can be expensive - for instance in automated teller machines (ATMs). Quality control should avoid such faults, but this is often a cumbersome, expensive and erroneous task. Jens Calamé from the Centrum Wiskunde & Informatica (CWI) in Amsterdam investigated how to automate this process. He took his PhD on 4 September 2008 at the University of Twente for his thesis Testing reactive systems with data - enumerative methods and constraint solving.
Calamé uses mathematical techniques - constraint solving and formal methods - to find faults in models and implementations of 'reactive systems with data', such as ATMs or electronic markets. The research challenge is that those systems can be in millions of possible states. Calamé found a way to reduce this number to a feasible quantity. He accomplished this by making test scenarios depending on the actual system behaviour.
To reduce the risks of faults even further, there has to be verified whether the models meet their specifications. This has to be done earlier in the development process. Calamé also designed a method to improve this check.
More information: see Jens Calamé's thesis.
