Detail publikace

On Analysis of Software Interrupt Limiters for Embedded Systems by Means of UPPAAL SMC

STRNADEL, J. RIŠA, M.

Originální název

On Analysis of Software Interrupt Limiters for Embedded Systems by Means of UPPAAL SMC

Anglický název

On Analysis of Software Interrupt Limiters for Embedded Systems by Means of UPPAAL SMC

Jazyk

en

Originální abstrakt

The paper deals with a novel method of modeling and analysis of software interrupt managers for event-driven embedded systems by means of the stochastic timed automata and statistical model checking instruments. The above-mentioned system is typically formed of a real-time part expected to produce correct responses and meet all predetermined timing constraints at runtime, even in adverse conditions such as an excessive rate of events caused by interrupts. Because of the asynchronnous nature of interrupts, their impact to the system being interrupted must be modeled and analyzed very carefully for various interrupt scenarios - either using classical analytical/formal approaches able to cover systems and interrupts with deterministic behavior or using probablistic ones able to deal with a stochastic behavior too. The paper is focused to the latter (probabilistic) approaches to show a style of such a modeling and show how and that both the analysis phase of a system can be facilitated and the information about a system behavior under particular configuration/scenarios can be produced using the statistical model checking instruments.

Anglický abstrakt

The paper deals with a novel method of modeling and analysis of software interrupt managers for event-driven embedded systems by means of the stochastic timed automata and statistical model checking instruments. The above-mentioned system is typically formed of a real-time part expected to produce correct responses and meet all predetermined timing constraints at runtime, even in adverse conditions such as an excessive rate of events caused by interrupts. Because of the asynchronnous nature of interrupts, their impact to the system being interrupted must be modeled and analyzed very carefully for various interrupt scenarios - either using classical analytical/formal approaches able to cover systems and interrupts with deterministic behavior or using probablistic ones able to deal with a stochastic behavior too. The paper is focused to the latter (probabilistic) approaches to show a style of such a modeling and show how and that both the analysis phase of a system can be facilitated and the information about a system behavior under particular configuration/scenarios can be produced using the statistical model checking instruments.

Dokumenty

BibTex


@inproceedings{BUT130996,
  author="Josef {Strnadel} and Michal {Riša}",
  title="On Analysis of Software Interrupt Limiters for Embedded Systems by Means of UPPAAL SMC",
  annote="The paper deals with a novel method of modeling and analysis of software
interrupt managers for event-driven embedded systems by means of the stochastic
timed automata and statistical model checking instruments. The above-mentioned
system is typically formed of a real-time part expected to produce correct
responses and meet all predetermined timing constraints at runtime, even in
adverse conditions such as an excessive rate of events caused by interrupts.
Because of the asynchronnous nature of interrupts, their impact to the system
being interrupted must be modeled and analyzed very carefully for various
interrupt scenarios - either using classical analytical/formal approaches able to
cover systems and interrupts with deterministic behavior or using probablistic
ones able to deal with a stochastic behavior too. The paper is focused to the
latter (probabilistic) approaches to show a style of such a modeling and show how
and that both the analysis phase of a system can be facilitated and the
information about a system behavior under particular configuration/scenarios can
be produced using the statistical model checking instruments.",
  address="IEEE Computer Society Press",
  booktitle="Proceedings of the 24th Austrian Workshop on Microelectronics",
  chapter="130996",
  doi="10.1109/Austrochip.2016.020",
  edition="NEUVEDEN",
  howpublished="online",
  institution="IEEE Computer Society Press",
  year="2016",
  month="october",
  pages="45--50",
  publisher="IEEE Computer Society Press",
  type="conference paper"
}