## Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures, Volume 4Daily 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. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

A Tutorial Overview | 3 |

Theorem Proving for Verification | 39 |

Composition and Abstraction | 58 |

UPPAAL Now Next and Future | 99 |

HMSCs as Partial Specifications with PNs as Completions | 125 |

Industrial Applications of Model Checking | 153 |

The Missing Links A Perspective from the Security Area | 169 |

Verification of Systems with an Infinite State Space | 181 |

An Annotated Bibliography | 187 |

A Commented Bibliography | 206 |

Author Index | 223 |

### Other editions - View all

Modeling and Verification of Parallel Processes Franck Cassez,Claude Jard,Brigitte Rozoy No preview available - 2014 |

Modeling and Verification of Parallel Processes: 4th Summer School ..., Volume 4 Franck Cassez No preview available - 2001 |

### Common terms and phrases

abstraction ambient calculus analysis automata automaton behaviour bisimilarity bisimulation bMSCs Büchi Büchi automaton calculus CFFD semantics CFFD-equivalence checker client clock communication components concurrent constraints construction defined Deﬁnition deterministic distributed editors Embedded System equivalence execution fault model finite formal methods formal verification formula function HMSC languages I/O FSM IEEE IFIP implementation initial interface Lecture Notes lemma linear linear temporal logic locations LTSs Luca Cardelli machines Message Sequence Charts Mobile Processes model checking monoid MOVEP nodes Notes in Computer operation parallel composition Petrenko Petri net Petri nets pi-Calculus problem Proc process calculi ProFiBus programs proof properties rational subsets reachable reduced relation Robin Milner server simulation specification Springer LNCS Springer-Verlag symbolic synchronous techniques temporal logic test suite theorem proving theory token tool transition relation transition systems undecidable Uppaal variables verification visible actions