Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999, Proceedings (Lecture Notes in Computer Science (1601))

This book constitutes the refereed proceedings of the Fifth International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, ARTS '99, held in Bamberg, Germany in May 1999. The 17 revised full papers presented together with three invited contributions were carefully reviewed and selected from 33 submissions. The papers are organized in topical sections on verification of probabilistic systems, model checking for probabilistic systems, semantics of probabilistic process calculi, semantics of real-time processes, real-time compilation, stochastic process algebra, and modeling and verification of real-time systems. Fully Abstract Characterization of Probabilistic May Testing....Pages 1-18 Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms....Pages 19-33 Establishing Qualitative Properties for Probabilistic Lossy Channel Systems....Pages 34-52 Root Contention in IEEE 1394....Pages 53-74 Automatic Verification of Real-Time Systems with Discrete Probability Distributions....Pages 75-95 ProbVerus: Probabilistic Symbolic Model Checking....Pages 96-110 Process Algebra with Probabilistic Choice....Pages 111-129 An Axiomatization of Probabilistic Testing....Pages 130-150 Verification of Hybrid Systems....Pages 151-151 A Parallel Operator for Real-Time Processes with Predicate Transformer Semantics....Pages 152-171 Comparing the Efficiency of Asynchronous Systems....Pages 172-191 A Formal Model of Real-Time Program Compilation....Pages 192-210 Specifying Performance Measures for PEPA....Pages 211-227 Semi-numerical Solution of Stochastic Process Algebra Models....Pages 228-243 Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation....Pages 244-264 Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach....Pages 265-276 Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal ....Pages 277-298 Verifying Progress in Timed Systems....Pages 299-314 Proof Assistance for Real-Time Systems Using an Interactive Theorem Prover....Pages 315-333 Modelling Timeouts without Timelocks....Pages 334-353

This book constitutes the refereed proceedings of the Fifth International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, ARTS '99, held in Bamberg, Germany in May 1999.
The 17 revised full papers presented together with three invited contributions were carefully reviewed and selected from 33 submissions. The papers are organized in topical sections on verification of probabilistic systems, model checking for probabilistic systems, semantics of probabilistic process calculi, semantics of real-time processes, real-time compilation, shastic process algebra, and modeling and verification of real-time systems.

Selected papers and invited contributions from the 5th International AMAST Workshop on Formal Methods for Real Time and Probabilistic Systems. Topics covered include verification and model checking for probabilistic systems, semantics of probabilistic process calculi and stochastic process algebra.