Veel mensen lopen tegenwoordig rond met een Android-mobieltje of een Iphone. Voor beide platforms zijn al heel wat apps verschenen. Wat komt er zoal bij kijken om een app te porten van Android naar Iphone (of vice versa) als de software is gemaakt met een modelgebaseerde aanpak? Verum heeft dit onderzocht voor een bestaande machinebesturingsapplicatie. Uit dit experiment blijkt dat de vertaling eenvoudig en goedkoop is (65 procent in een halve dag) en dat het werk vooral zit in de handgeschreven code (35 procent in acht dagen).
Enkele jaren geleden hebben we bij Verum de machinebesturingssoftware gemaakt voor een waferinspectie-unit van het Duitse bedrijf Nandatech. Daarbij hebben we gebruikgemaakt van model-driven development (MDD). Om de MDD-manier van werken te kunnen demonstreren, hebben we met Lego Mindstorms een demo gebouwd van het systeem. Dit had als bijkomende voordeel dat we gelijk een deel van de werking konden valideren. Conceptueel doet het legobouwsel hetzelfde als de waferinspectie-unit: onder controle van een manufacturing execution system (Mes) krijgt het een batch van wafers aangeboden om te inspecteren, waarna het iedere plak controleert op een aantal kenmerken. Op basis van het inspectieresultaat keurt het systeem de wafer goed voor verdere productie, of af.
Het inspectieproces bevat concurrencyaspecten en vele discrete beslismomenten (bijvoorbeeld: schakelaar is wel of niet ingedrukt, motor heeft wel of niet positie bereikt), waar de software besluit wat de vervolgactie wordt op basis van de situatie. Het ’controle‘-aspect in de software (gedrag) is zo ingewikkeld dat het lastig is om dit met handgeschreven code te implementeren. Bovendien is het ondoenlijk om de correctheid van de software door testen te verifiëren en aan te tonen, en wel om twee redenen: ten eerste kost grootschalig testen zeer veel tijd en geld en ten tweede kun je geen gedrag testen dat je niet verwacht. Hierdoor is het onmogelijk om daadwerkelijk alles te testen. Daarom hebben we de software gemaakt met MDD op basis van formele verificatie.

