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 : proc

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. 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

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.

The ACM 50th Anniversary edition of Computing Surveys contains two excellent papers describing the state of the art and research directions in Formal Methods [1] and Concurrency [2].