Abstrakt. Webbtjänster är mycket distribuerade program och är därför benägna att konvergera-relaterade fel. Modellkontroll är en kraftfull teknik för att identifiera brister i samtidiga system. De befintliga modellkontrollerna har dock endast ett mycket begränsat stöd för de programmeringsspråk och kommunikationsmekanismer som används vid typiska implementeringar av webbtjänster. Detta kapitel presenterar en formalisering av kommunikationssemantik inriktad på webbtjänster, och ett automatiserat sätt att extrahera formella modeller från program som implementerar webbtjänster för automatisk formell analys. De formella modellerna analyseras med hjälp av en symbolisk modellkontroll som implementerar automatisk abstraktion förfining. Vår implementation tar ett eller flera PHP5-program som indata och kan verifiera gemensamma egenskaper hos dessa program som körs samtidigt. Webbtjänster är momentiationer av tjänsteorienterade arkitekturer, där en tjänst är en funktion som är väl definierad, fristående och inte är beroende av sammanhanget eller tillståndet för andra tjänster [1]. De är utformade för att publiceras, nås och användas via intranät eller Internet. De delar av konstruktionen är 1) en tjänsteleverantör, som erbjuder vissa tjänster; 2) en tjänstemäklare som upprätthåller en katalog över tillgängliga tjänster; och 3) tjänsteleverantörer som söker en tjänst från tjänstemäklaren, och sedan bifoga till tjänsteleverantören genom att komponera de erbjudna tjänsterna med sina egna komponenter. En webbtjänst erbjuder en godtycklig komplex funktionalitet, som beskrivs i en global systemstruktur. Exempel på webbtjänster är informationssystem som kart- eller resetjänster, e-handelssystem som webbbutiker, resebyråer, aktiemäklare osv. Det är uppenbart att det är viktigt att se till att säkerhets- och säkerhetskraven efterlevs vid utvecklingen av sådana system. Webbtjänster genomförs vanligtvis på ett mycket distribuerat sätt och är därmed benägna att fel orsakade av distributionen. De involverar ofta flera parter. Som ett exempel kan du se en webbutik som accepterar avgifter till ett kreditkort som betalningsform. De berörda parterna är användarna eller 122 N. Sharygina och D. Kröning kunder, leverantören själv, och back-office tjänsteleverantörer, t.ex., betalningsclearing tjänsten. Bemyndigandet av betalningen ges av ett serviceföretag för kreditkortstransaktioner, medan "köpkorgen" och lagringen genomförs av säljaren. Det är lätt att föreställa sig en annan part som deltar i en transaktion, t.ex. ett företag som utför själva transporten. Varje part använder vanligtvis en stor uppsättning maskiner för lastdelning. Säkerhets- och säkerhetskraven är ofta globala, dvs. kräver resonemang om flera parter och kan omfatta mer än en server vid varje part. Ett typiskt scenario beskrivs i bild. 5,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0. En handlare driver tre värdar (t.ex. av redundans- eller lastbalanseringsskäl). Två av dessa värdar ('Host 1' och 'Host 2') används för att köra en webbserver, t.ex. Apache. Webbservern i sig är uppdelad i flera processer, T 1,. ..,.............................................................. Webbserverprocesserna har gemensam åtkomst till en delad databas, t.ex. med hjälp av SQL-protokollet. Denna databas antas vara den enda formen av kommunikation mellan serverprocesserna. Serverprocesserna kan kontakta en tredje part, t.ex. för att godkänna en betalning. Inkommande kundförfrågningar modelleras med hjälp av processerna T 5 och T 6. Att analysera programvara som implementerar sådana tjänster kräver därför att man resonerar om många program som kör parallellt. Konkurrent programvara är notoriskt felbenägen. Metoder baserade på testning misslyckas ofta med att hitta viktiga konvergens buggar. Förlagakontroll [2, 3] är en formell kontrollteknik. Det har visat sig vara särskilt användbart för att verifiera konvergensrelaterade egenskaper, och identifiera fel relaterade till processscheman. I samband med webbtjänster finns det många olika egenskaper som modellkontroll kan användas för att verifiera: • Säkerhetsegenskaper, t.ex. att inga undantag kastas av koden, att koden är fri från datatävlingar, eller att vissa säkerhetsegenskaper innehåller. • Liveness egenskaper, t.ex., att koden inte kommer in i ett tillstånd där det dödläge eller livlås. Modellkontroll lider emellertid av problemet med statsexplosionen. Vid BDD-baserad symbolisk modellkontroll manifesterar sig detta problem i form av ohanterligt stora BDD [4]. När det gäller samtidig programvara kommer explosionsproblemet i tillståndsrymden från två källor: (1) Modellkontrollen måste ta hänsyn till mångfaldiga interleavings mellan trådarna, och (2) programvara fungerar vanligtvis på en mycket stor uppsättning datavariabler. Den huvudsakliga tekniken för att ta itu med det första problemet är partiell orderminskning [5]. Den huvudsakliga metoden för att hantera den stora mängden data är abstraktion. Abstraction tekniker minskar tillståndet utrymme genom att kartlägga uppsättningen av tillstånd i det faktiska, konkreta systemet till en abstrakt och mindre uppsättning av tillstånd på ett sätt som bevarar relevanta beteenden i systemet. Användningen av abstraktion på övergångssystem formaliseras av den abstrakta tolkningsramen [6]. Predikerad abstraktion [7, 8] är en av de mest populära och allmänt tillämpade metoderna för systematisk abstraktion av program. Det absorberar data genom att bara hålla reda på vissa predikat på data. Varje predikat representeras av en boolesk variabel i det abstrakta programmet, medan de ursprungliga datavariablerna elimineras. Verifiering av ett programvarusystem med predikativ abstraktion består i att konstruera och utvärdera ett finit-state-system som är en abstraktion av det ursprungliga systemet med avseende på en uppsättning predikat. Vanligtvis skapas detta abstrakta program med hjälp av Existentiell Abstraction [9]. Denna metod definierar instruktionerna i det abstrakta programmet så att det garanteras att vara en konservativ över-uppskattning av det ursprungliga programmet för nåbarhet egenskaper. För att visa att inget felaktigt tillstånd kan nås räcker det alltså att visa att den abstrakta modellen inte innehåller den. Nackdelen med en sådan konservativ abstraktion är att när modellkontroll av det abstrakta programmet misslyckas, kan det producera ett motexempel som inte motsvarar något motexempel på det ursprungliga programmet. Detta kallas vanligen ett falskt motexempel. När man stöter på ett falskt motexempel utförs förfining genom att man justerar uppsättningen predikat på ett sätt som eliminerar detta motexempel från det abstrakta programmet. Denna process itereras tills antingen ett motexempel hittas, eller egenskapen visas. De faktiska stegen i slingan följer motexempelet guidad abstraktion förfining (CEGAR) ram. Den befintliga programvaran Model Checkers är dock inte lätt att använda för de flesta program som implementerar webbtjänster. Detta beror på att de befintliga verktygen saknar stöd för programmeringsspråken och de kommunikationsimperialer som används för webbtjänster. Ett antal programmeringsspråk har utformats särskilt för att genomföra webbtjänster. De allmänt använda programmeringsspråken för webbapplikationer är WSDL, BPEL, PHP [15] och ASP [16]. Deras mål är i allmänhet att tillhandahålla programplaneringskonstruktioner för genomförandet av webbtjänster, men de skiljer sig åt i fråga om den nivå på vilken de behandlar webbtjänstverksamheten. Till exempel har BPEL [17] utvecklats för att specificera interaktionsprotokoll (synkront och asynkront) mellan webbtjänster. BPEL är också ett språk på hög nivå för att implementera applikationer för webbtjänster, och stöds av de mest industriella aktörerna på området (IBM, Oracle, BEA). Den är utformad för att specificera kommunikationen mellan tjänstedeltagare och dess användare. Nackdelen med detta är att det inte stöder detaljerna för genomförandet av tjänsten på låg nivå. Bland de programmeringsspråk som stöder information på låg nivå om implementationer av webbtjänster finns ASP och PHP. ASP (Active Server Pages) är baserad på antingen Visual Basic Script eller JScript. ASP är ett egenutvecklat system som är implementerat enbart på Microsoft Internet Information Server (IIS). Det finns försök att genomföra ASP på andra arkitekturer, t.ex. InstantASP från Halcyon och Chili!Soft ASP. Formella modeller av ASP-skript är svåra att generera eftersom ASP tillåter full tillgång till WIN32 API, som erbjuder en enorm mängd funktioner. Det andra vanliga programmeringsspråket för webbapplikationer är PHP, ett skriptspråk specialiserat på generering av HTML, serversidan JAVA, Microsofts ASPx, och mer nyligen, C# som en del av.NET. PHP är ett tolkat programmeringsspråk som har en C-liknande syntax. Den vanligaste plattformen för PHP är Apache webbserver, men det finns implementationer för IIS-baserade servrar också. Ett stort antal verktyg och tekniker för modellering och modellkontroll av BPEL-processer har utvecklats (se t.ex. [18, 19, 20, 21, 22, 23, 24, 25] ). De fokuserar på att analysera interaktionsprotokollen, orkestreringen och sammansättningen av webbtjänster. De är dock inte tillämpliga för att kontrollera de faktiska tillämpningar som genomför webbtjänsterna på grund av begränsningarna i BPEL-notationen. När det gäller kontrollen av det faktiska genomförandet av webbtjänster finns det ännu inga verktyg tillgängliga. Dessutom finns det, såvitt vi vet, inga genomföranden av ramverket för abstractionraffinering tillgängliga för något av de språk som vanligtvis används för implementering av webbtjänster. Medan det finns modellkontroller för samtidig Java, antas samstämmigheten genomföras med hjälp av Java tråd gränssnitt. Kommunikation mellan processerna antas genomföras med hjälp av delade data. I motsats till detta är program som implementerar webbtjänster vanligtvis en gänga. Samstämmigheten uppstår från det faktum att det finns flera fall av samma enkeltrådade program som körs. Kommunikationen mellan processerna genomförs vanligtvis av antingen 1. TCP uttag som använder protokoll som HTML eller XML, eller 2. delade databaser med hjälp av frågespråk som SQL. Observera att de två kommunikationsimperialerna ovan har olika semantik: i samband med webbtjänster sker kommunikation via ett TCP-uttag vanligtvis på ett synkront, blockerande sätt, dvs. efter att ha skickat data, brukar sändningsprocessen vänta på ett erkännande från mottagaren och därmed blockeras tills mottagningsprocessen accepterar och bearbetar meddelandet. I motsats till detta utförs databasåtkomst vanligtvis oberoende av varje process. Blockering undviks för att få skalbarhet i antalet databasklienter. Medan själva SQL-protokollet blockerar, kommunikationen mellan processer genom en delad databas har asynkron semantik. Således blir interleakings av konkurrerande tillgång till databasen relevant. Återvänder till det scenario som beskrivs ovan ( Bild. 5.1) är gemensamma databaser vanligtvis endast tillgängliga inom ett enda partis område. Länkar till externa parter (klienter, tredjepartsleverantörer) genomförs vanligtvis med hjälp av synkroniseringsprotokoll såsom SOAP. Formellt resonemang om de globala egenskaperna hos webbtjänster kräver identifiering och modellering av båda dessa kommunikationsprimära. Framför allt behövs stöd för både synkronisering och asynkron kommunikation mellan processer. Ingen av de befintliga programvarumodellkontrollerna ger sådant stöd. Vi föreslår att använda LKS (Labeled Kripke Structures) som ett sätt att modellera webbtjänster: LKS är riktade grafer där stater är märkta med atomförslag och övergångar är märkta med åtgärder. Synkroniseringssemantiken är härledd från CSP (Communicating Sequential Processes), dvs. processer synkroniserar på delade händelser och fortsätter självständigt på lokala. Formalismen stöder delade variabler. När den formella modellen har hämtats från genomförandet blir webbtjänsten tillgänglig för formell analys genom modellkontroll [26]. Detta kapitel tar upp ett problem med att kontrollera de tillämpningar som genomför webbtjänsterna och utvecklar tekniker för modellering och verifiering av lågnivåspråk som används för genomförandet av webbtjänster. Vi formaliserar semantiken i ett PHP-liknande programmeringsspråk för webbtjänster med hjälp av märkta Kripke strukturer. Vi använder en beräkningsmodell som möjliggör både synkronisering och interleaving kommunikation. Tidigare modeller är begränsade till antingen synkron eller asynkron inter-process kommunikation. När modellen har erhållits, automatiskt predikat abstraktion är Vi implementerar den teknik som beskrivs ovan i ett verktyg som kallas SatAbs. Den kan kontrollera säkerhetsegenskaper hos en kombination av flera PHP-skript. Den använder Zend 2 motorn som en front-end för PHP. Den abstrakta modellen beräknas med hjälp av SAT och analyseras med hjälp av en symbolisk modellkontroll som har partiell orderreduktion. Formella modeller för synkroniseringsmekanismer har grundligt utforskats. Till exempel infördes CSP [30] och kalkylen av kommunikationssystem (CCS för kort) [31] under samma år och påverkade varandra under hela deras utveckling. CSP och CCS gör det möjligt att beskriva system i form av komponentprocesser som fungerar oberoende och interagerar med varandra enbart genom olika synkroniseringsmekanismer. I CSP måste två processer synkroniseras med varje identiskt namngiven åtgärd (dvs. med hjälp av delade åtgärder) som båda potentiellt kan utföra. Dessutom kan ett antal processer samverka om en enda gemensam åtgärd. I CCS kan processer interagera på två kompletterande åtgärder (t.ex. a och a, respektive input och output åtgärder över en delad kanal som heter a), och endast bi-part interaktion stöds. Både CSP och CCS ger inte ett sätt att direkt representera och resonera om dynamiska kommunikationstopologier och migrering av beräkningsagenter, som är en viktig aspekt av många moderna system. En del människor ser detta som en stor nackdel av sin teori. Pi-kalculus [32] uppstod som en generalisering av CCS [31]. I pi-calculus, processer inte bara synkronisera på två input/output åtgärder över en delad kanal, lånade också skicka data längs dessa kanaler. Detta kapitel bygger på det arbete som beskrivs i [26], där SAT-baserad predikativ abstraktion tillämpas på en SystemC-design. SystemC är ett beskrivningsspråk baserat på C++ som används för att modellera både hård- och programvarukomponenter i inbyggda konstruktioner. SystemC:s konvergerande primitiver är modellerade med hjälp av den stat/händelsebaserade notation som infördes i [33]. Liksom i detta arbete består modelleringsramverket av märkta Kripke-strukturer. Den kombinerade statsbaserade och händelsebaserade notationen har undersökts av ett antal forskare. De Nicola och Vaandrager [34] införde till exempel " dubbelt märkta övergångssystem", som är mycket lika våra LKS. Kindler och Vesper [35] använde en tillståndsbaserad temporallogik för Petrinät. Abstraction-baserad modellkontroll rapporteras inte för dessa formaliseringar. Huth m.fl. [36] föreslog också en stat/händelseram och definierade rika begrepp om abstraktion och förfining. Dessutom tillhandahöll de "kan" och "måste" villkor för övergångar, och visade hur man kan utföra effektiva trevärderade kontroller av sådana strukturer. Merparten av det relaterade arbetet med formell analys av webbtjänster består av att kontrollera en formell beskrivning av webbtjänsten med hjälp av en modellkontroll. Exempelvis föreslår författarna i [27] att modeller som beskrivs i BPEL ska översättas till Promela och kontrollera webbtjänstens flöde med SPIN-modellen. Ett annat exempel på modellering och modellkontroll av BPEL-protokoll är [18]. Den använder Petri-nät för modellering och verifiering av samordningen av BPEL-processerna. I [28], ett liknande tillvägagångssätt använder NuSMV. Verifieringen av Linear Temporal First-Order egenskaper asynkront kommunicerande webbtjänster studeras i [29]. Deltagarna får indata från sina användare och asynkrona meddelanden från andra. Författarna utvecklade en modellkontroll för särskilda ändamål [29] som möjliggör verifiering av webbapplikationer som anges i WebML. Bland andra viktiga tekniker för att analysera webbtjänster finns verk av Bultan och andra. Denna grupp utvecklade en formell modell för interaktioner mellan sammansatta webbtjänster som stöds av tekniker för analys av sådana interaktioner [25, 24, 23, 39, 22]. Kramer och Al. [40] definierade en modellbaserad metod för att verifiera processinteraktioner för samordnade webbtjänstsammansättningar. Tillvägagångssättet använder ändliga tillstånd maskin representationer av webbtjänst orkestreringar och tilldelar semantik till distribuerade processinteraktioner. Pistore m.fl. Föreslagna tekniker för automatiserad syntes av sammansatta webbtjänster från abstrakta BPEL-komponenter [20] och verifiering av webbtjänstsammansättningar som definieras av uppsättningar av BPEL-processer [19]. Modelleringstekniker används för att representera kommunikationen bland de tjänster som deltar i sammansättningen. Dessa meddelanden är asynkrona och buffrade i de befintliga genomföranderamarna, medan de flesta verifieringsmetoder antar en synkron kommunikationsmodell av effektivitetsskäl. I [37] verifieras åtminstone gränssnittsspecifikationen på källkodsnivån med hjälp av Java PathFinder. SPIN-modellkontrollen används för beteendeverifiering av asynkront kommunicerande deltagare (begränsade brevköer). Ett språk för att ange gränssnitt för webbtjänster presenteras i [38]. Ingen av ovanstående tekniker använder automatiserad abstraktionbaserad verifiering och är därmed mindre konkurrenskraftig i kontrollen av storskaliga webbsystem. Vi ger bakgrundsinformation om PHP och relaterade språk och predikerar abstraktion i Sect. Denna förordning träder i kraft den tjugonde dagen efter det att den har offentliggjorts i Europeiska unionens officiella tidning. Vi förklarar beräkningsmodellen i Sect. 5.3 och formalisera semantiken i den delmängd av PHP vi hanterar. I avsnitt 5.4 ges närmare information om hur den genererade modellen kan abstrakteras och hur den kan verifieras.  Bakgrund En webbtjänst är ett system som tillhandahåller ett gränssnitt som definieras i termer av XML-meddelanden och som kan nås via Internet [41]. Den är avsedd för maskin-till-maskin interaktion. En sådan tjänst är vanligtvis inbäddad i en applikationsserver. Appliceringsservern är ett program som körs i en oändlig loop och väntar tills en klient ansluter via ett uttag (med hjälp av dubbelriktad kommunikation över Internet) till en angiven port. För att behandla flera förfrågningar samtidigt hanteras varje inkommande begäran med en ny tråd från en trådpool. Således kan det finnas flera fall av samma kod som körs samtidigt. Det finns tre huvudsakliga XML-baserade standarder som definierar webbtjänsternas arkitektur: protokollet Universal Description, Discovery and Integration (UDDI) används för att publicera och upptäcka webbtjänster som specificeras i Web Service Description Language (WSDL). Kommunikationen mellan webbtjänster definieras i protokollet om enkel tillgång till objekt (SOAP). Det finns tre viktiga roller inom webbtjänstens arkitektur (Fig. Denna förordning träder i kraft den tjugonde dagen efter det att den har offentliggjorts i Europeiska unionens officiella tidning. Två: 1. Tjänsteleverantören - Tjänsteleverantören implementerar tjänsten och gör den tillgänglig på Internet. 2. Utgångspunkten är följande: Tjänsteförfrågan -Den klient som ansluter till webbtjänsten. 3. Vad är det som händer? Servicemäklare -Detta är en logiskt centraliserad katalog över tjänster där tjänsteleverantörer kan publicera sina tjänster tillsammans med en tjänstebeskrivning. Tjänsteförfrågan kan söka efter tjänster i denna katalog. Vi begränsar presentationen till tjänsteleverantörer och framställare, dvs. vi antar att tjänsterna hanteras statiskt av dem som begär tjänsten. Eftersom det finns XML-verktyg för nästan alla operativsystem och alla programmeringsspråk är webbtjänsterna oberoende av maskinarkitekturen, operativsystemet och programmeringsspråket. Vi använder PHP syntax för att presentera vår formalism. Formalismen är tillämplig på liknande språk för webbtjänster samt med mindre ändringar som är specifika för syntaxen för dessa språk.  WSDL WSDL SOAP Synkron kommunikation inom webbtjänster kännetecknas av att kunden blockeras tills tjänsten begäran har behandlats. Exempel 1 Ett exempel på synkron kommunikation är en kreditkortstjänst som används i en e-handelsapplikation: när kunden checkar ut sin kundvagn åberopas kreditkortstjänsten och ansökan väntar sedan på godkännande eller avslag av kreditkortstransaktionen (Fig. 5. 3................................................................................................... Figur 5.4 och 5.5 visar ett exempel på hur en klient respektive en server kan implementeras. Asynkron kommunikation används när programmet inte kan vänta på att mottagaren ska bekräfta att uppgifterna mottagits. Tänk till exempel på den del av e-handelsapplikationen som underhåller en inköpskorg. Denna shopping basked är vanligtvis lagras i ihållande minne, t.ex., en databas. Informationen är vanligtvis åtkomlig genom flera processer under livscykeln av interaktionen med klienten och, på sätt och vis, kommuniceras från en instans av serverprocessen till nästa. Tiden som går mellan åtkomsterna till korgen är godtycklig. Synkronisering mellan den tidpunkt då data skickas (lagras) och tas emot (läsas) önskas inte. Observera också att ordern blir viktig: som ett exempel, anta att en kund samtidigt utfärdar en begäran om att lägga till ett objekt av en viss typ i korgen och, självständigt, en annan begäran om att ta bort alla objekt av samma typ. Slutresultatet (ingen eller en post av den typen) beror på i vilken ordning databastransaktionerna behandlas. I f ( $ c l i e n t - > d e b i t ( $ kortnummer, $ belopp) ) { 4 / / t r a n s a c t i o n godkänd 5 / /. ......................................................................... .. 9 } Vi antar att en delad databas är det enda sättet att utbyta data mellan processerna på ett icke-synkroniserande sätt, dvs vi modellerar inte lokala, delade filer som kan skrivas in i, eller liknande. Databasen förväntas garantera en viss atomär nivå i form av transaktioner. De olika transaktionerna från de olika processerna för att få tillgång till databasen antas intervenera godtyckligt. Frågan om beställning fångas av begreppet raser. Den shopping-basked som beskrivs ovan är ett exempel på en sådan ras. Sådana raser representerar ofta ett felaktigt beteende. Fel orsakade av rasförhållanden är ett välkänt problem för alla system med asynkron konvergens och är mycket svåra att upptäcka med hjälp av testning. Den abstraktion förfiningsprocessen med hjälp av predikat abstraktion har främjats av framgången för Slam-projektet på Microsoft Research, som syftar till att verifiera partiell korrekthet av Windows enhetsdrivrutiner [10]. Algoritmen börjar med en grov abstraktion, och om det konstateras att en fel-trace som rapporterats av modellen kontroll är inte realistisk, felet spår används för att förfina det abstrakta programmet, och processen fortsätter tills inga falska fel spår kan Annars, C är falska, och M förfinas med hjälp av C för att få en mer exakt abstraktion. Algoritmen fortsätter med steg 1. Målet med abstraktionen är att beräkna en abstrakt modellM från betongmodellen M så att storleken på statsrymden reduceras och egendomen av intresse bevaras. Vi betecknar uppsättningen abstrakta stater med. Ett konkret tillstånd är kartlagt till ett abstrakt tillstånd med hjälp av en abstraktionsfunktion, som vi betecknar med α : S −→. Vi utvidgar också definitionen av α till uppsättningar av stater: Med tanke på en uppsättning S  och S, betecknar vi (=====} av α(S ). Vi begränsar presentationen till tillgänglighetsegenskaper. Målet är därför att beräkna en abstraktion som bevarar nåbarhet: varje program plats som kan nås i M måste vara nåbar inM. Existentiell abstraktion är en form av abstraktion som bevarar tillgängligheten [9]. Existentiell abstraktion är en konservativ abstraktion med avseende på nåbarhetsegenskaper, som formaliseras enligt följande. Definition 1 (Existentiell Abstraction [9]) Med tanke på en abstraktion funktion Således, för en existentiell abstractionM och någon program plats l som inte går att nå i den abstrakta modellenM, kan vi säkert dra slutsatsen att det är också ouppnåelig i den konkreta modellen M. Observera att den omvända inte håller, dvs det kan finnas platser som är nåbara inM men inte i M. Vi betecknar uppsättningen program platser av L. I programverifiering, är den abstrakta övergångsrelationenR typiskt representeras med hjälp av en partitionering, på samma sätt som den konkreta övergångsrelationen R. Den abstrakta övergångsrelationen för programplats l. L betecknas avR l ( och programplaceringen av en abstrakt stat av..................................................... Beräkningen avR följer strukturen för partitioneringen enligt programplatserna, dvs.,R genereras av computingR l från R l för varje plats l  och L separat. Följande avsnitt beskriver algoritmer för computingR l. Det finns olika möjliga val för en abstraktion funktion α. Predicate abstraktion är ett möjligt val. Det är en av de mest populära och allmänt tillämpade metoderna för systematisk abstraktion av program och introducerades av Graf och Saïdi [7]. Ett automatiserat förfarande för att generera predikativa abstraktioner infördes av Colón och Uribe [8]. Predicera abstraction abstracts data genom att hålla reda på endast vissa predikat på data. De predikat definieras typiskt av booleska uttryck över de konkreta programvariablerna. Varje predikat representeras sedan av en boolesk variabel i det abstrakta programmet, medan de ursprungliga datavariablerna elimineras. Verifiering av ett programvarusystem genom predikativ abstraktion innebär konstruktion och utvärdering av ett system som är en abstraktion av det ursprungliga systemet med avseende på en uppsättning predikat. i++; Detta uttalande översätts till följande konkreta övergångsförhållande R l (s, s ): Antag att uppsättningen predikat består av π 1  på i = 0 och π 2 på i), där even(i) innehar iff i är ett jämnt tal. Med n = 2 predikat finns det (2 n ) 2 = 16 potentiella abstrakta övergångar. Ett naivt sätt att beräkna R är att räkna upp paren och att kontrollera (5.1) för varje par separat. Som exempel kan nämnas att övergången från 1 = (l, F, F) till 2) = (l, F, F) motsvarar följande formel över konkreta tillstånd: Denna formel kan kontrolleras genom ett beslutsförfarande. Till exempel kan en automatisk teoremprovare som Simplify [42] användas om en definition av even(i) ges tillsammans med (5.5). Eftersom (5.5) inte har någon lösning, är denna abstrakta övergång inte inR l. Figur 5.6 visar de abstrakta övergångarna för programuttalandet ovan, och en motsvarande konkret övergång (dvs. en tillfredsställande uppgift till (5.1)) för varje möjlig abstrakt övergång. s.π1 ska.π2 ska.π1 ska abstrakt övergång Konkret övergång
Sharygina REF presenterar en modellkontroll med abstraktionsmetoder för webbtjänster, som översätter php-implementationer till en kriskestruktur för att verifiera den med SATABS.
Model Checking with Abstraction for Web Services
{'venue': 'Test and Analysis of Web Services', 'journal': None, 'mag_field_of_study': ['Computer Science']}