Reactive Systems
Modelling, Specification and Verification
- Authors:
- Luca Aceto, Reykjavik University
- Anna Ingólfsdóttir, Reykjavik University
- Kim Guldstrand Larsen, Aalborg University, Denmark
- Jiri Srba, Aalborg University, Denmark
- Date Published: August 2007
- availability: Available
- format: Hardback
- isbn: 9780521875462
Hardback
Other available formats:
eBook
Looking for an inspection copy?
This title is not currently available for inspection. However, if you are interested in the title for your course we can consider offering an inspection copy. To register your interest please contact asiamktg@cambridge.org providing details of the course you are teaching.
-
Formal methods is the term used to describe the specification and verification of software and software systems using mathematical logic. Various methodologies have been developed and incorporated into software tools. An important subclass is distributed systems. There are many books that look at particular methodologies for such systems, e.g. CSP, process algebra. This book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. Milner's CCS and its operational semantics are introduced, together with notions of behavioural equivalence based on bisimulation techniques and with variants of Hennessy-Milner modal logics. Later in the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout.
Read more- Broad accessible introduction to the topic - the first book to cover all the different approaches
- Based on taught courses, and containing case studies and many exercises, this book is ideal as a graduate text
- Offers first presentation in book form of Hennessy-Milner logic with recursive definitions and its applications
Customer reviews
02nd Jan 2014 by Aziz
Firstly i am very satisfied with this book. but when it comes to the page 205 ,second line from down i cant sure whether is it mistake or not but there is little problem related to term cx ,.cx have to be 1 for the timed automaton on the left in Example 11.4. thanks.
Review was not posted due to profanity
×Product details
- Date Published: August 2007
- format: Hardback
- isbn: 9780521875462
- length: 302 pages
- dimensions: 246 x 182 x 20 mm
- weight: 0.68kg
- contains: 28 b/w illus. 7 tables 188 exercises
- availability: Available
Table of Contents
Preface
Part I. A Classic Theory of Reactive Systems:
1. Introduction
2. The language CCS
3. Behavioural equivalences
4. Theory of fixed points and bisimulation equivalence
5. Hennessy-Milner logic
6. Hennessy-Milner logic with recursive definitions
7. Modelling and analysis of mutual exclusion algorithms
Part II. A Theory of Real-Time Systems:
8. Introduction
9. CCS with time delays
10. Timed automata
11. Timed behavioural equivalences
12. Hennessy-Milner logic with time
13. Modelling and analysis of Fischer's algorithm
Appendix
Bibliography
Index.-
Resources for
Reactive Systems
Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba
General Resources
Find resources associated with this title
Type Name Unlocked * Format Size Showing of
This title is supported by one or more locked resources. Access to locked resources is granted exclusively by Cambridge University Press to lecturers whose faculty status has been verified. To gain access to locked resources, lecturers should sign in to or register for a Cambridge user account.
Please use locked resources responsibly and exercise your professional discretion when choosing how you share these materials with your students. Other lecturers may wish to use locked resources for assessment purposes and their usefulness is undermined when the source files (for example, solution manuals or test banks) are shared online or via social networks.
Supplementary resources are subject to copyright. Lecturers are permitted to view, print or download these resources for use in their teaching, but may not change them or use them for commercial gain.
If you are having problems accessing these resources please contact lecturers@cambridge.org.
Sorry, this resource is locked
Please register or sign in to request access. If you are having problems accessing these resources please email lecturers@cambridge.org
Register Sign in» Proceed