Snabbast

Fastest är ett modellbaserat testverktyg som fungerar med specifikationer skrivna i Z-notationen . Verktyget implementerar ( Cristia & Rodriguez Monetti 2009 ) Test Template Framework (TTF) som föreslagits av Phil Stocks och David Carrington i ( Stocks & Carrington 1996 ).

Användande

Snabbast presenterar ett användargränssnitt på kommandoraden. Användaren måste först ladda en Z-specifikation skriven i LaTeX- format som verifierar ISO- standarden ( Z Standard 2002) . Sedan måste användaren ange en lista över de operationer som ska testas samt de testtaktik som ska tillämpas på var och en av dem. I ett tredje steg genererar Fastest testträdet för varje operation. Efter att testträd har genererats kan användare bläddra i dem och deras testklasser och, ännu viktigare, de kan beskära vilken testklass som helst både automatiskt eller manuellt . När testträd har beskärs kan användare instruera Fastest att hitta ett abstrakt testfall för varje löv i varje testträd. ( Cristia, Rodriguez Monetti & Albertengo 2009 )

Testa taktik som stöds av Fastest

För närvarande, ^{[ när? ]} Snabbast stöder följande testtaktiker:

Disjunktiv normalform (DNF). Det är den enda testtaktiken som tillämpas som standard (oavsett om användaren har lagt till andra testtaktiker eller inte) och den första som ska tillämpas.
Standardpartitioner (SP). Användaren kan lägga till, modifiera och ta bort standardpartitioner för valfri fördefinierad Z matematisk operator genom att helt enkelt redigera en textfil ( Cristia, Rodriguez Monetti & Albertengo 2009 ) harv .
Gratis typer (FT)
In Set Extension (ISE)
Korrekt delmängd av Set Extension (PSSE)
Delmängd av Set Extension (SSE)

Beskärning testar träd i Fastest

Snabbast ger två sätt att beskära testträd ( Cristia, Rodriguez Monetti & Albertengo 2010) :

Automatisk beskärning.

För att beskära ett testträd analyserar Fastest predikatet för varje blad för att avgöra om predikatet är en motsägelse eller inte. Eftersom det här problemet inte går att avgöra implementerar verktyget en algoritm för bästa ansträngning som kan förbättras av användarna. Den viktigaste aspekten av algoritmen är ett bibliotek av så kallade elimineringssatser som var och en representerar en familj av motsägelser. Detta bibliotek kan utökas av användare genom att helt enkelt redigera en textfil. Elimineringssatser är konjunktioner av parametriska Z-atompredikat.

Manuell beskärning.

De snabbaste användarna kan beskära underträd eller enskilda löv av testträd genom att utfärda två kommandon. Dessa kommandon kommer att beskära alla testklasser i underträdet oavsett om de är tomma eller inte. Huvudsyftet med dessa kommandon är att tillåta ingenjörer att minska antalet eller att eliminera oviktiga testfall.

Hur snabbast hittar abstrakta testfall

Verktyget hittar abstrakta testfall genom att beräkna en finit modell för varje blad i ett testträd ( Cristia & Rodriguez Monetti 2009) . Finita modeller beräknas genom att begränsa typen av varje VIS- variabel till en finit uppsättning och sedan genom att beräkna den kartesiska produkten mellan dessa uppsättningar. Varje bladpredikat utvärderas på varje element i denna kartesiska produkt tills man uppfyller predikatet (vilket betyder att ett abstrakt testfall hittades) eller tills det är uttömt (vilket betyder att antingen testklassen är otillfredsställande eller att den finita modellen är otillräcklig ) . I det sista fallet har användaren chansen att hjälpa verktyget att hitta rätt finita modell eller att beskära testklassen eftersom den är otillfredsställande.

Arkitektur och teknik

Fastest är en Java- applikation baserad på Community Z Tools -projektet (CZT) . Verktyget kan användas i ett av två lägen ( Cristia & Rodriguez Monetti 2009) :

I distribuerat läge fungerar Fastest som en klient-serverapplikation . Applikationen kan installeras på ett antal datorer som var och en fungerar som klient, server eller båda. Användare kommer åt applikationen via klienter som skickar testklasser till servrar (kallade testservrar ) som försöker hitta ett abstrakt testfall ur dem. På så sätt fördelas den tyngsta uppgiften på så många datorer som möjligt. Eftersom beräkningen av ett abstrakt testfall från en testklass är helt oberoende av varandra, snabbar denna arkitektur upp hela processen proportionellt med avseende på antalet testservrar.
I applikationsläge är varje instans av Fastest helt oberoende av varandra. Alla uppgifter beräknas i den lokala datorn.

Lägger till ny testtaktik

Som framgår av TTF- presentationen är testtaktik väsentliga för metoden. De är verktygen som ingenjörer måste använda för att skapa så upptäckande testfall som möjligt. Sedan, ju fler ljudtestningstaktik tillgängliga för ingenjörer desto bättre.

I Fastest kan användare lägga till sin egen testtaktik genom att implementera Tactic- gränssnittet som verktyget tillhandahåller. Det här gränssnittet har metoder för att konfigurera och tillämpa testtaktik. Gränssnittsdefinitionen är följande:

 

 
 
 
 





   
    
    





       
    
    



       
    
    



        
    
    



       
    
    



      
    
    




       
    
    



       
    
    



      
    
    


    
      
    
    



       
 paket  client.blogic.testing.ttree.tactics  ;  importera  java.util.*  ;  import  net.sourceforge.czt.z.ast.Spec  ;  importera  common.z.TClass  ;  importera  common.z.OpScheme  ;  /**  * Gränssnitt som abstraherar en testtaktik (behövs för att generera testträd) och  * gör det möjligt att applicera den på en testklass för att generera nya.  */  public  interface  Tactic  {  /**  * Tillämpar denna taktik på den angivna testklassen och returnerar listan med *  de genererade testklasserna.  * @param tClass  * @return  */  public  List  <  TClass  >  applyTactic  (  TClass  tClass  );  /**  * Ställer in specifikationen för systemet som testas.  * @param opScheme  */  public  void  setSpec  (  Spec  spec  );  /**  * Hämtar Z-schemarutan för operationen som testas.  * @return  */  public  Spec  getSpec  ();  /**  * Ställer in Z-schemarutan för operationen som testas.  * @param opScheme  */  public  void  setOriginalOp  (  OpScheme  opScheme  );  /**  * Hämtar Z-schemarutan för operationen som testas.  * @return  */  public  OpScheme  getOriginalOp  ();  /**  * Analyserar parametrarna för denna taktik.  * @param str  * @return  */  public  boolean  parseArgs  (  String  str  );  /**  * Ställer in instansen av TacticInfo som är kopplad till detta objekt.  * @param tacticInfo  */  public  void  setTacticInfo  (  TacticInfo  tacticInfo  );  /**  * Hämtar instansen av TacticInfo som är kopplad till detta objekt.  * @return  */  public  TacticInfo  getTacticInfo  ();  /**  * Får beskrivningen av denna taktik.  * @return strängen med beskrivningen av denna taktik.  */  public  String  getDescription  ();  /**  * Ställer in beskrivningen av denna taktik.  * @param description  */  public  void  setDescription  (  String  description  );  }

Se även

Anteckningar

Cristiá, Maximiliano; Rodríguez Monetti, Pablo (2009). "Implementera och tillämpa Stocks-Carrington-ramverket för modellbaserad testning". Formella metoder och mjukvaruteknik, 11:e internationella konferensen om formella ingenjörsmetoder, ICFEM 2009 . Rio de Janeiro, Brasilien: Springer-Verlag .
Aktier, Phil; Carrington, David (1996), "A framework for specification-based testing", IEEE Transactions on Software Engineering , 22 (11): 777–793, doi : 10.1109/32.553698 .
Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (1 MB PDF) ( ISO/IEC 13568:2002 ed.), 2002, s. 196 sidor {{ citation }} : Extern länk i |edition= ( hjälp ) .
Cristiá, Maximiliano; Albertengo, Pablo; Rodríguez Monetti, Pablo (2010). "Beskärning av testträd i ramverket för testmall genom att upptäcka matematiska motsägelser". 8:e IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2010 . Pisa, Italien: IEEE .