Antalet webbapplikationer som hanterar transaktioner online ökar, men verifieringen av webbapplikationens korrekta utveckling har gjorts manuellt. I detta dokument föreslås en metod för modellering, verifiering och testning av webbapplikationer. I vår metod, en webbapplikation modelleras med hjälp av två ändliga-state automata, dvs. en sida automaton som specificerar webbsida övergångar, och en intern stat automaton som specificerar interna tillstånd övergångar av webbapplikationen. Allmänna egenskaper för att kontrollera webbapplikationens design presenteras i LTL-formler och de verifieras med hjälp av modellkontrollen Spin. Testfall som undersöker beteendet hos webbapplikationen genereras också genom att använda de motexempel som erhållits som resultat av modellkontroll. Vi tillämpade vår metod på ett exempel Webbapplikation för att bekräfta dess effektivitet.
En liknande modellkontrollmetod presenteras i REF, där en webbapplikation modelleras som ett par automata (en för sidnavigering, en annan för interna statsövergångar) och egenskaper om tillgänglighet av sidor etc.
Modeling, Verification and Testing of Web Applications Using Model Checker
{'venue': 'IEICE Transactions', 'journal': 'IEICE Transactions', 'mag_field_of_study': ['Computer Science']}