Robust software is technically possible but too expensive
Does the lift go up when you push the up button or down because someone in a lower floor pushed the button at the same time? This is an example of the types of problems that occupy Professor Antti Valmari, recipient of the 2014 CAV Award.
“If software vendors really wanted to get rid of continuous software updates to fix vulnerabilities and other bugs, they could do it. But it would hurt their bottom line,” claims Professor Antti Valmari.
To frustrated users it often seems that security patches and updates are released when they are especially busy with work.
”Researchers could develop reliable software that does not need continuous updates,” Antti Valmari says. He holds a professorship in the Department of Mathematics at TUT.
”But software companies are disinclined to implement robust software development models, because they are expensive and time-consuming, at least to begin with. It couldn’t be done without delaying product launch and reshaping company culture. It is easier and cheaper to regularly release updates.”
Integrated circuit designers face a different set of challenges. If the circuit for an anti-lock braking system is faulty, car manufacturers are forced to recall millions of vehicles, which is very expensive. Circuit designers are therefore highly motivated to strive for faultless performance.
“Aircraft manufacturers are committed to the development of reliable software to ensure the safety of air traffic but have little wiggle room, because the number of programmers with a different approach to software development is limited. Most passenger aircrafts can be controlled manually, just in case the computer systems fail,” Valmari says.
CAV Award 2014
Computer-Aided Verification (CAV) is an area that aims to develop automatic methods that are capable of detecting errors in computer programmes and integrated circuits more effectively than any form of testing.
- The annual CAV Award was established in 2008 to recognize fundamental contributions to the field of computer-aided verification.
- The 2014 CAV Award was given out during Vienna Summer of Logic on 19 July.
- Antti Valmari is one of the four winners who received the 2014 CAV Award. The co-winners are Patrice Godefroid from the USA, Doron Peled from Israel and Pierre Wolper from Belgium.
- Godefroid, Peled and Valmari made their award-winning discoveries in computer-aided verification, independent of each other, around the year 1990. Godefroid wrote his dissertation under Wolper’s supervision, and Valmari was one of the opponents at Godefroid’s public defence. A number of other scientists began to explore similar ideas and gradually an active area of research known as partial-order methods evolved.
- The award worth 10,000 dollars was divided equally between the winners.
Computer-aided verification versus conventional software testing
Software goes through a rigorous testing and debugging process to expose failures but cannot be exhaustively tested in advance against all possible inputs.
Computer-Aided Verification (CAV) is an area that aims to develop automatic methods that are capable of detecting errors in computer programmes and integrated circuits and outperform conventional testing techniques.
“All possible alternative behaviours of a system constitute an abstract network called state space. Any real behaviour is one path through it. Rather than individual paths, the goal of CAV is to explore this network as a whole,” Valmari describes.
Valmari has developed methods that uncover hidden bugs and shed light on the interactions between software components or software and hardware. He was acknowledged for his scientific achievements with the international CAV Award in July 2014.
Stumbling blocks to communication
Valmari gives an example of what can go wrong in the communication between two pieces of hardware and software.
“If an excavator happens to accidentally cut off the cable between a cash machine and a bank’s computer right after a withdrawal has been authorized, the computer has no way of knowing whether the cash was dispensed or not. Should the bank software charge the account?”
“System failures cannot be completely prevented, but the methods I’ve developed ensure that even if the connection is dropped at the worst possible moment and money fails to appear, the customer’s account is not debited,” Valmari says.