Detail publikace

Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

STRNADEL Josef. Statistical Model Checking of Processor Systems in Various Interrupt Scenarios. In: Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). Lecture Notes in Computer Science, Vol. 11245. Cham: Springer International Publishing, 2018, s. 414-429. ISSN 0302-9743. Dostupné z: https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26
Název česky
Statistické ověřování modelů procesorových systémů v různých přerušovacích scénářích
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
URL
Abstrakt
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ů.
Rok
2018
Strany
414-429
Časopis
Lecture Notes in Computer Science, č. 10, ISSN 0302-9743
Sborník
Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)
Řada
Lecture Notes in Computer Science, Vol. 11245
Konference
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Limassol, CY
Vydavatel
Springer International Publishing
Místo
Cham, CH
DOI
BibTeX
@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"
}
Nahoru