Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures, Volume 4
Springer Science & Business Media, Oct 24, 2001 - Computers - 222 pages
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.
What people are saying - Write a review
We haven't found any reviews in the usual places.
A Tutorial Overview
Theorem Proving for Verification
Composition and Abstraction
UPPAAL Now Next and Future
HMSCs as Partial Specifications with PNs as Completions
Industrial Applications of Model Checking
The Missing Links A Perspective from the Security Area
Verification of Systems with an Infinite State Space
An Annotated Bibliography
A Commented Bibliography
Other editions - View all
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