Model checking van symbolische transitiesystemen

De formele theorie van model based testing maakt gebruik van Symbolic Transition Systems (STS), een vorm van labeled transition systems (LTS). Voor LTS-modellen heeft de academische wereld model checking-algoritmen ontwikkeld die kunnen controleren of modellen aan bepaalde eigenschappen voldoen. Met deze techniek kan het ontwerp van een systeem worden gevalideerd voordat het wordt gebouwd.

Model checking gebruikt zogenaamde Linear Time Logic (LTL) om eigenschappen uit te drukken die tegen het transitiesysteem worden gecontroleerd. Een LTL-eigenschap is een logische formule die bijvoorbeeld bereikbaarheid of veiligheid kan uitdrukken.

De modellen van Axini gebruiken symbolische transitiesystemen (STS), waarin ook data is opgenomen in de vorm van variabelen, toekenningen en condities. Dit verhoogt de expressiviteit en testkracht van onze modellen, maar maakt het lastig om de bestaande LTS-algoritmen uit de academische wereld toe te passen.

Een andere uitdaging is dat de model checker naadloos in onze tool moet kunnen worden geïntegreerd, zonder afhankelijkheden van componenten die niet in onze stack passen.

Bij Axini hebben we ruime kennis en ervaring in het bouwen van LTS-gebaseerde (zogenaamde explicit state) model checkers. Zo deed Dr. Ir. Machiel van der Bijl zijn promotie in de formele methoden-groep van de Universiteit Twente. We onderhouden contact met diverse onderzoeksgroepen aan universiteiten om je waar nodig te ondersteunen.