Название: Handbook of Truly Concurrent Process Algebra
Автор: Yong Wang
Издательство: Morgan Kaufmann/Elsevier
Год: 2024
Страниц: 648
Язык: английский
Формат: pdf (true)
Размер: 15.0 MB

Handbook of Truly Concurrent Process Algebra provides readers with a detailed and in-depth explanation of the algebra used for concurrent computing. This complete handbook is divided into five Parts: Algebraic Theory for Reversible Computing, Probabilistic Process Algebra for True Concurrency, Actors – A Process Algebra-Based Approach, Secure Process Algebra, and Verification of Patterns.

The author demonstrates actor models which are captured using the following characteristics: Concurrency, Asynchrony, Uniqueness, Concentration, Communication Dependency, Abstraction, and Persistence. Every pattern is detailed according to a regular format to be understood and utilized easily, which includes introduction to a pattern and its verifications.

Patterns of the vertical domains are also provided, including the domains of networked objects and resource management. To help readers develop and implement the software patterns scientifically, the pattern languages are also presented.

Reversible computing is an interesting topic in Computer Science. Reversible computing has been used in many area, such as quantum computing, transactions in databases, and business transactions. In these application areas, there are two aspects of reversible computing: one is that there is a corresponding reverse atomic action for each atomic action, so it is reversible at the level of atomic action; the other is in program logic, for the forward logic is important and the reverse logic is important too. The relation between the forward logic and reverse logic is the main content of reversible computing.

In the following, we take an example of business transactions. Traditional transactions with ACID (Atomicity, Consistency, Isolation and Durability) properties are supported by most of the current database management systems. They are usually implemented by middle states and a commit–rollback mechanism before being permanently stored or aborted. LLT (Long Living Transaction) or LRBT (Long Running Business Transaction) is a transaction surviving a long period of time. Compared to LLTs, LRBTs must satisfy the heterogeneity of applications located in different organizations, not only a long period of running time. More importantly, they are usually interactive, that is, LRBTs and their inner contained business activities or nested LRBTs are interacting with applications or humans. A LRBT may contain nested LRBTs or atomic business activities and finally be consisted of business activities. A business activity is usually located in one organization domain and survives for a shorter period of time. Hence, business activities are like traditional transactions and can be processed by use of traditional transaction process mechanisms. However, the abortion or failure of a LRBT cannot be settled by middle states to be rollbacked or permanently stored finally like traditional transaction processing, and the failure or abortion processing of a LRBT must adopt a special kind of mechanism, unlike rollback. Every step of a LRBT produces permanent effects without middle states to rollback, so a compensation operation corresponding to this step seems to be the only choice to cancel this step’s effects when the LRBT fails or is aborted. Corresponding to a LLT, with the running of a LRBT, every business activity with ACID attributes is finished, so when a LRBT is aborted or fails, a compensation activity according to each finished business activity must be executed to eliminate the permanent effect produced by the business activity.

The functions of compensation mechanisms in LRBTs have already been accepted by the industry. Since Web Service is one kind of solution to solve cross-organizational application integrations, a compensation mechanism was adopted in Web Service orchestration specifications, such as the early WSFL (Web Service Flow Language) and XLANG. The late OASIS’s WS-BPEL (Web Services Business Process Execution Language) also adopts compensation as the mechanism to abort a LRBT defined in a composite Web Service.

Key Features:
• Presents all aspects of full algebraic reversible computing, including the basis of semantics, calculi for full reversible computing, and axiomatization for full reversible computing
• Introduces algebraic properties and laws for probabilistic computing, one of the foundational concepts of Computer Science
• Presents the calculi for probabilistic computing, including the basis of semantics and calculi for reversible computing