Förbättrad mjukvarutestning med kodtäckning och formella metoder

Sammanfattning

Inom mjukvarutestning skapas ofta enhetstester som verifierar programmets funktion. Dessa tester är skapade för att upptäcka potentiella fel, vilket är särskilt viktigt inom säkerhetskritiska tillämpningar där fel kan leda till förödande konsekvenser. Kodtäckning är ett mått på hur stor andel av kod som har testats av ett testfall. Traditionella kodtäckningsmått mäter ofta hur stor andel av kod som har exekverats, vilket kan leda till att vissa typer av fel inte upptäcks. I detta arbete föreslås bevistäckning som alternativt mått på kodtäckning, vilket använder formella metoder och SMT-lösare för att markera logiskt relevant kod. Syftet är att upptäcka redundant kod och fel som exekveringsbaserade mått missar, och därmed öka kvaliteten på mjukvarutester. För att undersöka detta har de olika måtten jämförts i en mängd program skrivna i programmeringsspråket C, för att illustrera de mönster och skillnader som finns. För att besvara frågeställningarna har en matematisk formalisering konstruerats som beskriver program och de olika måtten i form av grafer. Sedan utvärderades metoderna på en mängd program för att se hur måtten kompletterar varandra. Arbetet avslutades med en prestandaevaluering för att evaluera den praktiska användbarheten hos bevistäckning. Resultatet visar att bevistäckning ofta täcker mindre kod än de traditionella måtten, och att det är ett strängare mått som visar vilken kod som faktiskt krävs för att assertions ska hålla. Genom att använda bevistäckning kan det fungera som ett komplement till de traditionella måtten. Det kan användas till att identifiera redundant kod som påverkar prestandan, men även att hitta kod som inte testas trots att den täcks av de traditionella måtten.