Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects

DOI10.1007/S10703-010-0107-8MaRDI QIDQ633299zbMATH OpenOpenAlexFDO

Authors Benoît Delahaye, Benoît Caillaud, Axel Legay

Publication date 31 March 2011

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-010-0107-8

zbMATH Keywords

contractsprobabilistic reasoningavailabilityreliability analysisassume/guarantee reasoning

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Reliability, availability, maintenance, inspection in operations research (90B25) Specification and verification (program logics, model checking, etc.) (68Q60) Stochastic systems in control theory (general) (93E03)

Recommendations

• Probabilistic Contracts for Component-Based Design
• Probabilistic contracts for component-based design
• Assume-guarantee contracts for continuous-time systems
• Assume-guarantee verification for probabilistic systems
• scientific article; zbMATH DE number 1863173

Cites work

• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1232241 (Why is no real title available?)
• scientific article; zbMATH DE number 1863173 (Why is no real title available?)
• scientific article; zbMATH DE number 3254905 (Why is no real title available?)
• A logic for reasoning about time and reliability
• Alternating-time temporal logic
• Assume-guarantee verification for probabilistic systems
• Automatic Conflict Detection on Contracts
• Challenges in the Specification of Full Contracts
• Computer Aided Verification
• Computer Aided Verification
• Frontiers of Combining Systems
• Interactive Markov chains. And the quest for quantified quality
• Modal specifications for the control theory of discrete event systems
• Multiple Viewpoint Contract-Based Specification and Design
• On simulation-based probabilistic model checking of mixed-analog circuits
• Reasoning about infinite computations
• Refinement and Consistency of Timed Modal Specifications
• Temporal logic can be more expressive
• Tools and Algorithms for the Construction and Analysis of Systems
• Validation of Stochastic Systems
• Verification, Model Checking, and Abstract Interpretation
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(12)

• Preserving Contract Satisfiability Under Non-monotonic Composition
• Contracts for schedulability analysis
• Conditions of contracts for separating responsibilities in heterogeneous systems
• Unifying theories of reactive design contracts
• Model checking probabilistic systems
• Probabilistic contracts for component-based design
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Integrating stochastic reasoning into Event-B development
• Assume-guarantee contracts for continuous-time systems
• Quantitative multi-objective verification for probabilistic systems
• Probabilistic Contracts for Component-Based Design
• scientific article; zbMATH DE number 1863173 (Why is no real title available?)

Describes a project that uses

Uses Software

• LiQuor
• D-Finder
• CLAN

This page was built for publication: Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects

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