Titel : 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
Dokumenttyp : Kongresswerk
ISBN : 3540434194
Erscheinungsjahr : 2002
Herausgeber : Katoen, Joost-Pieter Stevens, Perdita
Serientitel : Lecture Notes in Computer Science / LNCS
Bandnummer : 2280
Erste Seite : 1
Letzte Seite : 482
Tagungsname : The 8th International Conference TACAS 2002 & The Joint European
Conferences on Theory and Practice of Software, ETAPS , on Tools and
Algorithms for the Construction and Analysis of Systems April 8-12,
2002
Tagungsort : Grenoble, France
Tagungsjahr : 2002
Verlag : Springer, Berlin
Standort : 0105 (Serien)
Signatur : 09.2002F70
Archiviert am : 15.4.2002
Neuerwerbungsregal : von 16.4.2002 bis 22.4.2002
Inhaltsverzeichnis:
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
Hrsg.: Joost-Pieter Katoen Perdita Stevens
Springer, Berlin, 2002, 482 S.
ISBN 3540434194
( Lecture Notes in Computer Science / LNCS ; 2280 )
ISSN 03029743482
Table of Contents
Invited Contributions
Software Construction and Analysis Tools for Future Space Missions 1
Michael R. Lowry
Alloy: A New Technology for Software Modelling 20
Daniel Jackson
Real-Time and Probabilistic Systems
Improving the Verification of Timed Systems Using
Influence Information 21
Victor Braberman, Diego Garbervetsky, Alfredo Olivero
Digitisation and Full Abstraction for Dense-Time Model Checking 37
Joel Ouaknine
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. 52
Marta Kwiatkowska, Gethin Norman, David Parker
Scheduling
Timed Automata with Asynchronous Processes:
Schedulability and Decidability 67
Elena Fersman, Paul Pettersson, Wang Yi
Validating Timing Constraints of Dependent Jobs with Variable
Execution Times in Distributed Real-Time Systems 83
Hojung Cha, Rhan Ha
An Analysis of Zero-Clairvoyant Scheduling 98
K. Subramani
Preemptive Job-Shop Scheduling Using Stopwatch Automata 113
Yasmina Abdeddaim, Oded Maler
Miscellaneous
Explicit Modeling of Influences, and of Their Absence, in
Distributed Systems 127
Horst F. Wedde, Amim Wedig
A Functional Semantics of Attribute Grammars 142
Kevin Backhouse
Software Verification
Relative Completeness of Abstraction Refinement for Software
Model Checking 158
Thomas Ball, Andreas Podelski, Sriram K. Rajamani
Towards the Automated Verification of Multithreaded Java Programs 173
Giorgio Delzanno, Jean-Francois Raskin, Laurent Van Begin
CLPS-B - A Constraint Solver for B 188
Fabrice Bouquet, Bruno Legeard, Fabien Peureux
Formal Verification of Functional Properties of an SCR-Style
Software Requirements Specification Using PVS 205
Taeho Kim, David Stringer-Calvert, Sungdeok Cha
Infinite-State and Parametric Systems
Beyond Parameterized Verification 221
Marco Bozzano, Giorgio Delzanno
Resource-Constrained Model Checking of Recursive Programs 236
Samik Basu, K. Narayan Kumar, L. Robert Pokorny,
C.R. Ramakrishnan
Model Checking Large-Scale and
Parameterized Resource Allocation Systems 251
E. Allen Emerson, Vineet Kahlon
Model Checking: Logics and Algorithms
Exploring Very Large State Spaces Using Genetic Algorithms 266
Patrice Godefroid, Sarfraz Khurshid
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled
Transition Systems 281
Radu Mateescu
The ForSpec Temporal Logic: A New Temporal
Property-Specification Language 296
Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg,
Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singer-man,
Andreas Tiemeyer, Moshe Y. Vardi, Yael Zbar
Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis 312
HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi
Model Checking and Testing
A Temporal Logic Based Theory of Test Coverage and Generation 327
Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Hasan Ural
Synthesizing Monitors for Safety Properties 342
Klaus Havelund, Grigore Rosu
Adaptive Model Checking 357
Alex Groce, Doron Peled, Mihalis Yannakakis
Partial-Order and Simulation Techniques
Parallelisation of the Petri Net Unfolding Algorithm 371
Keijo Heljanko, Victor Khomenko, Maciej Koutny
Black Box Unfolding with Local First Search 386
Sebastien Bornot, Remi Morin, Peter Niebert, Sarah Zennou
Applicability of Fair Simulation 401
Doron Bustan, Orna Grumberg
Simulation as Coarsest Partition Problem 415
Raffaella Gentilini, Carla Piazza, Alberto Policriti
Debugging with Model Checking
Temporal Debugging Or Concurrent System 431
Elsa Gunter, Doron Peled
Fate and Free Will in Error Traces 445
HoonSang Jin, Kavita Ravi, Fabio Somenzi
Tool Papers
TIMES - A Tool for Modelling and Implementation of
Embedded Systems 460
Tobias Aranell, Elena Fersman, Leonid Mokrushin, Paul Pettersson,
Wang Yi
Compositional Verification Using SVL Scripts 465
Frederic Lang
STG: A Symbolic Test Generation Tool 470
Duncan Clarke, Thierry Jeron, Vlad Rusu, Elena Zinovieva
Real-Time Systems Design with PEP 476
Christian Stehno
Author Index 481
040020279390