mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
PTRebeca: Modeling and analysis of distributed and asynchronous systems
Reykjavik Univ, Reykjavik, Iceland.
Reykjavik Univ, Reykjavik, Iceland.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Reykjavik Univ, Reykjavik, Iceland.
Univ Saarland, Saarbrucken, Germany..
Show others and affiliations
2016 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 128, 22-50 p.Article in journal (Refereed) Published
Abstract [en]

Distributed systems exhibit probabilistic and non-deterministic behaviors and may have time constraints. Probabilistic Timed Rebeca (PTRebeca) is introduced as a timed and probabilistic actor-based language for modeling distributed real-time systems with asynchronous message passing. The semantics of PTRebeca is a Timed Markov Decision Process. In this paper, we provide SOS rules for PTRebeca, introduce a new tool-set and describe the corresponding mappings. The tool-set automatically generates a Markov Automaton from a PTRebeca model in the form of the input language of the Interactive Markov Chain Analyzer (IMCA). The IMCA can be used as a back-end model checker for performance analysis of PTRebeca models against expected reachability and probabilistic reachability properties. Comparing to the existing tool-set, proposed in the conference paper, we now have the ability of analyzing significantly larger models, and we also can add different rewards to the model. We show the applicability of our approach and efficiency of our tool by analyzing a Network on Chip architecture as a real-world case study. (C) 2016 Elsevier B.V. All rights reserved.

Place, publisher, year, edition, pages
2016. Vol. 128, 22-50 p.
Keyword [en]
Probabilistic Timed Automata, Timed Markov Decision Process, IMCA model checker, Probabilistic Timed Rebeca, Model checking, Performance analysis
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-33049DOI: 10.1016/j.scico.2016.03.004ISI: 000380595400003Scopus ID: 2-s2.0-84979492978OAI: oai:DiVA.org:mdh-33049DiVA: diva2:957177
Available from: 2016-09-01 Created: 2016-09-01 Last updated: 2016-10-31Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Sirjani, Marjan
By organisation
Embedded Systems
In the same journal
Science of Computer Programming
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 6 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf