Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

• https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26

cpu, systém, interrupt, arrival, servicing, execution, priority, jiter, nesting, masking, late arrival, tail chaining, modeling, stochastic timed automaton, predictability analysis, statistical model checking

Mnohé, zejména real-time, systémy se musí chovat předvídatelně i za různých nepředvídatelných okolností. Aby takové chování mohlo být garantováno, systém je nutno precizně modelovat a analyzovat v různých scénářích; to je však problém, jehož složitost roste s dynamikou systému. Kvůli obecné složitosti tohoto problému se však tento článek omezuje jen na procesorové systémy s přerušitelnými prováděními programů. Analýza předvídatelnosti chování takových systémů se však stává komplikovanější, zejména pokud k přerušení může dojít v libovolném čase, přerušení není pravidelné, doba provádění jeho obsluhy je proměnná, přerušení mají různou prioritu či mohou být od/maskovávána za běhu. Obdobné chování přerušení vykazuje stochastické rysy a vede k explozi situací, které je potřeba analyzovat. Pro tento účel navrhujeme simulační model stavějící na síti stochastických časovaných automatů. Novost našeho přístupu spočívá v řešení kombinujícím model přerušovacího podsystému, zdrojů přerušení a obsluh přerušení s vlastnostmi, mezi které patří priority, maskování přerušení a vnořování obsluh přerušení za běhu programu. Analýza navrženého modelu vychází se statistického ověřování modelů, které má potenciál efektivně řešit problém předvídatelnosti chování uvažovaných systémů.