Table of Contents |
| Contributors | ix |
| Preface | xi |
| Programme Committee and Referees | xiii |
| Acknowledgements | xv |
Part 1 | Verification and Theorem Proving | |
| 1. | Formal Verification of the TTP Group Membership Algorithm / H. Pfeifer | 3 |
| 2. | Verification of a Sliding Window Protocol Using IOA and MONA / M. A. Smith, N. Klarlund | 19 |
| 3. | A Priori Verification of Reactive Systems / M. Majster-Cederbaum, F. Salger, M. Sorea | 35 |
Part 2 | Test Generation | |
| 4. | From Rule-based to Automata-based Testing / K. Etessami, M. Yannakakis | 53 |
| 5. | Integrated System Interoperability Testing with Applications to VOIP / N. Griffeth, R. Hao, D. Lee, R. K. Sinha | 69 |
| 6. | On Test Derivation from Partial Specifications / A. Petrenko, N. Yevtushenko | 85 |
Part 3 | Model Checking - Theory | |
| 7. | Compositionality for Improving Model Checking / A. Santone | 105 |
| 8. | A Model Checking Method for Partially Symmetric Systems / S. Haddad, J.-M. Ilie, K. Ajami | 121 |
Part 4 | Model Checking - Applications | |
| 9. | Specification and Verification of Message Sequence Charts / D. Peled | 139 |
| 10. | A State-Exploration Technique for Spi-Calculus Testing Equivalence Verification / L. Durante, R. Sisto, A. Valenzano | 155 |
| 11. | Verification of Consistency Protocols via Infinite-State Symbolic Model Checking / G. Delzanno | 171 |
Part 5 | Multicast Protocol Analysis and Simulation | |
| 12. | Systematic Performance Evaluation of Multipoint Protocols / A. Helmy, S. Gupta, D. Estrin, A. Cerpa, Y. Yu | 189 |
| 13. | Simulating Multicast Transport Protocols in Estelle / J. Templemore-Finlayson, E. Borcoci | 205 |
| 14. | Generation of Realistic Signalling Traffic in an ISDN Load Test System using SDL User Models / T. Steinert, G. Roessler | 219 |
Part 6 | Exhaustive and Probabilistic Testing | |
| 15. | Satisfaction up to Liveness / U. Ultes-Nitsche | 237 |
| 16. | Testing IP Routing Protocols - From Probabilistic Algorithms to a Software Tool / R. Hao, D. Lee, R. K. Sinha, D. Vlah | 249 |
Part 7 | Hardware Specification, Implementation and Testing | |
| 17. | Verifying and Testing Asynchronous Circuits using LOTOS / J. He, K. J. Turner | 267 |
| 18. | Hardware implementation of Concurrent Periodic EFSM's / H. Katagiri, M. Kirimura, K. Yasumoto, T. Higashino, K. Taniguchi | 285 |
| 19. | Modeling Distributed Embedded Systems in Multiclock ESTEREL / B. Rajan, R. K. Shyamasundar | 301 |
Part 8 | Formal Semantics | |
| 20. | Compact Net Semantics for Process Algebras / M. Bernardo, M. Ribaudo, N. Busi | 319 |
| 21. | A Concise Compositional Statecharts Semantics Definition / M. von der Beeck | 335 |
| 22. | Implementing CCS in Maude / A. Verdejo, N. Marti-Oliet | 351 |
Part 9 | Invited Papers on Verification and Security | |
| 23. | From Refutation to Verification / J. Rushby | 369 |
| 24. | Process Algebraic Analysis of Cryptographic Protocols / M. Boreale, R. De Nicola, R. Pugliese | 375 |
| 25. | A Logic of Belief and a Model Checking Algorithm for Security Protocols / M. Benerecetti, F. Giunchiglia, M. Panti, L. Spalazzi | 393 |