Integrating stochastic reasoning into Event-B development

DOI10.1007/S00165-014-0305-ZzbMATH Open1328.68039OpenAlexW1990752815MaRDI QIDQ903513FDOQ903513

Authors: Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis 

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

Recommendations

• A framework for formal dynamic dependability analysis using HOL theorem proving
• Formal dependability modeling and analysis: a survey
• Qualitative Probabilistic Modelling in Event-B
• A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems
• Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects

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) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Reliability, testing and fault tolerance of networks and computer systems (68M15) Specification and verification (program logics, model checking, etc.) (68Q60) Computer system organization (68M99)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Refinement Calculus
• Bisimulation through probabilistic testing
• Title not available (Why is that?)
• Modeling in Event B. System and software engineering.
• The B-Book
• Abstraction, Refinement and Proof for Probabilistic Systems
• Title not available (Why is that?)
• Qualitative Probabilistic Modelling in Event-B
• Refinement algebra for probabilistic programs
• Title not available (Why is that?)
• Unifying Probability
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)

Cited In (3)

• Title not available (Why is that?)
• Modelling resilient collaborative multi-agent systems
• Consistency-preserving refactoring of refinement structures in Event-B models

Uses Software

• PRISM
• UNITY

This page was built for publication: Integrating stochastic reasoning into Event-B development

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q903513)