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.
Author(s): Bengt Jonsson, Wang Yi (auth.), Joost-Pieter Katoen (eds.)
Series: Lecture Notes in Computer Science 1601
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1999
Language: English
Pages: 362
Tags: Logics and Meanings of Programs; Software Engineering; Special Purpose and Application-Based Systems; Programming Languages, Compilers, Interpreters; Computer Communication Networks
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
