Detta dokument tar upp problemet med att verifiera likvärdighet mellan ett par program som fungerar över databaser med olika scheman. Detta problem är särskilt viktigt i samband med webbapplikationer, som vanligtvis genomgår databas refaktor av antingen prestanda- eller underhållsskäl. Medan webbprogram bör ha samma externt observerbara beteende före och efter schema migration, det finns inga befintliga verktyg för att bevisa likvärdighet av sådana program. Detta dokument tar ett första steg mot att lösa detta problem genom att formalisera likvärdighets- och förfiningsproblemen för databasdrivna tillämpningar. Vi föreslår också en bevismetod baserad på begreppet bisimulationsinvarianter över relationell algebra med uppdateringar och beskriver en teknik för att syntetisera sådana bisimuleringsinvarianter. Vi har implementerat den föreslagna tekniken i ett verktyg som kallas Mediator för att verifiera likvärdighet mellan databasdrivna applikationer skrivna på vårt mellanspråk och utvärdera vårt verktyg på 21 riktmärken extraherade från läroböcker och verkliga webbapplikationer. Våra resultat visar att den föreslagna metoden framgångsrikt kan verifiera 20 av dessa riktmärken.
Mediator REF ] är ett verktyg för att resonera om databasapplikationer med uppdateringar.
Verifying equivalence of database-driven applications
{'venue': 'PACMPL', 'journal': None, 'mag_field_of_study': ['Computer Science', 'Mathematics']}