Handbook of Truly Concurrent Process Algebra

Front Cover
Handbook of Truly Concurrent Process Algebra
Copyright
Contents
1 Introduction to algebraic theory for reversible computing
2 Backgrounds
	2.1 Operational semantics
	2.2 Proof techniques
	2.3 CTC
	2.4 πtc
	2.5 APTC
		2.5.1 Basic algebra for true concurrency
		2.5.2 Algebra for parallelism in true concurrency
		2.5.3 Recursion
		2.5.4 Abstraction
		2.5.5 Axiomatization for hhp-bisimilarity
		2.5.6 Placeholder
	2.6 Forward–reverse truly concurrent bisimulations
3 Reversible calculus
	3.1 Syntax and operational semantics
		3.1.1 Syntax
		3.1.2 Operational semantics
		3.1.3 Properties of transitions
	3.2 Strongly forward–reverse truly concurrent bisimulations
	3.3 Weakly forward–reverse truly concurrent bisimulations
4 Algebraic laws for reversible computing
	4.1 Basic reversible algebra for true concurrency
		4.1.1 Axiom system of BRATC
		4.1.2 Properties of BRATC
		4.1.3 Structured operational semantics of BRATC
	4.2 Reversible algebra for parallelism in true concurrency
		4.2.1 Parallelism
		4.2.2 Axiom system of parallelism
		4.2.3 Structured operational semantics of parallelism
		4.2.4 Encapsulation
		4.2.5 Recursion
	4.3 Abstraction
		4.3.1 Algebraic laws for the silent step
		4.3.2 Abstraction
5 Partially reversible calculus
	5.1 Syntax and operational semantics
		5.1.1 Syntax
		5.1.2 Operational semantics
		5.1.3 Properties of transitions
	5.2 Strongly forward–reverse truly concurrent bisimulations
		5.2.1 Laws and congruence
		5.2.2 Recursion
	5.3 Weakly forward–reverse truly concurrent bisimulations
		5.3.1 Laws
		5.3.2 Recursion
6 Algebraic laws for partially reversible computing
	6.1 Basic algebra for reversible true concurrency
		6.1.1 Axiom system of BARTC
		6.1.2 Properties of BARTC
		6.1.3 Structured operational semantics of BARTC
	6.2 Algebra for parallelism in reversible true concurrency
		6.2.1 Parallelism
		6.2.2 Axiom system of parallelism
		6.2.3 Structured operational semantics of parallelism
		6.2.4 Encapsulation
	6.3 Recursion
		6.3.1 Recursive definition and specification principles
	6.4 Abstraction
		6.4.1 Algebraic laws for the silent step
		6.4.2 Abstraction
7 Partially reversible πtc
	7.1 Operational semantics
	7.2 Syntax and operational semantics
		7.2.1 Syntax
		7.2.2 Operational semantics
		7.2.3 Properties of transitions
	7.3 Strong bisimilarities
		7.3.1 Laws and congruence
		7.3.2 Recursion
	7.4 Algebraic theory
8 Introduction to probabilistic process algebra for true concurrency
9 Backgrounds
	9.1 Guards
		9.1.1 Operational semantics
		9.1.2 BATC with guards
		9.1.3 APTC with guards
		9.1.4 Recursion
		9.1.5 Abstraction
	9.2 Probabilistic operational semantics for true concurrency
10 A calculus for probabilistic true concurrency
	10.1 Syntax and operational semantics
		10.1.1 Syntax
		10.1.2 Operational semantics
		10.1.3 Properties of transitions
	10.2 Strongly probabilistic truly concurrent bisimulations
		10.2.1 Laws and congruence
		10.2.2 Recursion
	10.3 Weakly probabilistic truly concurrent bisimulations
		10.3.1 Laws and congruence
		10.3.2 Recursion
11 Algebraic laws for probabilistic true concurrency
	11.1 Basic algebra for probabilistic true concurrency
		11.1.1 Axiom system of BAPTC
		11.1.2 Properties of BAPTC
		11.1.3 Structured operational semantics of BAPTC
	11.2 Algebra for parallelism in probabilistic true concurrency
		11.2.1 Axiom system of parallelism
		11.2.2 Structured operational semantics of parallelism
		11.2.3 Encapsulation
	11.3 Recursion
		11.3.1 Guarded recursive specifications
		11.3.2 Recursive definition and specification principles
		11.3.3 Approximation induction principle
	11.4 Abstraction
		11.4.1 Guarded linear recursion
		11.4.2 Algebraic laws for the silent step
		11.4.3 Abstraction
12 Mobility
	12.1 Syntax and operational semantics
		12.1.1 Syntax
		12.1.2 Operational semantics
		12.1.3 Properties of transitions
	12.2 Strongly probabilistic truly concurrent bisimilarities
		12.2.1 Basic definitions
		12.2.2 Laws and congruence
		12.2.3 Recursion
	12.3 Algebraic theory
13 Guards
	13.1 Operational semantics
	13.2 BAPTC with guards
	13.3 APPTC with guards
	13.4 Recursion
	13.5 Abstraction
	13.6 Hoare logic for APPTCG
14 CTC with probability and guards
	14.1 Operational semantics
	14.2 Syntax and operational semantics
		14.2.1 Syntax
		14.2.2 Operational semantics
		14.2.3 Properties of transitions
	14.3 Strong bisimulations
		14.3.1 Laws and congruence
		14.3.2 Recursion
	14.4 Weak bisimulations
		14.4.1 Laws and congruence
		14.4.2 Recursion
15 πtc with probability and guards
	15.1 Operational semantics
	15.2 Syntax and operational semantics
		15.2.1 Syntax
		15.2.2 Operational semantics
		15.2.3 Properties of transitions
	15.3 Strong bisimilarities
		15.3.1 Laws and congruence
		15.3.2 Recursion
	15.4 Algebraic theory
16 Introduction to actors
17 Truly concurrent process algebra
	17.1 Process creation
	17.2 Asynchronous communication
	17.3 Applications
18 Process algebra based actor model
	18.1 Modeling characteristics of an actor
	18.2 Combining all the elements into a whole
19 Process algebra based actor model of Map–Reduce
	19.1 Requirements of Map–Reduce
	19.2 The new actor model of Map–Reduce
		19.2.1 Map actor, MapA
		19.2.2 Reduce actor, RA
		19.2.3 Master actor, Mas
		19.2.4 Putting all actors together into a whole
20 Process algebra based actor model of the Google File System
	20.1 Requirements of the Google File System
	20.2 The new actor model of the Google File System
		20.2.1 Client actor, CA
		20.2.2 Chunk Server actor, CSA
		20.2.3 Master actor, Mas
		20.2.4 Putting all actors together into a whole
21 Process algebra based actor model of cloud resource management
	21.1 Requirements of cloud resource management
	21.2 The new actor model of cloud resource management
		21.2.1 Client actor, CA
		21.2.2 Virtual Resource actor, VA
		21.2.3 Resource Manager actor, RA
		21.2.4 State Collector actor, SA
		21.2.5 Putting all actors together into a whole
22 Process algebra based actor model of the Web Service composition
	22.1 Requirements of the Web Service composition
		22.1.1 WSO and WSC
		22.1.2 Design decisions on Web Service composition runtime
		22.1.3 A WS composition runtime architecture
	22.2 The new actor model of Web Service composition
		22.2.1 Activity actor, AA
		22.2.2 Web Service orchestration, WSO
		22.2.3 Web Service, WS
		22.2.4 Web Service choreography, WSC
		22.2.5 Putting all actors together into a whole
	22.3 An example
		22.3.1 User Agent AAs
		22.3.2 UserAgent WSO
		22.3.3 UserAgent WS
		22.3.4 BookStore AAs
		22.3.5 BookStore WSO
		22.3.6 BookStore WS
		22.3.7 BuyingBooks WSC
		22.3.8 Putting all actors together into a whole
23 Process algebra based actor model of the QoS-aware Web Service orchestration engine
	23.1 Requirements of the QoS-aware Web Service orchestration engine
		23.1.1 The BookStore WSO
		23.1.2 Architecture of a typical QoS-aware WSO engine, QoS-WSOE
	23.2 The new actor model of the QoS-aware Web Service orchestration engine
		23.2.1 Web Service, WS
		23.2.2 Web Service orchestration instance manager, WSOIM
		23.2.3 Web Service orchestration (instance), WSO
		23.2.4 Activity actor, AA
		23.2.5 Service selector, SS
		23.2.6 Putting all actors together into a whole
	23.3 An example
		23.3.1 BookStore AAs
		23.3.2 WSOIM
		23.3.3 BookStore WSO
		23.3.4 BuyerAgent WS
		23.3.5 BookStore WS
		23.3.6 Railway WS
		23.3.7 Airline WS
		23.3.8 Service selector
		23.3.9 Putting all actors together into a whole
24 Introduction to secure process algebra
25 Secure APTC
	25.1 Symmetric encryption
	25.2 Asymmetric encryption
	25.3 Hash
	25.4 Digital signatures
	25.5 Message authentication codes
	25.6 Random sequence generation
	25.7 Blind signatures
	25.8 XOR
	25.9 Extended communications
	25.10 Analyses of security protocols
		25.10.1 A protocol using private channels
		25.10.2 Secure communication protocols using symmetric keys
		25.10.3 Discussion
26 Analyses of key exchange protocols
	26.1 Key exchange with symmetric cryptography
	26.2 Key exchange with public key cryptography
	26.3 Interlock protocol
	26.4 Key exchange with digital signatures
	26.5 Key and message transmission
	26.6 Key and message broadcast
27 Analyses of authentication protocols
	27.1 Mutual authentication using the interlock protocol
	27.2 SKID
28 Analyses of practical protocols
	28.1 Wide-Mouth Frog protocol
	28.2 Yahalom protocol
	28.3 Needham–Schroeder protocol
	28.4 Otway–Rees protocol
	28.5 Kerberos protocol
	28.6 Neuman–Stubblebine protocol
	28.7 Denning–Sacco protocol
	28.8 DASS protocol
	28.9 Woo–Lam protocol
29 Analyses of other protocols
	29.1 Analyses of secret splitting protocols
	29.2 Analyses of bit commitment protocols
		29.2.1 Bit commitment protocol 1
		29.2.2 Bit commitment protocol 2
	29.3 Analyses of anonymous key distribution protocols
30 Analyses of digital cash protocols
	30.1 Digital cash protocol 1
	30.2 Digital cash protocol 2
	30.3 Digital cash protocol 3
	30.4 Digital cash protocol 4
31 Analyses of secure elections protocols
	31.1 Secure elections protocol 1
	31.2 Secure elections protocol 2
	31.3 Secure elections protocol 3
	31.4 Secure elections protocol 4
	31.5 Secure elections protocol 5
	31.6 Secure elections protocol 6
32 Introduction to verification of patterns
33 Verification of architectural patterns
	33.1 From mud to structure
		33.1.1 Verification of the Layers pattern
		33.1.2 Verification of the Pipes and Filters pattern
		33.1.3 Verification of the Blackboard pattern
	33.2 Distributed systems
		33.2.1 Verification of the Broker pattern
	33.3 Interactive systems
		33.3.1 Verification of the MVC pattern
		33.3.2 Verification of the PAC pattern
	33.4 Adaptable systems
		33.4.1 Verification of the Microkernel pattern
		33.4.2 Verification of the Reflection pattern
34 Verification of design patterns
	34.1 Structural decomposition
		34.1.1 Verification the Whole-Part pattern
	34.2 Organization of work
		34.2.1 Verification of the Master–Slave pattern
	34.3 Access control
		34.3.1 Verification of the Proxy pattern
	34.4 Management
		34.4.1 Verification of the Command Processor pattern
		34.4.2 Verification of the View Handler pattern
	34.5 Communication
		34.5.1 Verification of the Forwarder–Receiver pattern
		34.5.2 Verification of the Client–Dispatcher–Server pattern
		34.5.3 Verification of the Publisher–Subscriber pattern
35 Verification of idioms
	35.1 Verification of the Singleton pattern
	35.2 Verification of the Counted Pointer pattern
36 Verification of patterns for concurrent and networked objects
	36.1 Service access and configuration patterns
		36.1.1 Verification of the Wrapper Facade pattern
		36.1.2 Verification of the Component Configurator pattern
		36.1.3 Verification of the Interceptor pattern
		36.1.4 Verification of the Extension Interface pattern
	36.2 Event handling patterns
		36.2.1 Verification of the Reactor pattern
		36.2.2 Verification of the Proactor pattern
		36.2.3 Verification of the Asynchronous Completion Token pattern
		36.2.4 Verification of the Acceptor–Connector pattern
	36.3 Synchronization patterns
		36.3.1 Verification of the Scoped Locking pattern
		36.3.2 Verification of the Strategized Locking pattern
		36.3.3 Verification of the Double-Checked Locking Optimization pattern
	36.4 Concurrency patterns
		36.4.1 Verification of the Active Object pattern
		36.4.2 Verification of the Monitor Object pattern
		36.4.3 Verification of the Half-Sync/Half-Async pattern
		36.4.4 Verification of the Leader/Followers pattern
		36.4.5 Verification of the Thread-Specific Storage pattern
37 Verification of patterns for resource management
	37.1 Resource acquisition
		37.1.1 Verification of the Lookup pattern
		37.1.2 Verification of the Lazy Acquisition pattern
		37.1.3 Verification of the Eager Acquisition pattern
		37.1.4 Verification of the Partial Acquisition pattern
	37.2 Resource Life cycle
		37.2.1 Verification of the Caching pattern
		37.2.2 Verification of the Pooling pattern
		37.2.3 Verification of the Coordinator pattern
		37.2.4 Verification of the Resource Life cycle Manager pattern
	37.3 Resource release
		37.3.1 Verification of the Leasing pattern
		37.3.2 Verification of the Evictor pattern
38 Composition of patterns
	38.1 Composition of the Layers patterns
	38.2 Composition of the PAC patterns
	38.3 Composition of resource management patterns
References
Index
Back Cover