Publication Details
Statistical Model Checking of Processor Systems in Various Interrupt Scenarios
cpu, systém, interrupt, arrival, servicing, execution, priority, jiter, nesting,
masking, late arrival, tail chaining, modeling, stochastic timed automaton,
predictability analysis, statistical model checking
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.
@inproceedings{BUT155016,
author="Josef {Strnadel}",
title="Statistical Model Checking of Processor Systems in Various Interrupt Scenarios",
booktitle="Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",
year="2018",
series="Lecture Notes in Computer Science, Vol. 11245",
journal="Lecture Notes in Computer Science",
number="10",
pages="414--429",
publisher="Springer International Publishing",
address="Cham",
doi="10.1007/978-3-030-03421-4\{_}26",
issn="0302-9743",
url="https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26"
}