En stor utmaning i programvaruutvecklingsprocessen är att föra feldetektering till tidiga faser av programvarans livscykel. För detta ändamål spelar verifieringen och valideringen (V&V) av UML-diagram en mycket viktig roll för att upptäcka brister i konstruktionsfasen. Det har en tydlig betydelse för programvarusäkerhet, där det är viktigt att upptäcka säkerhetsbrister innan de kan utnyttjas. I detta dokument presenteras en formell V&V-teknik för ett av de mest populära UML-diagrammen: sekvensdiagram. Det föreslagna tillvägagångssättet skapar en PROMELA-baserad modell från UML-interaktioner uttryckta i sekvensdiagram, och använder SPIN-modellkontroll för att simulera utförandet och verifiera egenskaper skrivna i Linear Temporal Logic (LTL). Hela tekniken implementeras som en Eclipse plugin, som döljer modellkontroll formalism från användaren. Det viktigaste bidraget från detta arbete är att tillhandahålla en effektiv mekanism för att kunna spåra utförandet av en interaktion, vilket gör det möjligt för designers att skriva relevanta egenskaper som innefattar sända/mottagande händelser och källa/destination av meddelanden med hjälp av LTL. Ett annat viktigt bidrag är definitionen av PROMELA-strukturen som ger en exakt semantik av de flesta nya UML 2.0 introducerade kombinerade fragment, vilket gör det möjligt att utföra komplexa interaktioner. Slutligen illustrerar vi fördelarna med vår strategi genom en säkerhetsrelaterad fallstudie i ett verkligt scenario.
REF föreslog en metod för att utvärdera korrigeringen av beteendet och giltigheten av sekvensdiagram över UML.
Formal Verification and Validation of UML 2.0 Sequence Diagrams using Source and Destination of Messages
{'venue': 'Electron. Notes Theor. Comput. Sci.', 'journal': 'Electron. Notes Theor. Comput. Sci.', 'mag_field_of_study': ['Computer Science']}