Tools and Algorithms for the Construction and Analysis of Systems: 8th International Conference, TACAS 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings

Michael R. Lowry (auth.), Joost-Pieter Katoen, Perdita Stevens (eds.)9783540434191, 3540434194

ETAPS 2002 was the ?fth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998by combining a number of existing and new conferences. This year it comprised 5 conferences (FOSSACS, FASE, ESOP, CC, TACAS), 13 satellite workshops (ACL2, AGT, CMCS, COCV, DCC, INT, LDTA, SC, SFEDL, SLAP, SPIN, TPTS, and VISS), 8invited lectures (not including those speci?c to the satellite events), and several 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. Di?erent 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 :
Software Construction and Analysis Tools for Future Space Missions….Pages 1-19
Alloy: A New Technology for Software Modelling….Pages 20-20
Improving the Verification of Timed Systems Using Influence Information….Pages 21-36
Digitisation and Full Abstraction for Dense-Time Model Checking….Pages 37-51
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach….Pages 52-66
Timed Automata with Asynchronous Processes: Schedulability and Decidability….Pages 67-82
Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems….Pages 83-97
An Analysis of Zero-Clairvoyant Scheduling….Pages 98-112
Preemptive Job-Shop Scheduling Using Stopwatch Automata….Pages 113-126
Explicit Modeling of Influences, and of Their Absence, in Distributed Systems….Pages 127-141
A Functional Semantics of Attribute Grammars….Pages 142-157
Relative Completeness of Abstraction Refinement for Software Model Checking….Pages 158-172
Towards the Automated Verification of Multithreaded Java Programs….Pages 173-187
CLPS-B—A Constraint Solver for B….Pages 188-204
Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS….Pages 205-220
Beyond Parameterized Verification….Pages 221-235
Resource-Constrained Model Checking of Recursive Programs….Pages 236-250
Model Checking Large-Scale and Parameterized Resource Allocation Systems….Pages 251-265
Exploring Very Large State Spaces Using Genetic Algorithms….Pages 266-280
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems….Pages 281-295
The ForSpec Temporal Logic: A New Temporal Property-Specification Language….Pages 296-311
Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis….Pages 312-326
A Temporal Logic Based Theory of Test Coverage and Generation….Pages 327-341
Synthesizing Monitors for Safety Properties….Pages 342-356
Adaptive Model Checking….Pages 357-370
Parallelisation of the Petri Net Unfolding Algorithm….Pages 371-385
Black Box Unfolding with Local First Search….Pages 386-400
Applicability of Fair Simulation….Pages 401-414
Simulation as Coarsest Partition Problem….Pages 415-430
Temporal Debugging for Concurrent Systems….Pages 431-444
Fate and FreeWill in Error Traces….Pages 445-459
TIMES b— A Tool for Modelling and Implementation of Embedded Systems….Pages 460-464
Compositional Verification Using SVL Scripts….Pages 465-469
STG: A Symbolic Test Generation Tool….Pages 470-475
Real-Time Systems Design with PEP….Pages 476-480