The Evolution of Concurrent Programs

Process algebra are formal languages used for the rigorous specification and analysis of concurrent systems. By using a process algebra as the target language of a genetic programming system, the derivation of concurrent programs satisfying given problem specifications is possible. A genetic programming system based on Koza's model has been implemented. The target language used is Milner's CCS process algebra, and is chosen for its conciseness and simplicity. The genetic programming environment needs a few adaptations to the computational characteristics of concurrent programs. In particular, means for efficiently controlling the exponentially large computation spaces that are common with process algebra must be addressed. Experimental runs of the system successfully evolved a number of non–iterative CCS systems, hence proving the potential of evolutionary approaches to concurrent system development.     

基于LTS的Statecharts操作语义研究

Statecharts是一种用于复杂反应式系统行为的可视化规格语言。该文提出了一种基于标签变迁系统(LTS)的Statecharts操作语义描述方法，介绍了Statecharts及其项语法和一步语义，并基于进程代数描述Statecharts的并发行为，使用结构化的操作语义SOS规则描述Statecharts的组合语义，从而得到相应的LTS。     

Formal modelling and verification of GALS systems using GRL and CADP

A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronous components that evolve concurrently and interact with each other asynchronously. The design of GALS systems is tedious and error-prone due to the high degree of synchronous and asynchronous concurrency present in complex architectures. In this paper, we present GRL (GALS Representation Language), a formal language designed to model GALS systems, for the purpose of formal verification of the asynchronous aspects. GRL combines the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. We propose a translation from GRL to LNT, a value-passing concurrent language with classical process algebra flavour. This makes possible the analysis of GRL specifications using all the state-of-the-art simulation and verification functionalities provided by the CADP toolbox.     

An algebraic model for programming languages

The language of universal algebras is used as a model for programming language specification. BNF rules are employed for specifying the signature of the language algebra instead of the context free syntax. The algorithm for program evaluation is inductively defined by the following universal algebraic construction:

Any function defined on the generators of a free algebra taking values in the carrier of another similar algebra can be uniquely extended to a homomorphism between the two algebras.

Any conventional programming language can be specified by a finite set of BNF rules and its algebra of symbols is generated by a finite set of generator classes. Thus any function defined on the finite set of generators offers an algebraic mechanism for a universal algorithm for source language program evaluation.     

PVS Embedding of cCSP Semantic Models and Their Relationship

This paper demonstrates an embedding of the semantic models of the cCSP process algebra in the general purpose theorem prover PVS. cCSP is a language designed to model long-running business transactions with constructs for orchestration of compensations. The cCSP process algebra terms are defined in PVS by using mutually recursive datatype. The trace and the operational semantics of the algebra are embedded in PVS. We show how these semantic embeddings are used to define and prove a relationship between the semantic models by using the powerful induction mechanism of PVS.     

一个支持软件并行工程的过程建模语言

实施软件并行工程是缩短软件开发周期、加快软件开发速度的有效途径。文中讨论了软件并行工程对过程建模语言的要求,给出了一个支持软件并行工程的形式化过程建模语言ＳＤＤＭＬ和基于ＳＤＤＭＬ的过程建模方法。ＳＤＤＭＬ基于Ｐｅｔｒｉ网,具有面向对象的特征,可表示不同抽象级的过程模型,支持逐步求精的过程建模方法,为软件并行工程软件过程的控制、分析、评估和优化奠定了基础。     

An integrated framework for the performance analysis of asynchronous communicating stochastic processes

In this paper we present a design framework containing a process algebra and the concurrent functional programming language Eden. In order to study properties of a specification written in our process algebraic notation, we provide a translation mechanism to generate Eden programs. Once we have a translation, we may use the Eden tools to study the performance of the (simulation of the) system. In order to add expressiveness to our design language we use a very powerful process algebra. First, we allow the specification of delays induced by general random variables. We also consider value passing. Finally, the communication between concurrent processes is asynchronous. The usefulness of our framework is presented by two examples featuring all the characteristics of our process algebraic model, we give the corresponding translations, and we provide some performance measures obtained by using Eden tools.Research supported in part by the Ministerio de Ciencia y Tecnologí a projects MASTER (TIC2003-07848-C02-01) and AMEVA (TIC2000-0701-C02-01) and by the Junta de Comunidades de Castilla-La Mancha project PAC-03-001.Accepted in revised form 15 September 2003 by M. Broy, G. Lüttgen and M. Mendler     

A complete temporal relational algebra

Various temporal extensions to the relational model have been proposed. All of these, however, deviate significantly from the original relational model. This paper presents a temporal extension of the relational algebra that is not significantly different from the original relational model, yet is at least as expressive as any of the previous approaches. This algebra employs multidimensional tuple time-stamping to capture the complete temporal behavior of data. The basic relational operations are redefined as consistent extensions of the existing operations in a manner that preserves the basic algebraic equivalences of the snapshot (i.e., conventional static) algebra. A new operation, namely temporal projection, is introduced. The complete update semantics are formally specified and aggregate functions are defined. The algebra is closed, and reduces to the snapshot algebra. It is also shown to be at least as expressive as the calculus-based temporal query language TQuel. In order to assess the algebra, it is evaluated using a set of twenty-six criteria proposed in the literature, and compared to existing temporal relational algebras. The proposed algebra appears to satisfy more criteria than any other existing algebra. Edited by Wesley Chu. Received February 1993 / Accepted April 1995     

Formal specification of concurrent systems

This paper presents a formal methodology for developing concurrent systems. We extend the Larch family of specification languages and tools with the CCS process algebra to support the specification and verification of concurrent systems. We present and follow a refinement strategy that relates an implementation in a programming language to a formal specification of such a system. We illustrate our methodology on an example that uses the preconditioned conjugate gradient method for solving a linear system of equations.     

同步合成Petri网系统活性与无死锁性的保持性

合成操作是Petri网系统建模中一种重要的自底向上建模方法,而在Petri网系统的合成研究中,一些好性质,如活性、无死锁性、可回复性等的保持性,是一个重要的研究问题.研究了Petri网系统同步合成操作活性与无死锁性的保持性.与以往研究工作不同,基于路径的并发合成用并发语言的方法,提出并证明了同步合成Petri网系统的一个并发语言关系式.该语言关系式可用于判定同步合成Petri网系统的活性与无死锁性,同时给出了同步合成Petri网系统活性与无死锁性的充要条件.最后提出一些条件,在这些条件下,同步合成Petri网系统有活与无死锁的保持性质.     

Using binary decision diagrams for representation and analysis of communication protocols

A symbolic representation of a state/transition system based on binary decision diagrams (BDDs) is generally more compact than an explicit representation like a state/transition table. This is due to regular and repetitive patterns occurring in state/transition systems. By exploiting this property, huge state spaces can be represented, and the resulting BDDs can be profitably used for activities such as symbolic model checking and sequential circuit synthesis. This paper shows how such techniques can be applied to communication protocols by presenting a systematic method to build BDD representations from protocol specifications expressed in the ISO standard protocol specification language LOTOS. The method exploits the compositionality of the process algebra of LOTOS to avoid the enumeration of all the states and transitions, takes also data into account, enables building the BDDs in the more convenient disjunctive partitioned form, and can handle any LOTOS specification characterized by a finite LTS. The method consists in partitioning the set of process definitions according to their mutual recursion relationships, building an LTS for each set of mutually recursive process definitions, encoding these LTSs as BDDs which in turn are combined together, according to the process algebraic operators, to obtain the overall BDD representation. An example is used throughout the paper to illustrate the method.     

Relating state-based and process-based concurrency through linear logic (full-version)

This paper has the purpose of reviewing some of the established relationships between logic and concurrency, and of exploring new ones.Concurrent and distributed systems are notoriously hard to get right. Therefore, following an approach that has proved highly beneficial for sequential programs, much effort has been invested in tracing the foundations of concurrency in logic. The starting points of such investigations have been various idealized languages of concurrent and distributed programming, in particular the well established state-transformation model inspired by Petri nets and multiset rewriting, and the prolific process-based models such as the π-calculus and other process algebras. In nearly all cases, the target of these investigations has been linear logic, a formal language that supports a view of formulas as consumable resources. In the first part of this paper, we review some of these interpretations of concurrent languages into linear logic and observe that, possibly modulo duality, they invariably target a small semantic fragment of linear logic that we call LV^obs.In the second part of the paper, we propose a new approach to understanding concurrent and distributed programming as a manifestation of logic, which yields a language that merges those two main paradigms of concurrency. Specifically, we present a new semantics for multiset rewriting founded on an alternative view of linear logic and specifically LV^obs. The resulting interpretation is extended with a majority of linear connectives into the language of ω-multisets. This interpretation drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication, and more. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. For example, a simple translation maps process constructors of the asynchronous π-calculus to rewrite operators. The language of ω-multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature, with the potential of combining verification techniques from both worlds. Additionally, its logical underpinning makes it an ideal common ground for systematically comparing protocol specification languages.     

安全协议的进程代数规约到逻辑程序的自动转换

安全协议用于实现开放互连网络的安全通讯，它本质上是分布式并发程序，使用进程代数可以将其描述为角色进程的并发合成系统。使用抽象方法，安全协议角色进程并发合成模型可以转化为逻辑程序；通过计算逻辑程序的不动点，能够对安全协议无穷会话的并发交叠运行进行验证。本文基于Objective Caml语言，实现了安全协议进程代数描述述到安全协议逻辑程序的自动转化。     

On the Specification of Higher Dimensional Automata

Higher dimensional automata (HDA) have been widely studied as models of concurrent processes. Most current work focuses on developing the directed algebraic topological notions required to analyse HDA to determine their computer scientific properties (deadlock, safety, unreachable states, etc). Instead, this paper is concerned with the software engineering of HDA and details the specification of HDA by process algebra operations. The specifications work for cubical HDA, but are designed to also work for the explicit choice higher dimensional automata (ECHDA) originally proposed by Buckland. We introduce ω-multigraphs, a graphical notion which is easier to use than pasting schemes but more general than cubical complexes, we describe basic process algebra operations on ECHDA as constructions on ω-multigraphs, we discuss the trichotomy of concurrent, conferring, and conflicting choices, and note that the “deadlock choice” can arise from intersecting conflicting choices, and we remark that common software engineering refinements correspond to choice refinement.     

Process algebra approach to reasoning about concurrent actions

A reasonable transition rule is proposed for synchronized actions and some equational properties ofbisimilarity and weak bisimilarity in the process algebra for reasoning about concurrent actions are presented.     

A Process Calculus with Finitary Comprehended Terms

We introduce the notion of an ACP process algebra and the notion of a meadow enriched ACP process algebra. The former notion originates from the models of the axiom system ACP. The latter notion is a simple generalization of the former notion to processes in which data are involved, the mathematical structure of data being a meadow. Moreover, for all associative operators from the signature of meadow enriched ACP process algebras that are not of an auxiliary nature, we introduce variable-binding operators as generalizations. These variable-binding operators, which give rise to comprehended terms, have the property that they can always be eliminated. Thus, we obtain a process calculus whose terms can be interpreted in all meadow enriched ACP process algebras. Use of the variable-binding operators can have a major impact on the size of terms.     

一种FTCSP的服务组合时间建模与分析方法

为了实现适合描述并发和组合系统的经典进程代数对服务组合时间规约的建模与分析,首先,提出了一种模糊时间通信顺序进程(FTCSP),定义了其语法和操作语义,然后提出了基于FTCSP的服务组合时间建模与分析方法,定义了有利于服务组合时间规约分析的模糊时间算子,给出了服务组合时间分析算法.最后,以地下空间环境信息实时发布系统(UEIRS)为例,验证了该方法的有效性.     

DATALOG与关系代数

本文旨在通过描述DATALOG和关系代数的概念，以及DATALOG与关系代数的区别，经过从关系代数到逻辑规则和从逻辑到关系的论述，并比较DATALOG和关系代数，说明DATALOG是一种基于逻辑的数据模型，是PROLOG语言的数据库版本，关系代数是过程化的语言，关系代数表达式与安全、非递归、带有非操作的DATALOG程序的表达能力是相同的。     

Performance analysis of concurrent systems in algebra dtsiPBC

Petri box calculus PBC is a well-known algebra of concurrent processes with a Petri net semantics. In the paper, an extension of PBC with discrete stochastic time and immediate multiactions, which is referred to as discrete time stochastic and immediate PBC (dtsiPBC), is considered. Performance analysis methods for concurrent and distributed systems with random time delays are investigated in the framework of the new stochastic process algebra. It is demonstrated that the performance evaluation is possible not only via the underlying semi-Markov chains of the dtsiPBC expressions but also with the use of the underlying discrete time Markov chains, and the latter analysis technique is more optimal.