Het CTIT waarvoor Huisman werkt, is een onderdeel van de Universiteit Twente. De onderzoeker gaat proberen met wiskundige modellen ervoor te zorgen dat software vaker foutloos ontwikkeld wordt. Dat gebeurt gedeeltelijk ook met programmeertaal Java, maar de onderzoeker wil die techniek uitbreiden en toepasbaar maken voor andere soortgelijke programmeertalen.
Multi-core processoren
'Computers worden steeds sneller en kunnen steeds meer', aldus Huisman. 'Toch lijkt de grens zo langzamerhand bereikt te zijn. Het is niet meer mogelijk om processoren nog sneller te laten werken.' Om dat probleem op te lossen, zouden steeds vaker multi-core processoren gebruikt worden om tegelijkertijd berekeningen te doen. Om ervoor te zorgen dat een programma goed werkt, moet de software op de processor beschrijven welke berekeningen tegelijkertijd gedaan kunnen worden. Daar gaat volgens Huisman nog wel eens iets mis. Haar onderzoek moet daar dus verandering in brengen.
De ERC kijkt bij het toekennen van de subsidie naar de inhoud van het onderzoeksvoorstel en de kwaliteiten van de onderzoeker.
Marieke Huisman
Huisman is onderzoeker bij de vakgroep Formal Methods & Tools van de faculteit Elektrotechniek, Wiskunde en Informatica en het onderzoeksinstituut CTIT. Ze werkt sinds 2008 aan de Universiteit Twente. Voordat ze in Twente kwam, deed ze onder andere onderzoek bij een onderzoeksinstituut in Frankrijk en aan de Radboud Universiteit in Nijmegen.
Reacties
yeah right!!
Wat een geldverspilling weer.
Dit is technologie die al dik dertig jaar bestaat.
Hij wordt echter niet toegepast omdat deze voor de gewone sterveling niet te volgen is en bovendien slechts beperkt inzetbaar is, zaken als interrupts en multi-threading kun je aleen met gezond verstand in de hand houden.
En dan ook nog eens die wetenschap proberen toe te passen op JAVA ???? laten we dan eerst eens proberen java eenduidig en stabiel te krijgen zodat het met elke jve behoorlijk behoorlijk en liefts ook een beetje snel werkt.
Er worden me wat onderzoekjes en promoties bedacht zeg.
Wiskundige modellen? Doen we dat niet al met o.a. beslistabellen en andere technieken?
Fouten voorkomen door risico's in een vroeg stadium bekend te maken heeft meer te maken met de project aanpak en gekozen teststrategie.
"foutloos" is een utopie. Wij testers vinden altijd wel fouten. Ik vind het jammer om te lezen dat onze branche onderschat en niet serieus genomen word (zo ervaar ik het na het lezen van ditartikel).
Hoewel geautomatiseerd risico's inzichtelijk maken (dat wordt er onderzocht naar mijn mening op basis van bovenstaand artikel) is niet hetzelfde al foutloze software.
@Tester2
Onderschat jij dat universitair onderzoek dan niet ?
De titel van het artikel zal wel bedacht zijn door Computable, verderop in het artikel wordt het al een stuk genuanceerder.
Wat verstaan we onder 'foutloos'? Is dat software zonder technische gebreken (bugs) of foutloos in de meer functionele zin van het woord?
Anders geredeneerd: mislukken de meeste IT-projecten als gevolg van technische mankementen of ongeschiktheid voor de gebruikersorganisatie?
@ onderzoeker
Ik denk dat je gelijk hebt dat ik het onderschat. De titel van Computable is jammerlijk te noemen. Ik zal dieper in de details van het onderzoek moeten kijken, want het zou ook zeker waarde kunnen toevoegen (anders krijgen ze natuurlijk geen subsidie). Wetenschappelijke onderbouwing zie ik graag, dus ik hoop dat Computable hier zeker een follow-up artikel over doet.
Foutloos in de zin van verificatie is wel mogelijk, in de zin van validatie zal dat erg lastig zijn ivm communicatie problemen tussen mensen...
Er is een Nederlands bedrijf dat een tool aanbiedt (genaamd Verum Software technologies), niet alleen voor Java, maar ook voor C#, C++ en C welk nu al foutloos gedrag garandeert. Klanten en partners als Philips, Ericsson, CCM, Task24, Logica en vele andedren maken hier reeds gebruik van.
Verum heeft hierop reeds Europees patent en sinds kort ook in Hong Kong (USA etc is in aanvraag).
Het is een maand gratis te proberen:
http://www.verum.com/testdrive
Hmm, interessant. Het paralleliseren van control software is inderdaad door Verum al flink makkelijk gemaakt met behulp van formele methoden. Het paralleliseren van number crunching C applicaties heeft VectorFabrics onder de knie. Ben zeer benieuwd wat dit onderzoek toevoegt.
@Tester2: het maken van foutloze software, dwz de software doet volledig wat de spec vraagt is wel degelijk mogelijk mbv formele methoden. Knappe jongen (tester) die daar nog fouten in vindt. Of het dan is wat de klant wil is nog een tweede ...
@ Arjen
Ik ben het met je eens. Misschien mijn stelling in een andere vorm. Het niet kunnen vinden van fouten is geen garantie dat het foutloos is. Dus foutloze software maken kan mischien wel. Maar het is niet te bewijzen omdat er zoveel (direct/ indirecte) invloedfactoren zijn. Dat de kans op vinden van fouten nihil is, maakt het nog niet foutloos. Het liefst gebruik ik het woord niet omdat het woord verkeerde verwachtingen schept. Zo hetzelfde met het woord "succesvol".
Ik zeg nooit dat een stuk software werkt. Ik zeg altijd dat het LIJKT te werken. Blijf altijd scherp en kritisch, ook als de software "foutloos" lijkt!!!
Fouten kunnen ook functioneel zijn, en derhalve bestaat foutloos niet.
Louter om commerciele redenen is niemand geintereseerd in correcte software.
Fouten vereissen updates, updates vereisen facturabele uren.
In een wereld waarin hele bedrijfsnetwerken instorten omdat een medewerker een verkeerde website heeft bezocht boeit het niemand of er een lompe fout in software zit.
Men (ook computable) neemt het allemaal wat te letterlijk.
Er is een moeilijk technisch probleem, dat met software te lossen is, bijv programmeren in een multi processor/core omgeving. Men verzint een oplossing/algoritme en gaat dat met een formele methode ( http://nl.wikipedia.org/wiki/Formele_methoden ) onderbouwen. Men kan dan bewijzen dat het algoritme correct is.
Ik kan me voorstellen dat Google voor hun zoekmachines ook van formele methoden gebruik heeft gemaakt.
Misschien gaat er nog van alles fout, zoals implementatie van het algoritme (coding), of een waarde te groot om in geheugen te passen (runtime) als dat niet meegespecificeerd is in algoritme, compiler die rotte machinecode maakt (fout in compiler zelf), van alles dus.
De titel en veel reacties suggeren dat men denkt dat een programma even door een generiek filter programma wordt gehaald, waarbij alle errors automatisch worden verwijderd.
@Pascal
Jij geeft precies aan waarom sommigen (waaronder ik) een gruwelijke hekel beginnen te krijgen aan uitbesteden van software. "Fouten vereisen updates, updates vereisen facturabele uren."
Dit is de meest onprofessionele uitspraak in jaren op dit forum!
Als je met professionele systemen werkt, dan ga je hier echt wel anders mee om.
Wat denk je dat het kost als je in een productieproces machines uit moet gaan zetten omdat iemand een foutje heeft laten zitten onder het mom van "als ik nog een paar updates kan maken, heb ik weer wat facturabele uren"
Denk je dat ziekenhuizen blij worden als je hun MR of Röntgenkamers plat moet leggen omdat jij nog wat bugs in de software had laten zitten om ook volgend jaar nog werk te hebben?
En met een installed base van duizenden machines wereldwijd, wat denk je wat het kost om naar al die plaatsen een engineer te sturen om het systeem aan te passen, omdat jij te weinig geheugen gedimensioneerd had voor dat systeem ?
Om nog maar niet te spreken van reputatie-schade. Door een houding als de jouwe, hebben afgelopen jaar veel autobedrijven voertuigen terug moeten halen om "bugs" op te lossen.
Als je kijkt naar de bedrijven die momenteel met Verum werken, zie je dat dat allemaal bedrijven zijn die machines leveren met hoge beschikbaarheid en betrouwbaarheid. Voor de controllers / statemachines die hun ontwerpen, biedt de oplossing van Verum grote voordelen. Deze bedrijven gaan echt niet over één nacht ijs voordat ze met een bedrijf als Verum in zee gaan.
Inderdaad testers worden onderschat,
offf worden ze juist overschat?
Zijn het niet de stadswachters die zich als politie voordoen ?
@PaVaKe. Pascal zegt niet dat ontwikkelaars expres fouten maken om volgend jaar ook nog wat te doen te hebben. De commercie zorgt ervoor dat foutloze software geen vereiste is. Al helemaal niet in niet-kritieke omgevingen. Zolang fouten en updates een acceptabel iets blijven zullen er fouten gemaakt blijven worden. Updates en testers (no offence) zijn gevolgen van het feit dat er fouten gemaakt worden en (in veel te hoge mate) geaccepteerd worden. Als je een huis oplevert met een lekkend dak hoef je niet aan te komen met een extra factuur vd dakbedekker, maar in de software wereld is dat heel normaal.. absurd toch?
Van Verum heb ik niet zo'n hoge pet op. Wat ze hebben gemaakt is een tool waarin je in een spreadsheet vorm je state diagram kunt inkloppen waaruit dan weer code gegenereerd wordt. Maw je maakt geen 'programmeer' fouten meer omdat je niet meer aan het programeren bent. Je kunt natuurlijk wel fouten maken bij het verkeerd invoeren van je state diagram in die spreadsheet maar de meeste zullen wel gedetecteerd worden omdat er dan inconsistenties ontstaan. Echter is het bij lange na niet de heilige graal die zijn claimen te hebben ontdekt. Want afgezien van een PLC besturing ben ik nog maar weinig software tegengekomen die alleen maar met state diagrammen te beschrijven valt.