Den kritiska karaktären hos många komplexa mjukvaruintensiva system kräver formella, rigorösa arkitekturbeskrivningar som ett sätt att stödja automatisk verifiering och upprätthållande av arkitektoniska egenskaper och begränsningar. Modellkontroll har varit en av de mest använda teknikerna för att automatiskt verifiera programvaruarkitekturer med avseende på tillfredsställelsen av arkitektoniska egenskaper. Men en sådan teknik leder till en uttömmande undersökning av alla möjliga tillstånd i systemet, ett problem som blir svårare när verifiera dynamiska mjukvarusystem på grund av deras typiska icke-deterministiska körtid beteende och oförutsägbara driftsförhållanden. För att ta itu med dessa frågor föreslår vi att man använder statistisk modellkontroll (SMC) för att stödja verifieringen av dynamiska programvaruarkitekturer, samtidigt som man strävar efter att minska de beräkningsresurser och den tid som krävs för denna uppgift. I detta dokument introducerar vi en ny notation till formellt uttrycka arkitektoniska egenskaper samt en SMC-baserad verktygskedja för att verifiera dynamiska programvaruarkitekturer som beskrivs i π-ADL, ett formellt arkitekturbeskrivningsspråk. Vi använder ett system för övervakning av översvämningar för att visa hur man uttrycker relevanta egenskaper som ska verifieras. Vi rapporterar också resultaten av vissa beräkningsförsök som utförts för att bedöma effektiviteten i vårt tillvägagångssätt.
För kontroll av överensstämmelsen hos en dynamisk programvaruarkitektur, Cavalcante et al. I REF föreslås en statistisk modellkontroll (SMC).
Statistical Model Checking of Dynamic Software Architectures
{'venue': 'ECSA', 'journal': None, 'mag_field_of_study': ['Computer Science']}