Tools and Algorithms for the Construction of Analysis of Systems : 5th International Conference, TACAS'99, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings

by Cleaveland, W. Rance

• ISBN13: 9783540657033
• ISBN10: 3540657037
• Format: Paperback
• Copyright: 1999-03-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'99, held in Amsterdam, The Netherlands in March 1999 as part of ETAPS'99. The 28 revised full papers presented were carefully reviewed and selected from a total of 82 submissions. Also included are one invited paper, a position statement, and one ETAPS tool demonstration. The papers are organized in topical sections on real-time systems, case studies, compositionality and abstraction, symbolic analysis, process algebras, frameworks for system construction and analysis, and tool descriptions.

Table of Contents

Invited Contribution
Modeling for Mere Mortals	1	(18)
J. Kramer
J. Magee
Real-Time
Scheduling System Verification	19	(15)
P.-A. Hsiung
F. Wang
Y.-S. Kuo
A Period Assignment Algorithm for Real-Time System Design	34	(10)
M.Ryu
S. Hong
Analyzing Stochastic Fixed-Priority Real-Time Systems	44	(15)
M. Gardner
J. Liu
Timed Diagnostics for Reachability Properties	59	(15)
S. Tripakis
Case Studies
Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools	74	(15)
Y. Dong
X. Du
Y. Ramakrishna
C. Ramakrishnan
I. Ramakrishnan
S. Smolka
O. Sokolsky
E. Stark
D. Warren
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL	89	(15)
C. Pusch
Automated Fast-Track Reconfiguration of Group Communication Systems	104	(15)
C. Kreitz
Specifications and Proofs for Ensemble Layers	119	(15)
J. Hickey
N. Lynch
R. Van Renesse
Compositionality and Abstraction
An Automated Analysis of Ping-Pong Interactions in E-Mail Services	134	(14)
A. Bergeron
J.-C. Manzoni
Automatic Verification of Cryptographic Protocols through Compositional Analysis Techniques	148	(15)
D. Marchignoli
F. Martinelli
Verification of Hierarchical State/Event Systems Using Reusability and Compositionality	163	(15)
G. Behrmann
K. Larsen
H. Andersen
H. Hulgaard
J. Lind-Nielsen
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction	178	(15)
V. Rusu
E. Singerman
Symbolic Analysis
Symbolic Model Checking without BDDs	193	(15)
A. Biere
A. Cimatti
E. Clarke
Y. Zhu
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol	208	(15)
P. Abdulla
A. Annichini
A. Bouajjani
Model Checking in CLP	223	(17)
G. Delzanno
A. Podelski
Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets	240	(15)
K. Heljanko
Process Algebra
Finite State Verification for the Asynchronous Pi-Calculus	255	(15)
U. Montanari
M. Pistore
Process Algebra in PVS	270	(15)
T. Basten
J. Hooman
On the Benefits of Using the Up to Techniques for Bisimulation Verification	285	(15)
D. Hirschkoff
Computing Strong/Weak Bisimulation Equivalences and Observation Congruence for Value-Passing Processes	300	(15)
Z. Li
H. Chen
Frameworks for System Construction and Analysis
Hardware Testing Using a Communication Protocol Conformance Testing Tool	315	(15)
H. Kahlouche
C. Viho
M. Zendri
A Light-Weight Framework for Hardware Verification	330	(15)
C. Kern
T. Ono-Tesfaye
M. Greenstreet
An Easily Extensible Toolset for Tabular Mathematical Expressions	345	(15)
D. L. Parnas
D. Peters
From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm Approach	360	(15)
J. Knoop
Tool Descriptions
A Theorem Prover-Based Analysis Tool for Object-Oriented Databases	375	(15)
D. Spelt
S. Even
DYANA: An Environment for Embedded System Design and Analysis	390	(15)
A. Bakhmurov
A. Kapitonova
R. Smeliansky
Path Exploration Tool	405	(15)
E. Gunter
D. Peled
Modular State Level Analysis of Distributed Systems Techniques and Tool Support	420	(15)
P. Buchholz
P. Kemper
Position Paper
Some Issues in the Software Engineering of Verification Tools	435	(4)
P. Stevens
ETAPS Tool Demonstration
The ETI Online Service in Action	439	(6)
V. Braun
J. Kreileder
T. Margaria
B. Steffen
Author Index	445