Terug naar studenten

Formele methoden & verificatie

Requirements coverage

Modellen worden meestal geschreven op basis van dezelfde specificaties en requirements-documenten die traditioneel worden gebruikt om het systeem te ontwikkelen. Deze worden geschreven door architecten of domeinexperts en beschrijven het gewenste gedrag in natuurlijke taal. Om te verifiëren dat het systeem aan alle requirements voldoet, moeten we ervoor zorgen dat alle requirements gemodelleerd zijn én gedekt worden door de gegenereerde testgevallen.

Het Axini Modeling Platform heeft een feature genaamd scenarios, waarmee je gewenst gedrag kunt uitdrukken als een soort 'reguliere expressies op testgevallen'. Toekomstig onderzoek zou kunnen kijken hoe testgevallen zo snel mogelijk gegenereerd kunnen worden om deze scenario's te dekken, of hoe automatisch model-checked kan worden of ze in de modellen zelf zijn opgenomen.

Daarnaast is de regex-achtige aanpak vrij beperkt en kan deze niet alle (natuurlijke taal-)requirements uitdrukken die we in de praktijk zien. We zijn benieuwd of een alternatieve aanpak met (linear time) logica-formules gebruikt kan worden om requirements uit te drukken.

Een interessante invalshoek is de relatie tussen de populaire BDD-aanpak (Behavior Driven Development) en Axini Scenarios. Mogelijk kunnen die automatisch worden geconverteerd.

Mogelijke onderzoeksvragen

  1. 1

    Testgeneratie vanuit scenario's

    Hoe kunnen testgevallen worden gegenereerd op basis van requirements die als scenario's zijn uitgedrukt?

  2. 2

    Model checking van scenario-inclusie

    Hoe kan een model worden gecontroleerd op of alle scenario's daarin opgenomen zijn?

  3. 3

    Formaliseren van requirements

    Hoe kunnen requirements worden uitgedrukt zodat ze bruikbaar zijn voor testcasegeneratie en/of coverage-analyse?

  4. 4

    Requirements als logica-formules

    Hoe kunnen requirements worden uitgedrukt als (linear time) logica-formules?

  5. 5

    Automatische conversie van BDD-voorbeelden naar AMP Scenarios

    BDD-voorbeelden worden in de praktijk veel gebruikt. Is het mogelijk om deze (semi-)automatisch te converteren naar Axini Scenarios?

Interesse in dit onderwerp? Neem contact op!

students@axini.com