Detail publikace
Statistical Model Checking of Processor Systems in Various Interrupt Scenarios
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ů.
@INPROCEEDINGS{FITPUB11680, author = "Josef Strnadel", title = "Statistical Model Checking of Processor Systems in Various Interrupt Scenarios", pages = "414--429", booktitle = "Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)", series = "Lecture Notes in Computer Science, Vol. 11245", journal = "Lecture Notes in Computer Science", number = 10, year = 2018, location = "Cham, CH", publisher = "Springer International Publishing", ISSN = "0302-9743", doi = "10.1007/978-3-030-03421-4\_26", language = "english", url = "https://www.fit.vut.cz/research/publication/11680" }