'Extending Model Checking to Object Process Validation'

| Redactie

Error-free software an illusion? Crashes suggest this daily. Software is getting more and more complex and difficult to control. So states ir. Rick van Rein, who previously caused a stir by developing smart software to bypass faulty memory chips which ensured that a few faulty chips would not render the entire memory modules unusable. Van Rein was awarded his doctoral degree on May 2nd in the faculty of Computer Science of the University of Twente. His supervisor was Professor Peter Apers.

Software errors can result in major consequences. 'Take the Star Wars project, designed by the Americans to intercept Russian missiles. That is the greatest failure ever in the area of software engineering: it got too complex and generated too many errors. But less disastrous consequences can be seen on a daily basis on your desktop PC', Van Rein said.

According to him the problem is that new versions are constantly under development, while the original design concept is forgotten. 'Compare it to a block of flats where new floors and creative extensions are constantly being added, without taking the foundation into account. Assuming of course that the foundation was correct in the first place.'

The problems start when the very first version of new software is tested. Van Rein explains that if the design requirements are not well defined, it will be difficult to turn to the original idea when working on new versions.

When the idea is firmly fixed in a mathematical model, the test software can fall back on it, even when testing new versions. 'The technique of model checking is already used but gets complicated when many events occur at the same time. That results in guesswork.' That is why Van Rein has aimed his research at the processes in a practical object-oriented environment. Everything that happens in the workflow of an organization is recorded in a model and monitored. Says Van Rein, 'That is a difficult problem because the automatic prove-system should essentially be able to handle an unlimited number of processes. The real art is transforming this to a large but finite model.' For this purpose Rick van Rein has developed a sort of a language which can store the process design graphically and thus allows the proof-tool to quickly check whether the design adheres to the requirements.

Concurrently the PhD student has started a company in the area of digital signatures.


Stay tuned

Sign up for our weekly newsletter.