Abstract-Många mjukvarusystem fungerar på olika geografiskt distribuerade hårdvaruplattformar, operativsystem och programmeringsspråk. Publicera/prenumerera baserat Meddelande Orienterat Middleware (MOM) ger löskoppling och ett effektivt, asynkront och skalbart sätt att kommunicera. I takt med att komplexiteten i sådana system ökar blir emellertid den manuella kontrollen av omkonfigureringspolitiken orealistisk. Uppgiften kräver automatiserade metoder för att kontrollera konfigurationsinformation för att förbättra tillförlitligheten hos storskaliga MOM-system. I detta dokument föreslås en ny modell för kontroll med tidslogiska specifikationer för att utforma och verifiera en systemkonfiguration. Modellkontroll är en kraftfull teknik, men skapandet av lämpliga finita tillståndsmodeller för de system som kontrolleras är komplicerade och svåra att använda i praktiken av icke-formella. Den forskning som presenteras i denna uppsats finner lämpliga abstraktioner som reducerar systemet till en ändlig tillståndsmodell. De verktyg vi utvecklat för att skapa sådana modeller kan lätt användas av icke-formella personer. De systemmodeller som skapas med hjälp av våra tekniker hanterar statsexplosion tack vare val av våra abstraktioner. Ett exempel på användningen av våra verktyg och tekniker presenteras för en 50 nod MOM, där tillgängligheten för alla ämnen och förekomsten av slingor kontrolleras. Index Terms-meddelande orienterad middleware, modellkontroll, storskaligt system, publicera / prenumerera
REF föreslår en särskild modellkontrollteknik för att verifiera egenskaperna hos system för publicering/prenumeration-baserad meddelandeorienterad Middleware (MOM).
Improved reliability of large scale publish/subscribe based MOMs using model checking