Performance analysis and functional verification of the stop-and-wait protocol in HOL

DOI10.1007/s10817-008-9105-6zbMath1191.68101OpenAlexW2136755926MaRDI QIDQ1040781

Sofiène Tahar, Osman Hasan

Publication date: 25 November 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://spectrum.library.concordia.ca/974503/1/performance_analysis_and_functional_verification.pdf

zbMATH Keywords

real-time systemsprobability theorycommunication protocolsHOL theorem proverhigher-order-logic

Mathematics Subject Classification ID

Related Items (2)

Reasoning about conditional probabilities in a higher-order-logic theorem prover ⋮ Formalization of Normal Random Variables in HOL

Uses Software

• PRISM
• Rabbit
• Uppaal

Cites Work

• Isabelle. A generic theorem prover
• Automatic verification of real-time systems with discrete probability distributions.
• Stochastic Model Checking
• Verification of Expectation Properties for Discrete Random Variables in HOL
• Formalization of Continuous Probability Distributions
• Verification of Tail Distribution Bounds in a Theorem Prover
• Model Checking Software
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Performance analysis and functional verification of the stop-and-wait protocol in HOL