Detail publikace

Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

STRNADEL, J.

Originální název

Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

Anglický název

Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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.

Dokumenty

BibTex


@inproceedings{BUT155016,
  author="Josef {Strnadel}",
  title="Statistical Model Checking of Processor Systems in Various Interrupt Scenarios",
  annote="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.",
  address="Springer International Publishing",
  booktitle="Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",
  chapter="155016",
  doi="10.1007/978-3-030-03421-4_26",
  edition="Lecture Notes in Computer Science, Vol. 11245",
  howpublished="online",
  institution="Springer International Publishing",
  number="10",
  year="2018",
  month="march",
  pages="414--429",
  publisher="Springer International Publishing",
  type="conference paper"
}