Quantitative Analysis of Communication Scenarios

Clemens DubslaffClemens Dubslaff, Christel BaierChristel Baier

DOI Link

Clemens Dubslaff, Christel Baier
Quantitative Analysis of Communication Scenarios
Proc. of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), volume 9268 of Lecture Notes in Computer Science, 76--92, 2015. Springer

Details
Bibtex

KurzfassungAbstract
Message sequence charts (MSCs) and their higher-order formalism in terms of message sequence graphs (MSGs) provide an intuitive way to describe communication scenarios. Naturally, quantitative aspects such as the probability of failure, maximal latency or the expected energy consumption play a crucial role for communication systems. In this paper, we introduce quantitative MSGs with costs or rewards and stochastic timing information in terms of rates. To perform a quantitative analysis, we propose a branching-time semantics for MSGs as possibly infinite continuous-time Markov chains (CTMCs) interpreting delayed choice on the partial-order semantics of MSGs. Whereas for locally synchronized MSGs a finite-state bisimulation quotient can be found and thus, standard algorithms for CTMCs can be applied, this is not the case in general. However, using a truncation-based approach we show how approximative solutions can be obtained. Our implementation shows feasibility of this approach exploiting reliability, resilience and energy consumption.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-22975-1_6.

@inproceedings{DB2015,
  author    = {Clemens Dubslaff and Christel Baier},
  title     = {Quantitative Analysis of Communication Scenarios},
  booktitle = {Proc. of the 13th International Conference on Formal Modeling and
               Analysis of Timed Systems (FORMATS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9268},
  publisher = {Springer},
  year      = {2015},
  pages     = {76--92},
  doi       = {10.1007/978-3-319-22975-1_6}
}