Onderzoeker UT: minder softwarefouten door toepassen van moderne kansmodellen

Mark Timmer zal op de Universiteit Twente promoveren op zijn onderzoek naar model checking. Daarbij worden computersystemen gemodelleerd en vervolgens automatisch op fouten gecontroleerd. Dit concept zou bepaalde bugs met wiskundige zekerheid kunnen voorkomen.

Bij de Universiteit Twente doen Timmer en andere studenten onderzoek naar methoden om het aantal fouten in software terug te dringen. Daarbij is onder andere gekeken naar zogeheten Markov-automaten, een wiskundig kansmodel. Via dit model kunnen kwantitatieve aspecten bij het toepassen van model checking meegenomen worden, zoals bepaalde tijdsduren en door kansen bepaald gedrag.

Timmer heeft met name gekeken naar het verbeteren van een uitbreiding van de model checking-technologie waarbij moderne kansmodellen een belangrijke rol spelen. Zo kan er nauwkeuriger gemodelleerd worden en is het bijvoorbeeld mogelijk om tijdens het testen aan te geven dat een bepaald onderdeel na een x-aantal gebruiksuren defect raakt.

Volgens Timmer kunnen hierdoor complexe systemen beter getest worden op fouten, iets wat met name cruciaal is bij gevoelige systemen in bijvoorbeeld kerncentrales of raketten. Timmer zal op 13 september promoveren op zijn onderzoek naar model checking.

Reacties (19)

[Garyu]

Is dit nieuw? Er zijn duizenden onderzoekers ter wereld bezig met verschillende vormen van software-modellering naar mathematische en minder mathematische methodes.

Ik ben benieuwd waar deze heer Timmer dan speciaal onderzoek naar doet binnen het gebied van de formele methoden dat nieuw is? Er zijn een aantal model-checkers die gebruikt kunnen worden, vaak op basis van bepaalde (SMC) solvers die de mathematische modellen doorrekenen. Zo te lezen heeft hij de modellen met bepaalde kans- en timing-aspecten verbreed, wat natuurlijk de modellering ook ingewikkelder en duurder maakt.

Het grote probleem zit hem nl. in de kosten van het werk. Immers het modelleren van een wat complexer systeem is niet iets wat een laaggeschoolde kracht eventjes ernaast doet. Je hebt hier gemiddeld een flinke dosis abstractievermogen voor nodig en gedetailleerde kennis over de technologie. We hebben het dan meestal over mensen met een degelijke informatica en wiskunde-achtergrond (lees: gepromoveerd op dit gebied). Het zijn kosten die je bovenop de gemiddelde testactiviteiten kan tellen en wat snel in de zes (of zeven) cijferige getallen loopt.

En ook voor de gepromoveerde informaticus is het nog absoluut niet triviaal om een fatsoenlijk model te maken dat een correcte afspiegeling van de software zelf is. Wie bepaalt immers de correctheid van het model?

Vandaar ook dat er tal van Europese projecten die er op dit gebied zijn. Vooral in de context van High-Reliability systemen is model-checking eigenlijk de enige manier om nog valide uitspraken te kunnen doen over de kwaliteit van software, maar de kosten maken dit tot nog toe alleen maar toepasbaar in de hoeken van de high-reliability software, waar fouten in software echt extreem enorm kostbaar zijn. We hebben het dan over human-spaceflight of kerncentrales, draagraketten die satellieten de lucht insturen. Voor software in vliegtuigen is het de vraag of het rendabel is en bij automotive software wordt het momenteel niet of nauwelijks toegepast.

PS: De Thesis van Mark Timmer voor de geinteresseerde (via een ander persbericht)

[Reactie gewijzigd door Garyu op 23 juli 2024 12:27]

[sickyb]

De kosten van het werk zijn inderdaad enorm. Als ik bedenk hoe veel werk ik heb gehad om een relatief simpel model te maken voor mijn afstudeerscriptie is het gewoon economisch niet haalbaar voor veel bedrijven om dit soort technieken in te zetten om de kwaliteit van de software te bewaken/garanderen.

Overigens de correctheid van het model wordt natuurlijk bewezen door de modelchecker. Er zijn alleen een aantal aannames nodig om dit werkbaar te maken.
dus:
aannames + model ==> correctheidsbewijs

Maar inderdaad wie garandeerd de correctheid van de aannames. en hoe ga je om met de omgeving waarin je software moet draaien. ga je alles inclusief de drivers en het OS ook modelleren?

De wereld van de software development veranderd erg snel. Als je in een Dev team werkt volgens Scrum oid, ga je dan in je sprint een model van je nieuwe functionaliteit opleveren je code schrijven de nodige testen doen (ok testen wordt minder belangrijk met een correct bewezen model) en de documentatie bijwerken voor je gebruikers?

Met andere woorden er is nog een enorme effort nodig om Model checking te laten landen in de wereld van de Devvers.

PS. bedankt voor de link naar de thesis. Ik ga er eens doorheen bladeren.

[Verwijderd]

En ook voor de gepromoveerde informaticus is het nog absoluut niet triviaal om een fatsoenlijk model te maken dat een correcte afspiegeling van de software zelf is.

Waarom kan het model dan niet automatisch worden afgeleid van de software zelf?

[sickyb]

In een wetenschappelijke of technische context is een model een vereenvoudigde voorstelling, beschrijving of nabootsing van (een deel van) de werkelijkheid. Een model kan formeel zijn (bijvoorbeeld een wiskundige vergelijking, een diagram of een tabel) of informeel (een beschrijving in woorden).

Met andere woorden een model is een simpelere voorstelling van de software.

Overigens is het best mogelijk om het model te creeeren vanuit de software zelf alleen worden die weer onleesbaar voor mensen.

Maar er zijn wel pakketten te verkrijgen voor bijvoorbeeld UML reverse engineering waar je Java code aanbied en waar UML diagrammen opgeleverd worden. Een hels karwij om die UML diagrammen vervolgens een beetj leesbaar te maken kan ik je vertellen.

Echter:. Als je complexere systemen hebt die met elkaar communiceren en samenwerken (bijvoorbeeld zoals in SETI@home, niet zo'n heel goed voorbeeld trouwens) is het niet goed te modeleren in welke toestand de verschillende systemen zijn. Stel je voor dat systeem A en systeem B beide 100 toestanden kennen. Dan kent het model waarin beide systemen zijn opgenomen al 100x100 = 10.000 toestanden als je nog meer processen in je systeem hebt loopt het aantal toestanden waarin het hele systeem zich kan bevinden heel snel in de miljarden. Het probleem van software is dat er dus toestanden zijn waarin het systeem (als geheel) niet in mag geraken, de illegale toestanden (je krijgt dan bijvoorbeeld een deadlock waarin meerdere systemen op elkaar wachten tot het oneindige) Met modelchecking kun je dus door modellen te maken van de afzonderlijke processen en deze als systeem bij elkaar te voegen al deze toestanden doorrekenen om uiteindelijk vast te stellen of de software mogelijk in een van deze toestanden kan geraken. Als het model niet in deze illegale toestanden kan geraken heb je de software goed ontworpen. (althans dat is het idee)

[Reactie gewijzigd door sickyb op 23 juli 2024 12:27]

[Verwijderd]

Maar als bij het maken van die modellen al fouten kunnen optreden, dan kan alsnog het hele systeem als een kaartenhuis in elkaar vallen.

[elvries]

Even reagerend op de opmerking dat leesbare diagrammen uit code genereren een hels karwei is, dat was vroeger inderdaad zo, met de moderne tooling (bijv. IntelliJ IDEA) is het een fluitje van een cent om een zeer overzichtelijk class diagram of ERD te genereren.

Behavorial diagrammen zoals sequence diagrammen zijn volgens mij inderdaad nog niet echt goed te doen.

[Wilke]

Als je wilt kun je z'n papers er zo op nalezen: hier kun je ze allemaal vinden en hier staan ze van de hele vakgroep.

Als een paper geaccepteerd is bij een conferentie of journal kun je er van uitgaan dat de abstract vrij goed uitlegd wat er nieuw aan is, dus je hoeft niet per se elk detail door te gaan spitten.

Btw: hoi Mark!

[Reactie gewijzigd door Wilke op 23 juli 2024 12:27]

[Chip.]

Als je trouwens wilt lezen wat zijn bijdrage is moet je 331 lezen van zijn thesis. Dat is onderdeel van een chapter waarin hij in jik en janneke taal uitlegd wat hij doet en wat zijn bijdrage is.

[Kaw]

Misschien is het mijn gebrek, maar wat is het verschil met een geautomatiseerde regressietest en dit verhaal? Met Markov introduceer je in feite een stukje willekeur in het pad wat wordt afgelegd, met een van te voren vastgestelde kans op een actie die hoort bij die context. Wellicht is het nuttig in situaties waar het aantal mogelijke stappen door de Curse of dimensionality te veel tijd gaat vergen en dat je in een afzienbare tijd toch de meest waarschijnlijke situaties getest hebt? Maar fouten uitsluiten kun je dan niet, want ergens in de ruimte van mogelijkheden zou er nog steeds een fout kunnen optreden.

Edit: http://tweakers.net/plan/crew/9 Verklaart ook meteen dat dit aangedikte nieuwsbericht een plekje kreeg op tweakers.net.

[Reactie gewijzigd door Kaw op 23 juli 2024 12:27]

[Dr.Root]

''Volgens Timmer kunnen hierdoor complexe systemen beter getest worden op fouten''

Dus dat sluit inderdaad niet uit dat er nog steeds fouten kunnen optreden. Wellicht kun je op deze manier fouten wel beter in kaart brengen of risico's verkleinen, zogenaamd ''Veiligheidsmarge''

Bepaald product X maakt zoveel kans op defect raken na 2 uur gebruik, dat ze hem nog vóór die 2 uur al vervangen ofzo..

[Garyu]

Het sluit wel degelijk mathematisch uit dat er nog steeds fouten kunnen optreden. Met een paar slagen om de arm

1) Hoe ga je om met oneindige oplossingsruimtes? Je kan een supercomputer jarenlang aan een model laten rekenen, maar ergens moet je een keer stoppen.

2) Hoe verifieer je de correctheid van een model? Is het een valide weergave van de software, of zitten er abstracties in die baseren op ongeldige aannames?

3) Hoe kan je de kosten beheersbaar houden? Hoe complexer de software, hoe complexer het model. Je bent dan al snel maanden zoniet jaren aan het modelleren, wat de kosten enorm laat exploderen. Er worden daarom keuzes gemaakt welke delen van software gemodelleerd worden en welke met behulp van andere model-gebaseerde of niet-model-gebaseerde testmethodes geevalueerd worden. Een compromis dus, en dat compromis is nooit perfect.

[sickyb]

Wat een BS bericht. Ik ben zelf 5 jaar geleden afgestudeerd op Model Checking.
Een tool als UPPAAL bestaat al sinds 1995 compleet met plugins voor de Eclipse ontwikkelomgeving.

Bovendien NASA gebruikt voor kritische software veelal theorem proving om de corectheid van de software te garanderen, Theorem proving is verwant aan model checking maar levert voor je software correctheidsbewijzen in plaats van de correctheid van je model te verifieren.
helaas is dat veel bewerkelijker.

Ik weet zeker dat de techniek van Model Checking niet heeft stilgestaan en ik neem aan dat Dhr Timmer een prima bijdrage heeft geleverd en dat hij meer verstand heeft van de huidige stand van zaken op het gebied hiervan dan ik maar het bericht hierboven heeft verder weinig nieuwswaarde hiervoor gaat het niet diep genoeg op de materie en de ontwikkelingen van de laatste jaren op dit gebied in.

Overigens toen Mark nog wel eens een artikel schreef voor T.net waren er nog regelmatig artikelen te vinden over in depth informatica (ja de WO universitaire informatica zooi die nog mijlenver van het bedrijfsleven staat en waar veel mensen het nut niet van inzien). Ik mis die artikelen. Waar is de die hard wetenschapsjournalist van tweakers die de wiskundige kant van de informatica niet schuwt. Af en toe een artikel met wat keiharde wiskunde erin kan toch geen kwaad? Ik mis die artikelen.

[Reactie gewijzigd door sickyb op 23 juli 2024 12:27]

[Rev-anche]

* sickyb Overigens toen Mark nog wel eens een artikel schreef voor T.net waren er nog regelmatig artikelen te vinden over in depth informatica (ja de WO universitaire informatica zooi die nog mijlenver van het bedrijfsleven staat en waar veel mensen het nut niet van inzien). Ik mis die artikelen. Waar is de die hard wetenschapsjournalist van tweakers die de wiskundige kant van de informatica niet schuwt. Af en toe een artikel met wat keiharde wiskunde erin kan toch geen kwaad? Ik mis die artikelen.

Dat lijkt me nou juist het probleem als Promovendus, de tijd vinden om alle tweakers gelukkig te houden

[Archimond]

Is model checking dan net zo sterk als de gedefinieerde parameters?
Dus bij een bepaald gegeven limiet gaat een materiaal kapot.

Alles wat door mensen wordt gemaakt hebben altijd fouten, hopelijk zal dit grote dure fouten helpen voorkomen. Raketten, waterkeringen en kerncentrales zijn duur en hebben grote gevolgen als het misgaat.

[Aardwolf]

Punt bij waterkeringen is wel dat je met veel meer variabelen moet rekenen, omdat deze "vaste" constructie toch erg gevoelig is op o.a. (lokale) plastische vervorming. Een stuk kerncentrale van gewapend beton zal daarentegen al heel anders reageren en is wat betreft materiaalsamenstelling veel consistenter dan bijvoorbeeld 100 meter dijkvak. Waterkeringen kan je niet exact benaderen, wel proberen, maar niet 99%.

Zo bestaan er bijvoorbeeld wel specialistische programma's (bijv. Plaxis) waarmee je de verwachte vervorming en stabiliteit kunt bepalen, welke dan werken volgens de eindige-elementenmethode (EEM of FEM, net wat je wilt). Maar de hoeveelheid input (waarvan ook weer aannames), de complexiteit van het model en de ervaring/deskundigheid die de man achter de computer moet hebben m.b.t. het juist interpreteren van de output is daardoor al bijna onwerkbaar voor kleine stukken waterkering waar bijvoorbeeld bijzondere (niet-grond) constructies zijn aangebracht. Laat staan dat je zoiets gaat doen voor duizenden kilometers waterkering in Nederland. Wie weet in de toekomst mogelijk, maar ik zie dat niet binnen nu en 5 jaar gebeuren.

EEM en varianten daarvan zijn slechts kansmodellen die het risico verminderen, maar 0% risico zal je daarmee dus ook nooit kunnen bereiken naar mijn mening. Of althans, in elk geval niet wanneer je dit wilt doen met het rare materiaal genaamd "grond". Grond is zo hetereogeen als maar kan. Wat je op dit punt hebt aangenomen als inputdata geldt bij wijze van 1 meter verderop al niet meer, zowel over de lengte, breedte als diepte gezien.

Een mooi stukje over de geschiedenis en toekomstvisie van EEM/FEM binnen de waterbouw met betrekking tot waterkerende grondconstructies: klik.

Wat er niet echt in staat is dat EEM huidig nog enkel vooral voor de bepaling van macrostabiliteit is en in mindere mate de micro-instabiliteit. Interne erosie van korrelmateriaal zit niet in dat model. Dus bijvoorbeeld de gevoeligheid en kans op falen door zandmeevoerende wellen (piping). Maar wie weet dat het in de toekomst best haalbaar is, techniek en ontwikkelingen staan immers niet stil. Ik denk ook wel dat door dergelijke ontwikkelingen als bijvoorbeeld van dhr. Timmer deze software en de toepassingsmogelijkheden wel de goede kant op gaat.

[Reactie gewijzigd door Aardwolf op 23 juli 2024 12:27]

[corset]

Het gaat voor mij echt veel en veel te diep. Maar toch vind ik het zeer interesant. Het is wel iets wat (met mijn beperkte kennis) toch heel nuttig kan zijn.

Ik ga hier toch wat meer over lezen, klinkt wel zeer goed.

Vooral de manier waarop wiskundige modellen gebruikt worden hiervoor.

[Elephtera]

Ik ben afgestudeerd op een deel/vervolg/afgeleide onderzoek van Marks onderzoeken, en daar kwam voornamelijk uit naar voren dat de op dat moment ingeslagen weg met model based testing niet de juiste was, omdat je theoretisch een goede afweging kon maken over welke testen en welke hoeveelheid, maar dat je dat in de praktijk niet of nauwelijks kon door rekenen (je liep tegen het schaak probleem aan, teveel mogelijke zetten, teveel berekenen, te duur om het met een nuttige diepte door te rekenen).
Ik heb het gevoel dat Mark met dit proefschrift ook dat bezwaar heeft aangepakt door op een andere manier met de kansen om te gaan. Maar daarvoor zou ik eerst het proefschrift moeten doorlezen.

[Dr.Root]

Geniaal! en zo weer een Nederlandse uitvinding rijker?

''Volgens Timmer kunnen hierdoor complexe systemen beter getest worden op fouten''

Dit is wel iets voor de Amerikaanse overheid. Kunnen zij eindelijk een betere risico analyse gericht op de fouten die het systeem van de NSA maakt en nog gaat maken. Grandioos