Programarkitekturen i ett distribuerat program kan representeras av en hierarkisk sammansättning av delsystem, med växelverkan processer på bladen av hierarkin. Kompositionsåtkomstanalys (CRA) är en lovande tillståndsreduktionsteknik som kan automatiseras och användas i etapper för att härleda det övergripande beteendet hos ett distribuerat program baserat på dess arkitektur. CRA är särskilt lämpligt för analys av program som är föremål för evolutionär förändring. När ett program utvecklas behöver endast beteendet hos de delsystem som påverkas av förändringen omvärderas. Tekniken har dock en begränsning. De egenskaper som är tillgängliga för analys begränsas av de åtgärder som fortfarande är globalt observerbara. Egenskaper som inbegriper åtgärder inkapslade av delsystem kan därför inte analyseras. I den här artikeln förbättrar vi CRA-tekniken för att kontrollera säkerhetsegenskaper som kan innehålla åtgärder som inte är globalt observerbara. För att uppnå detta, är stat maskin modellen förstärkt med en särskild fälla tillstånd märkt som. Vi föreslår ett system för att i etapper omvandla en egendom som innebär dolda handlingar till en som endast omfattar globalt observerbara handlingar. Den förbättrade tekniken innehåller också en mekanism som syftar till att minska felsökningen. Tekniken illustreras med hjälp av ett exempel på bensinstationssystem.
I den sammansatta säkerhetsanalysmetoden REF beskrivs säkerhetsegenskaperna av statsmaskiner, så kallade egenskapsautomata, som förstärks med ett speciellt odefinierat tillstånd (π).
Checking safety properties using compositional reachability analysis
{'venue': 'TSEM', 'journal': None, 'mag_field_of_study': ['Computer Science']}