Článek ve sborníku konference

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). 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
Jazyk publikace:angličtina
Název publikace:Statistical Model Checking of Processor Systems in Various Interrupt Scenarios
Název (cs):Statistické ověřování modelů procesorových systémů v různých přerušovacích scénářích
Strany:414-429
Sborník:Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)
Konference:8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
Řada knih:Lecture Notes in Computer Science, Vol. 11245
Místo vydání:Cham, CH
Rok:2018
URL:https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26
Časopis:Lecture Notes in Computer Science, č. 10, DE
ISSN:0302-9743
DOI:10.1007/978-3-030-03421-4_26
Vydavatel:Springer International Publishing
Klíčová slova
cpu, systém, interrupt, arrival, servicing, execution, priority, jiter, nesting, masking, late arrival, tail chaining, modeling, stochastic timed automaton, predictability analysis, statistical model checking
Anotace
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ů.
BibTeX:
@INPROCEEDINGS{
   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 = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=11680}
}

Vaše IPv4 adresa: 54.87.61.215
Přepnout na https