Tools and Algorithms for the Construction and 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

Jeff Kramer, Jeff Magee (auth.), W. Rance Cleaveland (eds.)3540657037, 9783540657033

ETAPS’99 is the second instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998 by combining a number of existing and new conferences. This year it comprises ve conferences (FOSSACS, FASE, ESOP, CC, TACAS), four satellite workshops (CMCS, AS, WAGA, CoFI), seven invited lectures, two invited tutorials, and six contributed tutorials. The events that comprise ETAPS address various aspects of the system – velopment process, including speci cation, design, implementation, analysis and improvement. The languages, methodologies and tools which support these – tivities are all well within its scope. Dieren t blends of theory and practice are represented, with an inclination towards theory with a practical motivation on one hand and soundly-based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.

---

Table of contents :
Modeling for Mere Mortals….Pages 1-18
Scheduling System Verification….Pages 19-33
A Period Assignment Algorithm for Real-Time System Design….Pages 34-43
Analyzing Stochastic Fixed-Priority Real-Time Systems….Pages 44-58
Timed Diagnostics for Reachability Properties….Pages 59-73
Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools….Pages 74-88
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL….Pages 89-103
Automated Fast-Track Reconfiguration of Group Communication Systems….Pages 104-118
Specifications and Proofs for Ensemble Layers….Pages 119-134
An Automated Analysis of Ping-Pong Interactions in E-Mail Services….Pages 134-147
Automatic Verification of Cryptographic Protocols through Compositional Analysis Techniques….Pages 148-162
Verification of Hierarchical State/Event Systems Using Reusability and Compositionality….Pages 163-177
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction….Pages 178-192
Symbolic Model Checking without BDDs….Pages 193-207
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol….Pages 208-222
Model Checking in CLP….Pages 223-239
Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets….Pages 240-254
Finite State Verification for the Asynchronous π-Calculus….Pages 255-269
Process Algebra in PVS….Pages 270-284
On the Benefits of Using the Up-To Techniques for Bisimulation Verification….Pages 285-299
Computing Strong/Weak Bisimulation Equivalences and Observation Congruence for Value-Passing Processes….Pages 300-314
Hardware Testing Using a Communication Protocol Conformance Testing Tool….Pages 315-329
A Light-Weight Framework for Hardware Verification….Pages 330-344
An Easily Extensible Toolset for Tabular Mathematical Expressions….Pages 345-359
From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm Approach….Pages 360-374
A Theorem Prover-Based Analysis Tool for Object-Oriented Databases….Pages 375-389
DYANA: An Environment for Embedded System Design and Analysis….Pages 390-404
Path Exploration Tool….Pages 405-419
Modular State Level Analysis of Distributed Systems Techniques and Tool Support….Pages 420-434
Some Issues in the Software Engineering of Verification Tools….Pages 435-438
The ETI Online Service in Action….Pages 439-443