Visualisatie van formele modellen

Modellen worden geschreven in een domain specific language (de Axini Modeling Language) via een teksteditor in onze webapplicatie. De modellen kunnen worden gevisualiseerd om de states en transities van het onderliggende symbolische transitiesysteem te inspecteren. Wanneer een gebruiker op een state of transitie in de visualisatie klikt, navigeert de interface naar de bijbehorende plek in het tekstuele model. Dit helpt modelleurs hun modellen te begrijpen en erover te redeneren.

Een kleine, conceptueel eenvoudige visualisatie wordt al snel onoverzichtelijk door overlappende edges en labels. Modellen van echte systemen zijn doorgaans groot en complex. Verschillende visualisatietechnieken (of combinaties daarvan) zijn gewenst om beter te kunnen redeneren over zulke modellen.

Daarnaast kunnen bepaalde concepten in de modelleertaal, zoals parallellisme, synchronisatie, non-determinisme en tijd, nog niet effectief worden gevisualiseerd.

Het koppelen van de visualisatie aan de modeltekst is bovendien soms lastig wanneer modellen gebruikmaken van macro's, waarbij de feitelijke definitie van een deel van het model in een macro verstopt zit. De tool springt nu in de macro, maar gebruikers willen vaak juist zien wáár de macro wordt gebruikt. Een onderzoeksrichting is hoe je omgaat met source code-locaties bij gegenereerde code en metaprogrammering in het algemeen.

Een ander visualisatie-onderwerp is het visualiseren van coverage en testuitvoering. Gebruikers zien in de tool wel testcase-coverage en eindstates, maar niet hoe het systeem 'door het model heen liep' tijdens uitvoering. Een temporele visualisatie met video-player-achtige besturing zou gebruikers in staat stellen het executiepad af te spelen of stap voor stap te doorlopen.