Reading time: 3 minutes
Author:
Verum heeft zijn Dezyne-tooling voor modelgedreven software-engineering gereviseerd. Het Waalrese bedrijf heeft de FDR-modelchecker onder de motorkap vervangen door de MCRL2-modelchecker van de TU Eindhoven. De nieuwe engine presteert nu al beter dan zijn voorganger en biedt een platform waarmee in de toekomst grotere, complexere problemen zijn te verifiëren, zelfs functioneel, aldus Verum. De nieuwe Dezyne-release, versie 2.8.0, komt vandaag beschikbaar.
FDR (Failures-Divergences Refinement) checkt modellen die zijn opgesteld in de formele taal CSP (Communicating Sequential Processes), bedacht door de vermaarde Britse informaticus Tony Hoare. De technologie is ontwikkeld door Formal Systems uit Oxford. Latere versies zijn doorontwikkeld door de plaatselijke universiteit, waar het bedrijf uit is voortgekomen.
In 2008 verleende Formal Systems aan Verum het exclusieve recht om FDR te gebruiken als motor van zijn tooling om software te controleren op correctheid. In 2011 sloten beide partijen een licentieovereenkomst, waarmee het Waalrese bedrijf versie 2.83 mocht distribueren, openbaar maken en bewerken. In 2013 volgde een dienstverleningsovereenkomst met de universiteit van Oxford om versie 2.94 te verspreiden en te gebruiken voor intern onderzoek.
Door een zakelijk geschil vertroebelde de relatie, met als gevolg dat de licentieovereenkomst in 2015 niet werd verlengd. Dat zadelde Verum op met een enorm probleem, aangezien het voor zijn bedrijfsvoering afhankelijk was van de technologie uit Oxford. Uiteindelijk belandde het met Formal Systems voor de rechter. Die stelde het Waalrese bedrijf vorig jaar in het gelijk en wees de Britse vordering tot staking van het gebruik van FDR2 af.
Begin 2014 was Verum echter al gaan uitkijken naar een alternatief en een samenwerking gestart met informaticahoogleraar Jan Friso Groote en zijn vakgroep aan de TUE. Doel: het door hem ontwikkelde MCRL2 integreren in de tooling uit Waalre, ter vervanging van FDR2. Voor het project verwierf Verum financiële ondersteuning uit meerdere bronnen, waaronder het Europese Zevende Kader-initiatief Tetracom (Technology Transfer in Computing Systems) en het Innovatiekrediet van RVO. Het resultaat is het MCRL2-gebaseerde Dezyne 2.8.0.
MCRL2 (Micro Common Representation Language 2) is een procesalgebra, een wiskundige taal om te redeneren over wat er gebeurt in een systeem met aan elkaar gekoppelde processoren of computers. De algebra beschrijft hoe toestanden veranderen in dit geheel. MCRL2 houdt daarbij rekening met data en het tijdsaspect. De technologie kent al verschillende industriële toepassingen, van de verificatie van signalering op het spoor tot de analyse van de controlesystemen van de Large Hadron Collider bij Cern.
‘De TUE staat veel dichter bij ons dan Oxford’, verklaart Verum-ceo Rob Howe de overstap naar MCRL2. ‘Niet alleen in fysieke afstand, maar ook in technologie en businessfilosofie: het kernteam van Verum is opgegroeid met MCRL2 en het is een opensource tool, waardoor we geen lastige discussies hoeven te voeren over licenties – de TUE is zelfs bereid om een service level agreement af te sluiten met ons. We hebben de afgelopen jaren een solide relatie opgebouwd, die een veel betere dynamiek geeft.’
Behalve de gloednieuwe verificatiemotor verandert er niks voor Dezyne-gebruikers. Versie 2.8.0 is volledig achterwaarts compatibel met de laatste FDR2-gebaseerde release 2.6.x. Verum heeft wel extra functionaliteit toegevoegd voor de beschrijving van concurrent gedrag, alsook het online aanbod aan documentatie, tutorials, usecases en voorbeelden uitgebreid.
