2/2014

Robust software is technically possible but too expensive

Antti Valmari

 

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.

Text: Leena Koskenlaakso
Photo: Mika Kanerva

 
Tell a friend
Synthetic bone graft straight off the OR shelf
Synthetic bone graft straight off the OR shelf
2/2014
Synthetic bone graft straight off the OR shelf
Miro Erkintalo wants to leave his mark on the world and academia
Miro Erkintalo wants to leave his mark on the world and academia
2/2014
Miro Erkintalo wants to leave his mark on the world and academia
Brain research leaps forward
Brain research leaps forward
2/2014
Brain research leaps forward
Joint implant stirs up growing interest around the world
Joint implant stirs up growing interest around the world
2/2014
Joint implant stirs up growing interest around the world
Bacteria meet their match in antibacterial coatings
Bacteria meet their match in antibacterial coatings
2/2014
Bacteria meet their match in antibacterial coatings
Multi-functional materials through surface modification
Multi-functional materials through surface modification
2/2014
Multi-functional materials through surface modification
Making sense of a jumble of sounds
Making sense of a jumble of sounds
2/2014
Making sense of a jumble of sounds
Effective speech recognition makes life easier for people and machines
Effective speech recognition makes life easier for people and machines
2/2014
Effective speech recognition makes life easier for people and machines
Quest for the Holy Grail of artificial intelligence
Quest for the Holy Grail of artificial intelligence
2/2014
Quest for the Holy Grail of artificial intelligence
Why does everything beep?
Why does everything beep?
2/2014
Why does everything beep?
TUT brings expertise to bear on engineering mathematics education in Russia and Caucasia
TUT brings expertise to bear on engineering mathematics education in Russia and Caucasia
2/2014
TUT brings expertise to bear on engineering mathematics education in Russia and Caucasia

Tampere University of Technology is at the leading edge of technology development and a sought-after collaboration partner among the scientific and business communities. The University produces competent graduates who enter careers in the different sectors of society.

Visiting address
Korkeakoulunkatu 10,
FI-33720 Tampere
Finland

Mailing address
PO Box 527, FI-33101 Tampere
Finland

Switchboard:
+358 3 311 511