Reactive Systems
Námskeið
- T-707-MOVE Modeling and Verification
Lýsing:
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.
Annað
- Höfundar: Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba
- Útgáfa:1
- Útgáfudagur: 09-08-2007
- Hægt að prenta út 5 bls.
- Hægt að afrita 5 bls.
- Format:Page Fidelity
- ISBN 13: 9780511332142
- Print ISBN: 9780521875462
- ISBN 10: 0511332149
Efnisyfirlit
- Half-title
- Title
- Copyright
- Contents
- Figures and tables
- Figures
- Tables
- Preface
- Part I A Classic Theory of Reactive Systems
- 1 Introduction
- Aims of this book
- 1.1 What are reactive systems?
- 1.2 Process algebras
- 2 The language CCS
- 2.1 Some CCS process constructions
- 2.1.1 The behaviour of processes
- 2.2 CCS, formally
- 2.2.1 The model of labelled transition systems
- 2.2.2 The formal syntax and semantics of CCS
- 2.2.3 Value-passing CCS
- 2.1 Some CCS process constructions
- 1 Introduction
- 3 Behavioural equivalences
- 3.1 Criteria for good behavioural equivalence
- 3.2 Trace equivalence: a first attempt
- 3.3 Strong bisimilarity
- 3.4 Weak bisimilarity
- 3.5 Game characterization of bisimilarity
- 3.5.1 Weak bisimulation games
- 3.6 Further results on equivalence checking
- 4 Theory of fixed points and bisimulation equivalence
- 4.1 Posets and complete lattices
- 4.2 Tarski?s fixed point theorem
- 4.3 Bisimulation as a fixed point
- 5 Hennessy?Milner logic
- 5.1 Introduction to Hennessy?Milner logic
- 5.2 Hennessy?Milner theorem
- 6 Hennessy?Milner logic with recursive definitions
- Introduction
- 6.1 Examples of recursive properties
- 6.2 Syntax and semantics of HML with recursion
- 6.3 Largest fixed points and invariant properties
- 6.4 A game characterization for HML with recursion
- 6.4.1 Examples of use
- 6.5 Mutually recursive equational systems
- 6.6 Characteristic properties
- 6.7 Mixing largest and least fixed points
- 6.8 Further results on model checking
- 7 Modelling and analysis of mutual exclusion algorithms
- Introduction
- 7.1 Specifying mutual exclusion in HML
- 7.2 Specifying mutual exclusion using CCS itself
- 7.3 Testing mutual exclusion
- 8 Introduction
- 8.1 Real-time reactive systems
- 9 CCS with time delays
- 9.1 Intuition
- 9.2 Timed labelled transition systems
- 9.3 Syntax and SOS rules of timed CCS
- 9.4 Parallel composition
- 9.5 Other timed process algebras and discussion
- 10 Timed automata
- 10.1 Motivation
- 10.2 Syntax of timed automata
- 10.3 Semantics of timed automata
- 10.4 Networks of timed automata
- 10.5 More on timed-automata formalisms
- 11 Timed behavioural equivalences
- 11.1 Timed and untimed trace equivalence
- 11.2 Timed and untimed bisimilarity
- 11.3 Weak timed bisimilarity
- 11.4 Region graphs
- 11.5 Zones and reachability graphs
- 11.6 Further results on timed equivalences
- 12 Hennessy?Milner logic with time
- Introduction
- 12.1 Basic logic
- 12.2 Hennessy?Milner logic with time and regions
- 12.3 Timed bisimilarity versus HML with time
- 12.4 Recursion in HML with time
- 12.4.1 Characteristic properties for timed bisimilarity
- 12.4.2 Examples of real-time temporal properties
- 12.5 More on timed logics
- 13 Modelling and analysis of Fischer?s algorithm
- Introduction
- 13.1 Mutual exclusion using timing
- 13.2 Modelling Fischer?s algorithm
- 13.2.1 Proving mutual exclusion using UPPAAL
- 13.2.2 An erroneous version of Fischer?s algorithm
- 13.3 Further exercises on timing-based mutual exclusion algorithms
- A.1 Alternating-bit protocol
- A.2 Gossiping girls
- A.3 Implementation of regions
UM RAFBÆKUR Á HEIMKAUP.IS
Bókahillan þín er þitt svæði og þar eru bækurnar þínar geymdar. Þú kemst í bókahilluna þína hvar og hvenær sem er í tölvu eða snjalltæki. Einfalt og þægilegt!Rafbók til eignar
Rafbók til eignar þarf að hlaða niður á þau tæki sem þú vilt nota innan eins árs frá því bókin er keypt.
Þú kemst í bækurnar hvar sem er
Þú getur nálgast allar raf(skóla)bækurnar þínar á einu augabragði, hvar og hvenær sem er í bókahillunni þinni. Engin taska, enginn kyndill og ekkert vesen (hvað þá yfirvigt).
Auðvelt að fletta og leita
Þú getur flakkað milli síðna og kafla eins og þér hentar best og farið beint í ákveðna kafla úr efnisyfirlitinu. Í leitinni finnur þú orð, kafla eða síður í einum smelli.
Glósur og yfirstrikanir
Þú getur auðkennt textabrot með mismunandi litum og skrifað glósur að vild í rafbókina. Þú getur jafnvel séð glósur og yfirstrikanir hjá bekkjarsystkinum og kennara ef þeir leyfa það. Allt á einum stað.
Hvað viltu sjá? / Þú ræður hvernig síðan lítur út
Þú lagar síðuna að þínum þörfum. Stækkaðu eða minnkaðu myndir og texta með multi-level zoom til að sjá síðuna eins og þér hentar best í þínu námi.
Fleiri góðir kostir
- Þú getur prentað síður úr bókinni (innan þeirra marka sem útgefandinn setur)
- Möguleiki á tengingu við annað stafrænt og gagnvirkt efni, svo sem myndbönd eða spurningar úr efninu
- Auðvelt að afrita og líma efni/texta fyrir t.d. heimaverkefni eða ritgerðir
- Styður tækni sem hjálpar nemendum með sjón- eða heyrnarskerðingu
- Gerð : 208
- Höfundur : 6173
- Útgáfuár : 2007
- Leyfi : 379