Tools and Algorithms for the Construction and Analysis of Systems: Second International Workshop, TACAS ’96 Passau, Germany, March 27–29, 1996 Proceedings

Gerard J. Holzmann (auth.), Tiziana Margaria, Bernhard Steffen (eds.)3540610421, 9783540610427

This book presents the refereed proceedings of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’96, held in Passau, Germany in March 1996.
The book presents 19 revised full papers selected from a total of 47 submissions together with 11 tool presentations and 3 invited papers. The collection of papers addresses all current aspects of the design and analysis of distributed systems; the volume is organized in topical sections on tools, model checking and testing, security, models and methods, case studies, and logic and programs.

---

Table of contents :
Early fault detection tools….Pages 1-13
Kleene algebra with tests and commutativity conditions….Pages 14-33
Managing proofs….Pages 34-34
An analyzer for message sequence charts….Pages 35-48
Relation-algebraic analysis of Petri nets with RELVIEW….Pages 49-69
Efficient search as a means of executing specifications….Pages 70-86
An improvement of McMillan’s unfolding algorithm….Pages 87-106
Efficient local model-checking for fragments of the modal Μ-calculus….Pages 107-126
Test generation with inputs, outputs, and quiescence….Pages 127-146
Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR….Pages 147-166
Automatic compositional verification of some Security properties….Pages 167-186
Permutable agents in process algebras….Pages 187-206
Strategy construction in infinite games with Streett and Rabin chain winning conditions….Pages 207-224
Timed Condition/Event systems: A framework for modular discrete models of chemical plants and verification of their real-time discrete control….Pages 225-240
Formal verification of a partial-order reduction technique for model checking….Pages 241-257
Fully automatic verification and error detection for parameterized iterative sequential circuits….Pages 258-277
Priorities for modeling and verifying distributed systems….Pages 278-297
Games and modal mu-calculus….Pages 298-312
Generic system support for deductive program development….Pages 313-328
Extending promela and spin for real time….Pages 329-348
Reactive EFSMs — Reactive Promela/RSPIN….Pages 349-368
Probabilistic duration automata for analyzing real-time systems….Pages 369-390
The Concurrency Factory software development environment….Pages 391-395
The Fc2Tools set (tool demonstration)….Pages 396-396
PEP — more than a Petri Net tool….Pages 397-401
Rapid prototyping for an assertional specification language….Pages 402-406
cTc — A tool supporting the construction of cTLA-Specifications….Pages 407-411
A tool for proving invariance properties of concurrent systems automatically….Pages 412-416
Using the constraint language toupie for “Software Cost Reduction” specification analysis….Pages 417-417
A constraint-oriented Service Creation Environment….Pages 418-421
DFA&OPT-MetaFrame: A tool kit for program analysis and optimization….Pages 422-426
A construction and analysis tool based on the stochastic process algebra TIPP….Pages 427-430
Uppaal in 1995….Pages 431-434