Tools and Algorithms for the Construction of Analysis of Systems

1. Front Matter

   Pages I-XI

   PDF

2. Invited Contribution

   1. Modeling for Mere Mortals

      • Jeff Kramer, Jeff Magee

      Pages 1-18

3. Real-Time

   1. Scheduling System Verification

      • Pao-Ann Hsiung, Farn Wang, Yue-Sun Kuo

      Pages 19-33

   2. A Period Assignment Algorithm for Real-Time System Design

      • Minsoo Ryu, Seongsoo Hong

      Pages 34-43

   3. Analyzing Stochastic Fixed-Priority Real-Time Systems

      • Mark K. Gardner, Jane W. S. Liu

      Pages 44-58

   4. Timed Diagnostics for Reachability Properties

      • Stavros Tripakis

      Pages 59-73

4. Case Studies

   1. Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools

      • Yifei Dong, Xiaoqun Du, Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka et al.

      Pages 74-88

   2. Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL

      • Cornelia Pusch

      Pages 89-103

   3. Automated Fast-Track Reconfiguration of Group Communication Systems

      • Christoph Kreitz

      Pages 104-118

   4. Specifications and Proofs for Ensemble Layers

      • Jason Hickey, Nancy Lynch, Robbert van Renesse

      Pages 119-134

5. Compositionality and Abstraction

   1. An Automated Analysis of Ping-Pong Interactions in E-Mail Services

      • Anne Bergeron, Jean-Christophe Manzoni

      Pages 134-147

   2. Automatic Verification of Cryptographic Protocols through Compositional Analysis Techniques

      • Davide Marchignoli, Fabio Martinelli

      Pages 148-162

   3. Verification of Hierarchical State/Event Systems Using Reusability and Compositionality

      • Gerd Behrmann, Kim G. Larsen, Henrik R. Andersen, Henrik Hulgaard, Jørn Lind-Nielsen

      Pages 163-177

   4. On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction

      • Vlad Rusu, Eli Singerman

      Pages 178-192

6. Symbolic Analysis

   1. Symbolic Model Checking without BDDs

      • Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu

      Pages 193-207

   2. Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol

      • Parosh Abdulla, Aurore Annichini, Ahmed Bouajjani

      Pages 208-222

   3. Model Checking in CLP

      • Giorgio Delzanno, Andreas Podelski

      Pages 223-239

   4. Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets

      • Keijo Heljanko

      Pages 240-254

7. Process Algebra

   1. Finite State Verification for the Asynchronous π-Calculus

      • Ugo Montanari, Marco Pistore

      Pages 255-269

   2. Process Algebra in PVS

      • Twan Basten, Jozef Hooman

      Pages 270-284

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.

• Algorithms
• Analysis
• Formal Methods
• Real-Time Systems
• Software Tols
• Systems Analysis
• Systems Design
• algebra
• algorithm
• real-time
• system

• Department of Computer Science, State University of New York at Stony Brook, Stony Brook, USA

  W. Rance Cleaveland

Policies and ethics