PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level rule-based programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically analyzing various quantitative aspects of such models based on the samples that are generated through discrete-event simulation. Because distributed and concurrent communication protocols can be modelled using actors (concurrent objects with asynchronous message passing), we provide an actor PMaude module. The module aids writing specifications in a probabilistic actor formalism. This allows us to easily write specifications that are purely probabilistic – and not just non-deterministic. The absence of such (un-quantified) non-determinism in a probabilistic system is necessary for a form of statistical analysis that we also discuss. Specifically, we introduce a query language called Quantitative Temporal Expressions (or QuaTEx in short), to query various quantitative aspects of a probabilistic model. We also describe a statistical technique to evaluate QuaTEx expressions for a probabilistic model

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Dantas, Yuri Gil; Lemos, Marcilio O.O.; Fonseca, Iguatemi E.; Nigam, Vivek: Formal specification and verification of a selective defense for TDos attacks (2016)
  2. Elleuch, Maissa; Hasan, Osman; Tahar, Sofiène; Abid, Mohamed: Formal probabilistic analysis of detection properties in wireless sensor networks (2015)
  3. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014)
  4. Bentea, Lucian; Ölveczky, Peter Csaba: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing (2013)
  5. Eckhardt, Jonas; Mühlbauer, Tobias; Meseguer, José; Wirsing, Martin: Statistical model checking for composite actor systems (2013)
  6. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  7. Bulychev, Peter; David, Alexandre; Guldstrand Larsen, Kim; Legay, Axel; Li, Guangyuan; Bøgsted Poulsen, Danny; Stainer, Amelie: Monitor-based statistical model checking for weighted metric temporal logic (2012)
  8. Katelman, Michael; Keller, Sean; Meseguer, José: Rewriting semantics of production rule sets (2012)
  9. Krause, Christian; Giese, Holger: Probabilistic graph transformation systems (2012)
  10. Meseguer, José: Twenty years of rewriting logic (2012)
  11. Wirsing, Martin; Eckhardt, Jonas; Mühlbauer, Tobias; Meseguer, José: Design and analysis of cloud-based architectures with KLAIM and Maude (2012)
  12. AlTurki, Musab; Meseguer, José: PVeSTA: A parallel statistical model checking and quantitative analysis tool (2011)
  13. Ölveczky, Peter Csaba; Thorvaldsen, Stian: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude (2009)
  14. Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
  15. Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Martí-Oliet, Narciso; Meseguer, José; Talcott, Carolyn: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. (2007)
  16. Ölveczky, Peter Csaba; Meseguer, José; Talcott, Carolyn L.: Specification and analysis of the AER/NCA active network protocol suite in real-time Maude (2006)
  17. Meseguer, José: A rewriting logic sampler (2005)