Forum for Science, Industry and Business

Sponsored by:     3M 
Search our Site:

 

Goodbye to faulty software?

17.07.2008
Will it ever be possible to buy software guaranteed to be free from bugs? A team of European researchers think so. Their work on the mathematical foundations of programming could one day revolutionise the software industry.

We have become used to the idea that software will not work properly. While we would take a faulty car back to the dealer and demand they put it right, we are remarkably tolerant of software that goes wrong.

The software we buy usually comes with no guarantee and disclaimers are notoriously all encompassing. We no longer expect everything to work correctly ‘out of the box’. More to the point, neither does the manufacturer. Indeed, software houses seem to rely on their customers to find faults, which they can then ‘patch’ in a so-called ‘upgrade’ of the product.

“The software industry is still very immature compared to other branches of engineering,” says Dr Bengt Nordström, a computer scientist at Chalmers University in Göteborg. “We want to see programming as an engineering discipline but it’s not there yet. It’s not based on good theory and we don’t have good design methods to make sure that at each step we produce something that’s correct.”

Nordström believes that the whole approach to software design needs to be rethought. The usual approach is to validate a program via a lengthy testing process. Instead, he would like to see a design philosophy that guarantees from first principles that a program will do what it says on the box.

The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct.

Open source

It is not that simple, of course, but so promising is type theory that since 1989 the EU has been funding a string of projects to develop it under the Future and Emerging Technologies programme.

Nordström was coordinator of one of the projects, TYPES, which fosters co-operation on the topic among researchers at 15 European universities and research institutes, along with those at 19 associated academic and industrial organisations.

The TYPES partners are also releasing open source software packages that anyone can download, use and modify. These packages include several ‘proof editors’ that, in type theory, are the key to guaranteeing the correctness of programs.

Can such an abstract research area really lead to reliable, bug-free software?

“European research in this field is the strongest in the world,” Nordström points out. “Many computer programs are going wrong, they don’t work properly, and in the long run this research will help. This is a very slow process, it takes many years to get ideas from the universities into industry but I think it’s slowly taking place.”

The open source principle, says Nordström, is fundamental to what they are trying to achieve.

“It’s important that anyone can evaluate the code and check if it is correct, so it’s inherent in this project that what we are doing should be open so that it can be discussed by everybody.”

Results from type theory are already finding their way into other projects. The EU-funded Mobius project is developing methods, known as ‘proof-carrying code’, for downloaded programs to be certified as bug-free.

Meanwhile, a France-based company is using ideas from type theory to design secure embedded computer systems such as those used for smart cards. Further research is also under way in Japan.

Theory, in practice

Researchers have also demonstrated the power of type theory by proving the classic ‘four colour’ theorem with one of the proof editors used in TYPES. Type theory is also finding application in the analysis of human language.

Nordström does not see type theory as being necessary for all programs, but there is a clear need for guarantees in critical systems in banking, for example. But type theory could also be important in the transport, defence and healthcare sectors, where mistakes can cost lives.

TYPES received funding from the EU’s Sixth Framework Programme for research as a ‘coordination action’, which describes projects that aim to oil the wheels of co-operation rather than directly develop a new technology. TYPES interweaves both basic and applied research.

“That’s one thing I find very, very interesting compared to other sciences,” Nordström notes. “We are maybe 150 people working in this project and it’s a mixture of very practical persons and very theoretical persons and there is a lot of exchange between them. I think that’s very rare compared to other sciences.”

He hopes that the work done under TYPES will ultimately allow programming to mature into a genuine engineering discipline with the same high standards and quality assurance now expected elsewhere in the engineering profession.

“A lot of effort is now spent on testing software,” he says. “Very often programs are written quite quickly and then they are tested and changed and tested again, and so on. It’s very unsystematic. This is not how we build bridges and highways.

That style of working is going to change so that we spend more effort on actually writing programs than testing them.”

Christian Nielsen | alfa
Further information:
http://cordis.europa.eu/ictresults
http://cordis.europa.eu/ictresults/index.cfm/section/news/tpl/article/BrowsingType/Features/ID/89864

More articles from Information Technology:

nachricht Smart Computers
18.08.2017 | Albert-Ludwigs-Universität Freiburg im Breisgau

nachricht AI implications: Engineer's model lays groundwork for machine-learning device
18.08.2017 | Washington University in St. Louis

All articles from Information Technology >>>

The most recent press releases about innovation >>>

Die letzten 5 Focus-News des innovations-reports im Überblick:

Im Focus: Fizzy soda water could be key to clean manufacture of flat wonder material: Graphene

Whether you call it effervescent, fizzy, or sparkling, carbonated water is making a comeback as a beverage. Aside from quenching thirst, researchers at the University of Illinois at Urbana-Champaign have discovered a new use for these "bubbly" concoctions that will have major impact on the manufacturer of the world's thinnest, flattest, and one most useful materials -- graphene.

As graphene's popularity grows as an advanced "wonder" material, the speed and quality at which it can be manufactured will be paramount. With that in mind,...

Im Focus: Exotic quantum states made from light: Physicists create optical “wells” for a super-photon

Physicists at the University of Bonn have managed to create optical hollows and more complex patterns into which the light of a Bose-Einstein condensate flows. The creation of such highly low-loss structures for light is a prerequisite for complex light circuits, such as for quantum information processing for a new generation of computers. The researchers are now presenting their results in the journal Nature Photonics.

Light particles (photons) occur as tiny, indivisible portions. Many thousands of these light portions can be merged to form a single super-photon if they are...

Im Focus: Circular RNA linked to brain function

For the first time, scientists have shown that circular RNA is linked to brain function. When a RNA molecule called Cdr1as was deleted from the genome of mice, the animals had problems filtering out unnecessary information – like patients suffering from neuropsychiatric disorders.

While hundreds of circular RNAs (circRNAs) are abundant in mammalian brains, one big question has remained unanswered: What are they actually good for? In the...

Im Focus: RAVAN CubeSat measures Earth's outgoing energy

An experimental small satellite has successfully collected and delivered data on a key measurement for predicting changes in Earth's climate.

The Radiometer Assessment using Vertically Aligned Nanotubes (RAVAN) CubeSat was launched into low-Earth orbit on Nov. 11, 2016, in order to test new...

Im Focus: Scientists shine new light on the “other high temperature superconductor”

A study led by scientists of the Max Planck Institute for the Structure and Dynamics of Matter (MPSD) at the Center for Free-Electron Laser Science in Hamburg presents evidence of the coexistence of superconductivity and “charge-density-waves” in compounds of the poorly-studied family of bismuthates. This observation opens up new perspectives for a deeper understanding of the phenomenon of high-temperature superconductivity, a topic which is at the core of condensed matter research since more than 30 years. The paper by Nicoletti et al has been published in the PNAS.

Since the beginning of the 20th century, superconductivity had been observed in some metals at temperatures only a few degrees above the absolute zero (minus...

All Focus news of the innovation-report >>>

Anzeige

Anzeige

Event News

Call for Papers – ICNFT 2018, 5th International Conference on New Forming Technology

16.08.2017 | Event News

Sustainability is the business model of tomorrow

04.08.2017 | Event News

Clash of Realities 2017: Registration now open. International Conference at TH Köln

26.07.2017 | Event News

 
Latest News

A Map of the Cell’s Power Station

18.08.2017 | Life Sciences

Engineering team images tiny quasicrystals as they form

18.08.2017 | Physics and Astronomy

Researchers printed graphene-like materials with inkjet

18.08.2017 | Materials Sciences

VideoLinks
B2B-VideoLinks
More VideoLinks >>>