Integrating stochastic reasoning into Event-B development

DOI10.1007/s00165-014-0305-zzbMath1328.68039OpenAlexW1990752815MaRDI QIDQ903513

Anton Tarasyuk, Linas Laibinis, Elena Troubitsyna

Publication date: 6 January 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-014-0305-z

zbMATH Keywords

reliabilityMarkov processesrefinementprobabilistic reasoningEvent-Bresponsivenesscyclic systems

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Computer system organization (68M99) Reliability, testing and fault tolerance of networks and computer systems (68M15) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Consistency-preserving refactoring of refinement structures in Event-B models, Modelling resilient collaborative multi-agent systems

Uses Software

• PRISM
• UNITY

Cites Work

• Bisimulation through probabilistic testing
• The critical discount factor for finite Markovian decision processes with an absorbing set
• Extensions of the UNITY methodology: compositionality, fairness and probability in parallelism
• A unification of probabilistic choice within a design-based model of reversible computation
• Refinement algebra for probabilistic programs
• Qualitative Probabilistic Modelling in Event-B
• The B-Book
• Refinement Calculus
• Abstraction, Refinement and Proof for Probabilistic Systems
• Unifying Probability
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item