Publication Details

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, pp. 414-429. ISSN 0302-9743. Available from: https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26
Czech title
Statistické ověřování modelů procesorových systémů v různých přerušovacích scénářích
Type
conference paper
Language
english
Authors
Strnadel Josef, Ing., Ph.D. (DCSY FIT BUT)
URL
Keywords

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

Abstract

Many practical, especially real-time, systems are expected to be predictable under various sources of unpredictability. To cope with the expectation, a system must be modeled and analyzed precisely for various operating conditions. This represents a problem that  grows with the dynamics of the system and that must be, typically, solved before the system starts to operate.  Due to the general complexity of the problem, this paper focuses just to processor based systems with interruptible executions. Their predictability analysis becomes more difficult especially when interrupts may occur at arbitrary times, suffer from arrival and servicing jitters, are subject to priorities, or may be nested and un/masked at run-time. Such a behavior of interrupts and executions has stochastic aspects and leads to the explosion of the number of situations to be considered.  To cope with such a behavior, we propose a simulation model that relies on a network of stochastic timed automata and involves the above-mentioned behavioral aspects related to  interrupts and executions. For a system, modeled by means of the automata, we show that the problem of analyzing its predictability may be efficiently solved by means of the statistical model checking.

Published
2018
Pages
414-429
Journal
Lecture Notes in Computer Science, no. 10, ISSN 0302-9743
Proceedings
Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)
Series
Lecture Notes in Computer Science, Vol. 11245
Conference
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Limassol, CY
Publisher
Springer International Publishing
Place
Cham, CH
DOI
10.1007/978-3-030-03421-4_26
EID Scopus
2-s2.0-85056478486
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"
}
Files
Back to top