Een formele methode, maar tóch hanteerbaar

De medische tak van Philips raakte overtuigd van een ‘proof of concept’ van de Eindhovense startup Verum, die een formele methode (die software al in de ontwerpfase wiskundig verifieert) in een hanteerbaar product aan het verwerken is.

De Brit Robert Howe, CEO van Verum, vermijdt als het even kan de term ‘formele methode’. “Ik gebruik die term alleen als ik zeker weet tegen wie ik praat. Als categorie heeft het toepassen ervan al 20 jaar een slechte reputatie. Men vindt het complexer dan het probleem dat je probeert op te lossen. Men kent het als niet-schaalbaar. En het is alleen te begrijpen door zonderlinge experts. Maar wij hebben die drie problemen opgelost.”

Het product in wording van Verum heet Analytical Software Design (ASD), een combinatie van een aantal onderdelen die deels door Verum gehost wordt. Verum heeft ASD gebaseerd op een aantal oude elementen. ‘Sequence Based Specification’ (SBS), een door IBM ontwikkeld concept waarbij geen enkele gedraging van een systeem buiten beschouwing blijft, leidt tot een model dat in de procesalgebra CSP (Communicating Sequential Processes) wordt vertaald, ontwikkeld door Tony Hoare in de jaren ’80.
Bij die stap wordt ‘wiskundige compleetheid’ uitgebreid naar ‘wiskundige correctheid’ en in die vertaling ligt de belangrijkste octrooi-aanvraag van Verum. “CSP is obscuur, maar heeft de unieke eigenschap van ‘compositionaliteit’.” Dat wil zeggen dat als onderdelen van een complex systeem apart te verifiëren zijn, het gehele model ook gegarandeerd integer is. “Je software wordt wiskundig geverifieerde Lego”, zegt Howe. Daarmee is volgens hem het schaalbaarheidsprobleem opgelost.

ASD omvat ook een tool voor het controleren van de CSP-modellen, FDR (Failures-Divergences Refinement), dat ook al jaren bestaat en waarvoor Verum de exclusieve commerciële rechten net van het Britse Formal Systems heeft gekocht. “Je zegt bijvoorbeeld tegen de FDR modelchecker ‘Dit systeem kent geen illegal behavior’ en dat probeert het tool dan te falsifiëren.” Of, meer toegespitst op een röntgenmachine van Philips: “Je kunt het veiligheidspaneel van dit systeem niet verwijderen als het actief is.” FDR zal dan op alle mogelijke manieren nagaan of het softwaremodel nooit en te nimmer het openen van dat paneel zal toestaan.

Als een softwaremodel is geverifieerd, genereert ASD automatisch softwarecode in naar keuze C++, C#, of Java. Op dezelfde manier zijn ook de interfaces met externe handgeschreven code te realiseren.
ASD, als hanteerbare bundeling van deze op zichzelf lastig toe te passen concepten, is volgens Howe met name bedoeld voor complexe systemen waarin ‘discreet gedrag’ en processcommunicatie een grote rol spelen. Vaak gaat het daarbij om embedded software, waarin het maken van fouten achteraf duur kan uitpakken.
Naast de huidige pilotklanten, Philips Healthcare, Philips Applied Technologies en Nanda Technologies (dat inspectieapparatuur voor siliconen-wafers maakt) hoopt Howe dan ook bijvoorbeeld klanten in de automobielindustrie binnen te halen. Verums claim dat het aantal geschreven regels code voor dit soort toepassingen omhoog kan van 4 á 6 per manuur naar tussen de 13 en 80, is het grootste verkoopargument. “Dat lukt ons vooral omdat je met ASD bijna niets handmatig hoeft te coderen.”

Wim Pasman van Philips Healthcare ziet de voordelen van Verums technologie vooral in het beter kunnen standaardiseren van componenten en protocollen in de embedded software die het bedrijf maakt. “Onze systemen worden alleen maar complexer. We verwachten niet meteen wonderen, maar wel verbeteringen in de komende vijf jaar.”
Hij benadrukt het belang van een snelle systeemintegratie tussen de vele oude en nieuwe componenten die samen de software in de systemen van zijn bedrijf vormen. “Juist daar is het tot dusver moeilijk om aan te tonen dat er geen fouten in het gedrag van een systeem ontstaan.” Cijfers over het voorkomen van fouten durft Pasman nauwelijks te noemen, maar “de ervaring is dat we nu zeker 50 procent winst boeken.”

Verum bestaat een jaar of vier, maar mede-oprichter Guy Broadfoot is al sinds 1999 met het idee bezig. Nu komt het bedrijf in een stroomversnelling, na het binnenhalen van 3 miljoen aan durfkapitaal van Shatho Beheer en SenterNovem. In de loop van dit jaar moet het product – met name de SBS-editor die bij de klant zelf draait – vervolmaakt worden.
En Howe moet een nieuw businessplan schrijven, want een aanvullende module, het Compliance Testing Framework (CTF), dat controleert of externe conventionele softwarecomponenten wel goed samenwerken met ASD-software, blijkt door klanten veel belangrijker gevonden te worden dan gedacht. Ook moet Howe nog nadenken over hoe de klanten zullen gaan betalen voor hun gebruik van het systeem. “Ik denk dat we het aanpakken via de omvang van het model. Uiteindelijk gaat het voor de klant om de kosten per regel code. Nu is dat ruwweg 10 tot 15 euro. Ons doel is ergens tussen de 1,50 en 2,50 euro.”