TIJD
14:00-14:45

TITEL
Ervaringen met formele engineering: modelgebaseerd specificeren, implementeren en testen van een softwarebus bij Neopost

SPREKER
Axel Belinfante, Universiteit Twente

ABSTRACT
In deze presentatie belichten we de actuele industriële inzet van formele methodes tijdens de ontwikkeling van een softwarebus. Bij Neopost hebben we de servercomponent van de zogeheten XBus ontwikkeld en daarbij formele methodes toegepast in de ontwerp-, validatie- en testfase: we hebben het design gemodelleerd in de procesalgebra MCRL2 en gevalideerd met de bijbehorende simulator en de implementatie volledig automatisch getest met de modelgebaseerde testtool JTorx.
Het resultaat is een goed geteste softwarebus met een onderhoudbare architectuur. Het schrijven en simuleren van het model en het testen van de implementatie nam zeventien procent van de totale ontwikkeltijd in beslag. De fouten die modelgebaseerd testen daarbij aan het licht heeft gebracht, zouden met conventionele testmethodes moeilijk gevonden zijn. Dit geeft aan dat formele engineering haalbaar, nuttig en kosteneffectief is.