Abstrakt. Mycket forskningsarbete har gjorts på formalisering UML diagram, men mindre har fokuserat på att använda denna formalisering för att analysera dynamiska beteenden mellan formaliserade komponenter. I detta dokument föreslår vi att man använder en delmängd av fUML (Foundational Subset for Executable UML) som ett semiformellt språk, och formaliserar det till processen algebraisk specifikationsspråk CSP, för att använda FDR som modellkontroll. Vår formalisering inkluderar modellering av den asynkrona kommunikationsram som används inom fUML. Detta gör det möjligt att utvärdera olika tolkningar av kommunikationsmodellen. För att illustrera tillvägagångssättet använder vi modellering av Tokeneer ID Station specifikationer i fUML, och formalisera dem i CSP för att kontrollera om modellen är dödlägesfri.
Abdelhalim m.fl. REF presenterar ett tillvägagångssätt för att manuellt kartlägga en fUML-modeller i processen algebraic specifikation språk CSP (Communicating Sequential Processes) och använda FDR (Underkänder-Divergences Raffinement) modellchecker för att kontrollera om modellen är dödlägesfri.
Formal verification of Tokeneer behaviours modelled in fUML using CSP
{'venue': 'ICFEM', 'journal': None, 'mag_field_of_study': ['Computer Science']}