UniTESK teknologi

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 22. december 2020; verifikation kræver 1 redigering .

UniTESK (Unified Testing & specification toolKit) er en teknologi til test af software og hardware baseret på formelle specifikationer , udviklet ved Institut for Systemprogrammering ved Det Russiske Videnskabsakademi . Teknologien er en kombination af veletablerede teknikker, der kan anvendes i forskellige kombinationer, der gensidigt kombinerer og forstærker hinanden. Dette gør teknologien fleksibel og kan tilpasses eksisterende udviklingsprocesser på alle stadier af softwareudviklingens livscyklus fra kravindsamling og analyse til vedligeholdelse.

Grundlaget for at afgøre , om det testede systems opførsel er korrekt, er kontraktspecifikationer i form af forud- og efterbetingelser , skrevet i forlængelse af traditionelle programmeringssprog som C , Java og giver mulighed for at lave en dom helt automatisk. Specifikationer er en repræsentation af de funktionelle krav til et system. Specifikationernes form og dækningskriterierne baseret på dem sikrer sporbarheden af kravene .

Med succes anvendt i praksis kan teknikkerne til at konstruere test baseret på tilstandsgrafgennemgang betydeligt minimere mængden af manuelt oprettet programkode , samtidig med at de sikrer diversiteten og massiviteten af testsættet.

Dataabstraktionsteknikker og kravbaserede dækningskriterier muliggør fleksibel kontrol over testsættets størrelse og direkte generering for at dække specifikke krav, og derved minimere testsættets udførelsestid.

Et særligt mellemlag tilgængeligt i teknologien giver dig mulighed for hurtigt at tilpasse testpakken til forskellige implementeringer med samme funktionalitet.

Alle disse teknikker giver test af høj kvalitet, sporbarhed af krav og et højt niveau af genbrug af testsuite-komponenter med et minimum af manuelt arbejde og acceptabel testudførelsestid.

Teknologitrin

Definition af den del af systemet, der testes På dette trin bestemmes den testede funktionalitet, det vil sige en del af mulighederne i det undersøgte system, som skal testes, og den testede grænseflade, det vil sige måden at få adgang til de testede muligheder. Definition og analyse af krav til det system, der testes Baseret på analyse af alle inputdata, kommunikation med kunden, eksperter og brugere, identificeres og systematiseres kravene til det system, der testes. Som yderligere præsenteres i form af en formel model. Definition og analyse af krav til fuldstændighed af test Testfuldhedskriterier er fremhævet, som afspejles i den formelle model. Test udvikling Udvikling af testdatakilder og testmodel generelt.
Grundlæggende teknikker .
Optælling af endelige mængder, optælling af kombinationer, optælling af grænseværdier og dem tæt på dem, optælling af nodale og tætte værdier, optælling af grammatiske strukturer ved hjælp af modulære generatorer, opregning med filtrering, optælling af tilskrevne grafer og sekvenser.
Finite automater, mærkede overgangssystemer, implicit repræsentation af automatmodeller, lag-for-lag test af komplekse modeller. Udvikling af adaptere, der binder test til implementeringen under test Fejlretning og kørsel af tests Analyse af testresultater

Oprettelseshistorie

I 1994 udviklede Institut for Systemprogrammering ved Det Russiske Videnskabsakademi (ISP RAS) under en kontrakt med Nortel Networks en metodologi og et sæt værktøjer til automatisering af applikationsprogramgrænsefladetest (API) . Den første praktiske anvendelse af metoden var kernen i realtidsoperativsystemet.
I løbet af 1994-1999 oprettede og installerede ISP RAS adskillige versioner af KVEST-1-teknologi i Nortel Networks.
I 1998-1999 blev skabelsen af KVEST-2-teknologien afsluttet.
I 2000 blev KVEST-teknologien tilpasset til brug i C- og C++- projekter .
I 1999 begyndte ISP RAS at udvikle en ny generation af verifikationsteknologi - UniTESK (Unified Testing & specification toolKit).

Anvendelse i praksis

Teknologien er med succes blevet anvendt i mange projekter. Mest interessant:

Åbn Linux -verifikation ( OLVER ) (siden 2005);
Test af integrations- og faktureringskomponenter i VimpelCom (siden 2007);
Test af den mobile implementering af IPv6 -protokollen (2002-2003, 2 årsværk);
Objektmæglertest (2000, 1 årsværk) ;
ATM Framework- komponenttest (1999-2000, 6 årsværk);
Test og redesign af applikationsstøttesystemet (1998-1999, 2 årsværk);
Kerneltest af operativsystem (1994-1997, 25 årsværk).

Instrumentel støtte

CTESK er et værktøj til test af software implementeret i C -sproget .
CTESK Community Edition er en gratis, fuldt funktionel version af CTESK-værktøjet til Linux -platformen .
JavaTESK er et værktøj til test af software implementeret i Java-sproget .
C++TESK er et værktøj til at teste software implementeret i C++ sproget , såvel som modeller af synkront digitalt udstyr i hardwarebeskrivelsessprog .
Pinery - designet til at generere testdata af en kompleks struktur baseret på beskrivelser i form af grammatikker (sådanne beskrivelser inkluderer for eksempel BNF , regulære udtryk , DTD osv.).
OTK (Optimizer Testing Kit) er et værktøj til test af softwaresystemer, der arbejder med data, der har en kompleks struktur. Brugen af OTK er mest effektiv ved test af compilere eller andre formelle tekstbehandlingssystemer. Hovedvægten i OTK er på at opbygge en række forskellige inputtestdata.
SynTESK (Syntax Testing Kit) er et værktøj til at teste parsere (parsere) af formelle sprog. SynTESK giver dig mulighed for at kontrollere overensstemmelsen af parserens implementering og specifikationen af et givet formelt sprog, det vil sige at parseren genkender dette særlige formelle sprog.
MicroTESK (Microprocessor Testing Kit) er et værktøj til automatiseret udvikling af testprogramgeneratorer til mikroprocessorer og andre programmerbare enheder.

Litteratur

Kulyamin V. V. . Testdækningskriterier baseret på strukturen af kontraktspecifikationer // Proceedings of ISP RAS, UniTESK Approach: Results and Perspectives. 14(1):89-107, 2008 [1]
Grinevich A. I. , Kulyamin V. V. , Markovtsev D. A. , Petrenko A. K. , Rubanov V. V. , Khoroshilov A. V. Brug af formelle metoder til at sikre overholdelse af softwarestandarder // Proceedings of ISP RAS, Leveringspålidelighed og kompatibilitet af Linux-systemer. 10:51-68, 2006 [2]
Burdonov I.B. , Kosachev A.S. , Kulyamin V.V. Ikke-redundante rettet grafgennemløbsalgoritmer: ikke-deterministisk kasus //Programmering. 30(1):2-17, 2004 [3]
Burdonov I.B. , Kosachev A.S. , Kulyamin V.V. Brug af finite state-maskiner til at teste programmer //Programmering. 26(2):61-73, 2000 [4]
Bourdonov I. , Kossatchev A. , Kuliamin V. og Petrenko A .. UniTesK Test Suite Architecture // Proc. af FME 2002. LNCS 2391, s. 77-88, Springer-Verlag, 2002. ISBN 3-540-43928-5
Bourdonov IB , Demakov AV , Jarov AA , Kossatchev AS , Kuliamin VV , Petrenko AK og Zelenov SV . Java-specifikationsudvidelse til automatiseret testudvikling //Proceedings of PSI'2001. Novosibirsk, Rusland, 2.-6. juli 2001. LNCS 2244:301-307, Springer-Verlag, 2001. ISBN 978-3-540-43075-9 [5] (link ikke tilgængeligt)
Bourdonov I. , Kossatchev A. , Petrenko A. og Galter D .. KVEST: Automatiseret generering af testsuiter fra formelle specifikationer //FM'99: Formelle metoder. LNCS 1708, Springer-Verlag, 1999, pp. 608-621. ISBN 3-540-66587-0 [6] (utilgængeligt link)