Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000 Nantes, France, June 19–23, 2000 Revised Tutorial Lectures

Stephan Merz (auth.), Franck Cassez, Claude Jard, Brigitte Rozoy, Mark Dermot Ryan (eds.)3540427872, 9783540427872

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 :
Model Checking: A Tutorial Overview….Pages 3-38
Theorem Proving for Verification….Pages 39-57
Composition and Abstraction….Pages 58-98
UPPAAL – Now, Next, and Future….Pages 99-124
HMSCs as Partial Specifications…with PNs as Completions….Pages 125-152
Industrial Applications of Model Checking….Pages 153-168
Formal Methods in Practice: The Missing Links. A Perspective from the Security Area….Pages 169-180
Verification of Systems with an Infinite State Space….Pages 183-186
Testing Transition Systems: An Annotated Bibliography….Pages 187-195
Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography….Pages 196-205
Mobile Processes: A Commented Bibliography….Pages 206-222