Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures (Lecture Notes in Computer Science, 2067)

✍ Scribed by Franck Cassez (editor), Claude Jard (editor), Brigitte Rozoy (editor), Mark D. Ryan (editor)

• Publisher: Springer
• Year: 2001
• Tongue: English
• Leaves: 228
• Category: Library

✦ Synopsis

Daily life relies more and more on safety critical systems, e.g. in areas such as power plant control, traffic management, flight control, and many more. MOVEP is a school devoted to the broad subject of modeling and verifying software and hardware systems.
This volume contains tutorials and annotated bibliographies covering the main subjects addressed at MOVEP 2000. The four tutorials deal with Model Checking, Theorem Proving, Composition and Abstraction Techniques, and Timed Systems. Three research papers give detailed views of High-Level Message Sequence Charts, Industrial Applications of Model Checking, and the use of Formal Methods in Security. Finally, four annotated bibliographies give an overview of Infinite State Space Systems, Testing Transition Systems, Fault-Model-Driven Test Derivation, and Mobile Processes.

✦ Table of Contents

Modeling and Verification of Parallel Processes
Foreword
Program Committee
Contents
Model Checking: A Tutorial Overview
Introduction
Analysis of a Cryptographic Protocol
Description of the Protocol
A Promela Model
Model Checki g the Protocol
Systems and Properties
Transition Systems
Properties and Temporal Logic
omega-Automata
Temporal Logic and Automata
Algorithms for Model Checking
Local PTL Model Checki g
Global CTL Model Checki g
Symbolic Model Checking
Partial-Order Reductions
Further Topics
References
Theorem Proving for Verification
Introduction
Choice of Logic and Language
Basic Mechanization
The Challenge of Human Guidance
Verifying Parallel Processes
Abstraction
Automated Abstraction
Summary
References
Example:Bakery
Inductive Invariance Proof
Proof by Manual Abstraction andModel Checking
Proof by AutomatedAbstraction andModel Checking
Composition and Abstraction
Introduction
Systems and Their Behaviour
The Architecture of the Example System
The Servers
Labelled Transition Systems
“Sameness ”of LTSs
The Clients
Putting the System Together
A Digression on the Parallel Composition Operator
Verification
Requirements
Introduction to Abstraction
CFFD-Equivalence
The Meaning of “CFFD ”
Compositional LTS Construction
Interface Speci .cations
Induction
Discussion
References
UPPAAL - Now, Next, and Future
Current Version of Uppaal
Background
The Latest Uppaal Release Version
New Directions of Uppaal
COUppaal :Cost-Optimal Search
Parametric-Uppaal :Solving Parameterized Reachability Problems
Stopwatch-Uppaal :From Timed Automata to Hybrid Systems
PrUppaal :Probabilistic Timed Automata
HUppaal :Hierarchical Structures for Modeling
ExUppaal :Executable Timed Automata
Hybrid Automata Animation
Recent Developments in Uppaal
CDD ’s:Clock Di .erence Diagrams
Compact Representation of States
Partial Order Reduction for Timed Systems
DUppaal :Distributed State Space Exploration
Dynamic Partitioning:Tackling the State Explosion Problem
Recent Case Studies
Online Available Distributions
References
HMSCs as Partial Specifications ... with PNs as Completions
Introduction
Notations
Basic Message Sequence Charts
High Level Message Sequence Charts
Using HMSCs as Behavioural Speci .cations?
Undecidability Results
Recognizable and Rational Sets and Relations
Marked Sets and Pre .x Sets
A Reduction Yielding Negative Decision Results for HMSCs
Should HMSCs Be Considered as Speci .cations?
Petri Net Realization of HMSC Languages
Commutative Images of HMSC Languages Are Semilinear
Petri Net Closures of HMSC Languages
An Undecidability Result
Distributed Net Realizations of HMSCs
Model-Checking Petri Net Realizations of HMSCs
Case Studies
A HMSC with Non-local Choice
A Non-regular HMSC Language
Conclusion
References
Industrial Applications of Model Checking
Introduction
Formal Design of a Communication Protocol
Informal Description of the Protocol
Formal Speci .cation
Formal Veri .cation
Formel Design of an Embedded Control System
Informal Description of the Embedded System
The Structured Formal Speci .cation Methodology
Customization of the Formal Veri .cation Tools
Conclusions
References
Formal Methods in Practice: The Missing Links. A Perspective from the Security Area
Introduction
Challenges and Pitfalls
Formal and Informal:Integration Rather than Opposition
Establish Links
TL-FIT:Linking Formal and Informal Descriptions
TL-CAT:Linking Speci .cations and Test Suites
Conclusion
References
Verification of Systems with an Infinite State Space
Testing Transition Systems: An Annotated Bibliography
Formal Testing Theory
Test Frameworks
Formal Test Generation
Asynchronous Test Contexts
Test Generation Tools
Current Developments
Other Formal Approaches to Testing
References
Mobile Processes: A Commented Bibliography
Introduction
Mobility of Names
The Signi .cance of Names
The π -Calculus
Equational Theoryand Properties of Processes
The π -Calculus as a Programming Model
Verification and Type Systems
Locality-Based Semantics
Mobility of Processes
Distributed Process Calculi
The Ambient Calculus
Summary
References
Author Index