A transformation system for concurrent processes

Program transformation techniques have been extensively studied in the framework of functional and logic languages, where they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention. In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented” to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information. Received: 24 April 1997 / 19 November 1997     

State space reduction by non-standard semantics for deadlock analysis

In recent years many techniques have been developed for automatically verifying concurrent systems and most of them are based on the representation of the concurrent system by means of a transition system. State explosion is one of the most serious problems of this approach: often the prohibitive number of states renders the verification inefficient and, in some cases, impossible.

We propose a method for reducing the state space of the transition system corresponding to a CCS process that suites deadlock analysis. The reduced transition system is generated by means of a non-standard operational semantics containing a set of rules which are, in some sense, an abstraction, preserving deadlock freeness, of the inference rules of the standard semantics. Our method does not build the standard transition system, but directly generates an abstract system with a fewer number of states, so saving memory space. We characterize a class of processes whose abstract transition system is not exponential in the number of parallel components.     

Two Case Studies of Semantics Execution in Maude: CCS and LOTOS

We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas we consider two substantial case studies. In the first one, we represent both the semantics of Milner’s CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics is already known, it cannot be directly executed in the default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by controlling the rewriting process by means of reflection. This executable specification plus the reflective control of rewriting can be used to analyze CCS processes. The same techniques are also used to implement a symbolic semantics for LOTOS in our second case study. The good properties of Maude as a metalanguage allow us to implement a whole formal tool where LOTOS specifications without restrictions in their data types (given as ACT ONE specifications) can be executed. In summary, we present Maude as an executable semantic framework by providing easy-tool-building techniques for a language given its operational semantics.Research supported by CICYT projects Desarrollo Formal de Sistemas Distribuidos (TIC97-0669-C03-01) and Desarrollo Formal de Sistemas Basados en Agentes Móviles (TIC2000-0701-C02-01).     

Methods for specifying static semantics

The formal specification of a programming language involves the specification of three types of rules: syntax, static semantics and semantics. Various methods have been proposed for specifying the static semantic rules of programming languages, but as yet no method has received general acceptance. This paper looks at several different specification techniques and attempts to isolate the basic mechanisms used by each of them and explain the pattern of development of specification techniques for static semantics.     

Temporal Semantics for Concurrent M M

Concurrent is a programming language based on the notion of concurrent, communicating objects, where each object directly executes a specification given in temporal logic, and communicates with other objects using asynchronous broadcast message-passing. Thus, Concurrent represents a combination of the direct execution of temporal specifications, together with a novel model of concurrent computation. In contrast to the notions of predicates as processes and stream parallelism seen in concurrent logic languages, Concurrent represents a more coarse-grained approach, where an object consists of a set of logical rules and communication is achieved by the evaluation of certain types of predicate. Representing concurrent systems as groups of such objects provides a powerful tool for modelling complex reactive systems. In order to reason about the behaviour of Concurrent systems, we requir a suitable semantics. Being based upon executable temporal logic, objects in isolation have an intuitive semantics. However, the addition of both operational constraints upon the object's execution and global constraints provided by the asynchronous model of concurrency and communication, complicates the overall semantics of networks of objects. It is this, more complex, semantics that we address here, where temporal semantics for varieties of Concurrent are provided.     

A theory of Orwellian specifications with NewThink

We introduce NewThink, a specification language designed specifically for real-time safety-critical systems. NewThink is a component of an overall Orwellian development method for safety-critical systems which consists of a specification language, a programming language and a set of sound decomposition rules. In this paper, we present the syntax and semantics of NewThink. We demonstrate a relationship between timed and static specifications, which potentially allows us to continue using techniques from the static case in the timed case. We also prove that our extension for real-time is conservative, which is very much in keeping with our Orwellian philosophy.     

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.     

Formalizing the specification and execution of workflows using the event calculus

The event calculus is a logic programming formalism for representing events and their effects especially in database applications. This paper proposes the event calculus as a logic-based methodology for the specification and execution of workflows. It is shown that the control flow graph of a workflow specification can be expressed as a set of logical formulas and the event calculus can be used to specify the role of a workflow manager through a set of rules for the execution dependencies of activities. The proposed framework for a workflow manager maintains a history of events to control the execution of activities. The events are instructions to the workflow manager to coordinate the execution of activities. Based on the already occurred events, the workflow manager triggers new events to schedule new activities in accordance with the control flow graph of the workflow. The net effect is an alternative approach for defining a workflow engine whose operational semantics is naturally integrated with the operational semantics of a deductive database. Within this framework it is possible to model sequential and concurrent activities with or without synchronization. It is also possible to model agent assignment and execution of concurrent workflow instances. The paper, thus, contributes a logical perspective to the task of developing formalization for the workflow management systems.     

Enabling metrology-oriented specification of geometrical variability – A categorical approach

In this paper a metrology-oriented specification schema is proposed to enrich the specification semantics with sufficient metrological information. It is designed particularly for applications where non-traditional measurement methods are applied; and it can also identify any redundancies, inconsistencies or incompletenesses of a specification. The proposed schema is based on category theoretical semantics which uses category theory as the foundation to model the semantics. A set of verification operations that derived from the measurement process was firstly formalised using the categorical semantics. Then a set of full faithful functors were constructed to map the set of verification operations to a set of specification operations. A set of simplification rules was then developed to deduce all of the necessary specification objects which are independent to each other. Then the residual specification objects provide a compact structure of the specification. Three test cases were conducted to validate the proposed schema. An industrial computed tomography (CT) measurement process for an impeller manufacturing using selective laser sintering (SLS) technique, was modelled and a set of independent specification elements was then deduced. The other two test cases for checking redundancy and incompleteness on general ISO specifications were carried out. The results show that the proposed schema works for proposing semantic enriched specification that are characterised by non-traditional measurement methods and for testing redundancy and incompleteness of specifications based on geometrical product specifications and verification (GPS) standards system.     

An interpreter for LOTOS,a specification language for distributed systems

LOTOS is an executable specification language for distributed systems currently being standardized within ISO as a tool for the formal specification of open systems interconnection protocols and services. It is based on an extended version of Milner's calculus of communicating systems (CCS) and on ACT ONE abstract data type (ADT) formalism. A brief introduction to LOTOS is given, along with a discussion of LOTOS operational semantics, and of the executability of LOTOS specifications. Further, an account of a prototype LOTOS interpreter is given, which includes an interactive system that allows the user to direct the execution of a specification (for example, for testing purposes). The interpreter was implemented in YACC/LEX, C and Prolog. The following topics are discussed: syntax and static semantics analysis; translation from LOTOS external format to internal representation; evaluation of ADT value expressions and extended CCS behaviour expressions. It is shown that the interpreter can be used in a variety of ways: to recognize whether a given sequence of interactions is allowed by the specification; to generate randomly chosen sequences of interactions; in a user-guided generation mode, etc.     

Prototyping realistic programming languages based on formal specifications

The specification of realistic programming languages is difficult and expensive. One approach to make language specification more attractive is the development of techniques and systems for the generation of language–specific software from specifications. To contribute to this approach, a tool–based framework with the following features is presented: It supports new techniques to specify more language aspects in a static fashion. This improves the efficiency of generated software. It provides powerful interfaces to generated software components. This facilitates the use of these components as parts of language–specific software. It has a rather simple formal semantics. In the framework, static semantics is defined by a very general attribution technique enabling e.g. the specification of flow graphs. The dynamic semantics is defined by evolving algebra rules, a technique that has been successfully applied to realistic programming languages. After providing the formal background of the framework, an object–oriented programming language is specified to illustrate the central specification features. In particular, it is shown how parallelism can be handled. The relationship to attribute grammar extensions is discussed using a non-trivial compiler problem. Finally, the paper describes new techniques for implementing the framework and reports on experiences made so far with the implemented system. Received: 20 November 1995 / 20 January 1997     

OCCAM-an overview

The language OCCAM has been developed on the basis of communication and concurrency. OCCAM describes the structure of a system of connected microcomputers. It can also be used to program the individual computers. In addition, OCCAM is a design formalism. Its formal semantics allows a program to be read either as a set of commands or as a predicate in an extension of the predicate calculus. The semantics provides a set of rules for transforming programs.The initial implementation of OCCAM is described. Examples are given of its use in a concurrent system and for program transformation.     

Early experience with the Visual Programmer's WorkBench

The Visual Programmer's WorkBench (VPW) addresses the rapid synthesis and customization of environments for the specification, analysis, and execution of visual programs. The goal of VPW is to enable the easy creation of environments for visual languages. The design of VPW and experience using it to generate a distributed programming environment for a concurrent visual language are described. A visual programming environment for the PetriFSA language generated with VPW is outlined. An overview is provided of the language definition model and its relation to the logical architecture of VPW. Details are given of the language specifications used in VPW, and its application in defining the PetriFSA language. A language-based environment for a specific visual language is generated in VPW from a specification of the syntactic structure, the abstract structure, the static semantics, and the dynamic semantics of the language. VPW is built around a model of distributed processing based on a shared distributed memory. This framework is used in defining the architecture of the environment and for the execution model of visual languages     

Concurrent behavior: A construct to specify the external behavior of objects in object databases

We present a linguistic construct to define concurrency control for the objects of an object database. This construct, calledconcurrent behavior, allows to define a concurrency control specification for each object type in the database; in a sense, it can be seen as a type extension. The concurrent behavior is composed by two parts: the first one, calledcommutativity specification, is a set of conditional rules, by which the programmer specifies when two methods do not conflict each other. The second part, the constraint specification, is a set of guarded regular expressions, calledconstraints, by which the programmer defines the allowed sequences of method calls. At each time during an actual execution, a subset of constraints may be active so limiting the external behavior of the object. A constraint becomesactive when its guard is verified, where a guard is composed of the occurrence of some method callm along with the verification of a boolean expression on the object state and the actual parameters ofm. A constraint dies when a string of the language corresponding to the regular expression has been recognized. While the commutativity specification is devoted to specify the way in which the external behavior of an object is influenced by the existence of concurrent transactions in the system, the constraint specification defines the behavior of the object, independently from the transactions. Since the two parts of the concurrent behavior are syntactically distinct and, moreover, each of them consists of a set of independent rules, modularity in specifying the objects is enhanced, with respect to a unique specification. We outline an implementation of the construct, which is based on a look-ahead policy: at each method execution, we foresee the admissible successive behaviors of the object, instead of checking the admission of each request at the time it is actually made.     

Formally based tool support for model checking Erlang applications

Model checking as a verification technique has proved effective at the system design and hardware level, and is now beginning to be applied to program code. In this paper, we study the application of model checking techniques in the development of Erlang systems. Erlang is a concurrent functional language with specific support for the development of distributed, fault-tolerant systems with soft real-time requirements. It was designed from the start to support a concurrency-oriented programming paradigm and large distributed implementations that this supports. The methodology we describe in this paper consists of abstracting the behaviour of Erlang and OTP components into a process algebraic specification, specifically an mCRL2 specification, upon which the standard model checker CADP can be used to verify the system’s properties. In addition to rules that model the Erlang syntax, a translation mechanism for the OTP modules gen_server, supervisor and gen_fsm, and the timeout event are defined. A tool-set etomcrl2 has been developed to automate the process of translation. A small illustrative example is used to evaluate the effectiveness of the proposed techniques, and its results show that the proposed techniques are effective in both verifying properties as well as distinguishing between correct and faulty implementations of the design.     

Semantics of under-determined expressions

Some specification languages, such as VDM-SL, allow expressions whose values are not fully determined. This may be convenient in cases where the choice of value should be left to a later stage of development.We consider a simple functional language including such under-determined expressions and present a denotational semantics for the language along with a set of proof rules for reasoning about properties of under-determined expressions. One of the specific problems considered is the combination of under-determinedness and a least fixed point semantics of recursion. Soundness of the proof rules is also discussed.     

LORETO: a tool for reducing state explosion in verification of LOTOS programs

LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value‐passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu‐calculus. The reduced system with respect to ρ preserves the truth value of all selective mu‐calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non‐standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction. Copyright © 1999 John Wiley & Sons, Ltd.     

Visual knowledge specification for conceptual design: Definition and tool support

Current CAD tools are not able to support the conceptual design phase, and none of them provides a consistency analysis for sketches produced by architects. This phase is fundamental and crucial for the whole design and construction process of a building. To give architects a better support, we developed a CAD tool for conceptual design and a knowledge specification tool. The knowledge is specific to one class of buildings and it can be reused. Based on a dynamic and domain-specific knowledge ontology, different types of design rules formalize this knowledge in a graph-based form. An expressive visual language provides a user-friendly, human readable representation. Finally, a consistency analysis tool enables conceptual designs to be checked against this formal conceptual knowledge.In this article, we concentrate on the knowledge specification part. For that, we introduce the concepts and usage of a novel visual language and describe its semantics. To demonstrate the usability of our approach, two graph-based visual tools for knowledge specification and conceptual design are explained.     

A fully abstract semantics of classes for Object-Z

This paper presents a fully abstract semantics of classes for the object oriented formal specification language Object-Z. Such a semantics includes no unnecessary syntactic details and, hence, describes a class in terms of the external behaviour of its objects only. The semantics, based on an extension of existing process models, defines a notion of behavioural equivalence which is stronger than that of CSP and weaker than that of CCS.