Integrating stochastic reasoning into Event-B development

DOI10.1007/S00165-014-0305-ZMaRDI QIDQ903513zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 420890 (Why is no real title available?)
• scientific article; zbMATH DE number 3145626 (Why is no real title available?)
• scientific article; zbMATH DE number 1303997 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• scientific article; zbMATH DE number 1400096 (Why is no real title available?)
• scientific article; zbMATH DE number 5685899 (Why is no real title available?)
• A unification of probabilistic choice within a design-based model of reversible computation
• Abstraction, Refinement and Proof for Probabilistic Systems
• Bisimulation through probabilistic testing
• Extensions of the UNITY methodology: compositionality, fairness and probability in parallelism
• Modeling in Event B. System and software engineering.
• Qualitative Probabilistic Modelling in Event-B
• Refinement Calculus
• Refinement algebra for probabilistic programs
• The B-Book
• The critical discount factor for finite Markovian decision processes with an absorbing set
• Unifying Probability

Cited in

(3)

• scientific article; zbMATH DE number 6452641 (Why is no real title available?)
• Modelling resilient collaborative multi-agent systems
• Consistency-preserving refactoring of refinement structures in Event-B models

Describes a project that uses

Uses Software

• UNITY
• PRISM

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)