Tools and Algorithms for the Construction and Analysis of Systems : 7th International Conference, TACAS 2001, Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001: Proceedings

by Tacas 200 (2001 Genoa, Italy); Yi, Wang

• ISBN13: 9783540418658
• ISBN10: 3540418652
• Format: Paperback
• Copyright: 2001-04-01
• Publisher: Springer Verlag

Summary

This practical book gives a comprehensive introduction to the concepts and languages of the new standard IEC 61131 used to program industrial control systems. A summary of the special requirements in programming industrial automation systems and the corresponding features in the IEC 61131-3 standard makes it suitable for students as well as PLC experts. The material is presented in an easy-to-understand form using numerous examples, illustrations and summary tables. There is also a purchaser's guide and a CD-ROM containing two reduced but functional versions of programming systems. These increase the value of the book for PLC programmers and for those in charge of purchasing software in industrial companies.

Table of Contents

Invited Contributions
Branching vs. Linear Time: Final Showdown	1	(22)
M. Y. Vardi
Propositional Reasoning	23	(1)
M. P. Fourman
Symbolic Verification
Language Containment Checking with Nondeterministic BDDs	24	(15)
B. Finkbeiner
Satisfiability Checking Using Boolean Expression Diagrams	39	(13)
P.F. Williams
H. Reif Andersen
H. Hulgaard
A Library for Composite Symbolic Representations	52	(15)
T. Yavuz-Kahveci
M. Tuncer
T. Bultan
Infinite State Systems: Deduction and Abstraction
Synthesis of Linear Ranking Functions	67	(15)
M. A. Colon
H.B. Sipma
Automatic Deductive Verification with Invisible Invariants	82	(16)
A. Pnueli
S. Ruah
L. Zuck
Incremental Verification by Abstraction	98	(15)
Y. Lakhnech
S. Bensalem
S. Berezin
S. Owre
A Technique for Invariant Generation	113	(15)
A. Tiwari
H. Rueb
H. Saidi
N. Shankar
Application for Model Checking Techniques
Model Checking Syllabi and Student Careers	128	(15)
R. Sebastiani
A. Tomasi
F. Giunchiglia
Verification of Vortex Workflows	143	(15)
X. Fu
T. Bultan
R. Hull
J. Su
Parameterized Verification of Multithreaded Software Libraries	158	(16)
T. Ball
S. Chaki
S. K. Rajamani
Timed and Probabilistic Systems
Efficient Guilding Towards Cost-Optimality in UPPAL	174	(15)
G. Behrmann
A. Fehnker
T. Hune
K. Larsen
P. Pettersson
J. Romijn
Linear Parametric Model Checking of Timed Automata	189	(15)
T. Hune
J. Romijn
M. Stoelinga
F. Vaandrager
Abstraction in Probabilistic Process Algebra	204	(16)
S. Andova
J. C. M. Baeten
First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders	220	(16)
T. C. Ruys
R. Langerak
J.-P. Katoen
D. Latella
M. Massink
Hardware: Design and Verification
Hardware/Software Co-design Using Functional Languages	236	(16)
A. Mycroft
R. Sharp
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors	252	(16)
M. N. Velev
Software Verification
Boolean and Cartesian Abstraction for Model Checking C programs	268	(16)
T. Ball
A. Podelski
S. K. Rajamani
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs	284	(15)
C. S. Pasareanu
M. B. Dwyer
W. Visser
The LOOP Compiler for Java and JML	299	(14)
J. van den Berg
B. Jacobs
Symbolic Verification
Searching Powerset Automata by the Combining Explicit-State and Symbolic Model Checking	313	(15)
A. Cimatti
M. Roverti
P. Bertoli
Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation	328	(15)
G. Ciardo
G. Luttgen
R. Siminiceanu
Testing: Techniques and Tools
Automated Test Generation from Timed Automata	343	(15)
B. Nielsen
A. Skou
Testing an Intentional Naming Scheme Using Genetic Algorithms	358	(15)
S. Khurshid
Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions	373	(16)
F. Ricca
P. Tonella
TATOO: Testing and Analysis Tool for Object-Oriented Software	389	(15)
A. L. Souter
T. M. Wong
S. A. Shindo
L. L. Pollock
Implementation Techniques
Implementing a Multi-valued Symbolic Model Checker	404	(16)
M. Chechik
B. Devereux
S. Easterbrook
Is There a Best Symbolic Cycle-Detection Algorithm?	420	(15)
K. Fisler
R. Fraer
G. Kamhi
M. Y. Vardi
Z. Yang
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets	435	(15)
R. Carvajal-Schiaffino
G. Delzanno
G. Chiola
A Sweep-Line Method for State Space Exploration	450	(15)
S. Christensen
L. M. Kristensen
T. Mailund
Semantics and Compositional Verification
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams	465	(15)
N. Amla
E. A. Emerson
K. Namjoshi
R. Trefler
Simulation Revisited	480	(16)
L. Tan
R. Cleaveland
Compositional Message Sequence Charts	496	(16)
E. L. Gunter
A. Muscholl
D. A. Peled
An Automata Based Interpretation of Live Sequence Charts	512	(16)
J. Klose
H. Wittke
Logics and Model-Checking
Coverage Metrics for Temporal Logic Model Checking	528	(15)
H. Chockler
O. Kupferman
M. Y. Vardi
Paralleld Model Checking for the Alternation Free μ-Calculus	543	(16)
B. Bollig
M. Leucker
M. Weber
Model Checking CTL*[DC]	559	(15)
P. K. Pandya
ETAPS Tool Demonstration
CPN/Tools: A Tool for Editing and Simulating Coloured Peteri Nets ETAPS Tool Demonstration Related to TACAS	574	(4)
M. Beaudouin-Lafon
W. E. Mackay
M. Jensen
P. Andersen
P. Janecek
M. Lassen
K. Lund
K. Mortensen
S. Munck
A. Ratzer
K. Ravn
S. Christensen
K. Jensen
The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models	578	(4)
G. Del Castillo
The Erlang Verification Tool	582	(5)
T. Noll
L. Fredlund
D. Gurov
Author Index	587