We present an interactive semi-automatic procedure to help users refine their requirements formally and precisely, using knowledge the user possesses but does not notice as relevant and has difficulty formalizing. Questions in natural language are presented to the user, and augmentations to specifications, written in Linear Temporal Logic, are automatically created according to the answers. We apply our approach to a case study on specifying the desired aspect behavior in a delicate case when multiple aspects can share a join-point, i.e., be applied at the same state of base program computation. The questions used in the case study are derived from an in-depth analysis of semantics and mutual influence of aspects at a shared join-point. Aspects sharing a join-point might, but do not have to, semantically interfere. Our analysis and specification refinement enables programmers to distinguish between potential and actual interference among aspects at shared join-points, when aspects are modeled as state transition diagrams, and specifications are given as LTL assumptions and guarantees. The refined aspect specification, obtained from the procedure we describe, enables modular verification and interference detection among aspects even in the presence of shared join-points.

The ideas of a classic distributed superimposition are used to design a new object-oriented version incorporating aspects. A superimposition is a collection of generic parameterized aspects and new classes (often singleton concrete classes). Superimpositions can be combined, either sequentially or in a merge, to create new ones. Superimpositions also include specifications about assumed properties of basic programs to which the superimposition can be applied and desired properties added by the superimposition. These specifications are used to define proof obligations for the correctness of superimpositions and to check feasibility of combining superimpositions. SuperJ, a notation and an implemented preprocessor over AspectJ, is described. SuperJ can be used to apply a superimposition to a basic system, generating concrete aspects from generic aspects and then weaving them to basic classes. Superimpositions are separately declared, specified and verified. Among the examples used to demonstrate the approach are a termination detection algorithm, a version of the Dining Philosophers Problem and a monitoring superimposition that gathers statistics on basic objects.

As system complexity has increased, so has interest in reusing software components in early development phases. While most current modeling methods support design of generic parameterized frameworks or patterns and weaving them into specific models, they do not support open reuse, i.e., the ability to develop partially specified components and refine them in the target application. We introduce an open reuse formalism that is based on OPM/Web, an extension of object-process methodology for distributed systems and Web applications. Our open reuse is accomplished by a three-step process, consisting of designing reusable models, creating basic woven models, and enhancing their specification. We model a reusable component through partially specified environmental elements that are bound to concrete counterparts when the component is integrated into the system under development. Rules for modeling and combining components are defined and applied to a Web example.

A model of computation and a language construct are considered in which global names are used, but all read and write operations are local

article Free Access Share on A superimposition control construct for distributed systems Author: Shmuel Katz Technion–Israel Institute of Technology, Haifa, Israel Technion–Israel Institute of Technology, Haifa, IsraelView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 2April 1993 pp 337–356https://doi.org/10.1145/169701.169682Published:01 April 1993Publication History 122citation463DownloadsMetricsTotal Citations122Total Downloads463Last 12 Months32Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Serializability of database transactions is first defined within the framework of linear temporal logic. For commutativity-based serializability, an alternative specification is given in a temporal logic whose semantic interpretation is especially tailored for reasoning about equivalence sequences of histories. The alternative specification method is given in ISTL* and is limited to the specification of concurrency control algorithms based on commutativity. A formal verification system for serializability that uses classical logic reasoning is provided. Within it, proving serializability of transactions executing a concurrency control algorithm is done along the same lines as proving properties of concurrent programs. Serializability for the multiversion-timestamp algorithm is verified.>

Self-stabilization is an abstraction of fault tolerance for transient malfunctions.Intuitively, a self-stabilizing program resumes normal behavior even if execution begins in an illegal initial state.In this paper, we explore the possibility of extending an arbitrary program into a self-stabilizing one.Our contributions are: (1) a formal definition of the concept of a program being a self-stabilizing extension of a non-stabilizing program; (2) a characterization of what properties may hold in such extensions; (3) a demonstration of the possibility of mechanically creating such extensions.The computational model used is that of an asynchronous distributed message-passing system whose communication topology is an arbitrary graph.We contrast the difficulties of self-stabilization in this model with those of the more common shared-memory models.

An integrated system design for debugging distributed programs written in concurrent high-level languages is described. A variety of user-interface, monitoring, and analysis tools integrated around a uniform process model are provided. Because the tools are language-based, the user does not have to deal with low-level implementation details of distribution and concurrency, and instead can focus on the logic of the program in terms of language-level objects and constructs. The tools provide facilities for experimentation with process scheduling, environment simulation, and nondeterministic selections. Presentation and analysis of the program's behavior are supported by history replay, state queries, and assertion checking. Assertions are formulated in linear time temporal logic, which is a logic particularly well suited to specify the behavior of distributed programs. The tools are separated into two sets. The language-specific tools are those that directly interact with programs for monitoring of and on-line experimenting with distributed programs. The language-independent tools are those that support off-line presentation and analysis of the monitored information. This separation makes the system applicable to a wide range of programming languages. In addition, the separation of interactive experimentation from off-line analysis provides for efficient exploitation of both user time and machine resources. The implementation of a debugging facility for OCCAM is described.

The authors consider the essential properties of a multiparty interaction construct which serves as a primitive for interprocess communication and synchronization in distributed programs. It is claimed that more general constructs, which violate the suggested properties, are appropriate for abstraction but should not be seen as a communication primitive, and that both facilities are needed. Several acceptability criteria are posed for multiparty interactions, and various possibilities for constructs satisfying these criteria are presented. These include introducing a novel kind of nondeterminism within the assignments of an interaction, weakening the synchronization among the participants in an interaction, and varying the number of participants in order to provide a high-level treatment of fault tolerance.>

A new temporal logic and interpretation are suggested which have features from linear temporal logic, branching time temporal logic, and partial order temporal logic.The new logic can describe properties essential to the specification and correctness proofs of distributed algorithms such as those for global snapshots.It is also appropriate for the justification of proof rules and giving temporal semantics to properties such as layering of a program.These properties cannot be described with existing temporal logics.The semantic model of the logic is based on a set of sets of interleaving sequences which reflect partial orders from the underlying semantics of the computational model.For the common partial order derived from sequential&y in execution of each process, the logic will distinguish between nondeterminism due to the parallel execution and nondeterminism due to local nondeterministic choices.The difference in expressive power is thus qualitative, and not merely due to the presence or absence of a particular temporal operator.In the logic, theorems are proven which clarify when it is possible to establish a property P for SGWZ~ of the interleaving computations, and yet conclude the truth of P for every interleaving.

The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate for CSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully acceptable for a model with an n-way synchronization mechanism. Finally, the notion of fairness most often mentioned for Ada is shown to be fully acceptable.

Parallel distributed algorithms are presented for adding and deleting edges in a directed graph without creating a cycle. Such algorithms are useful for a variety of problems in distributed systems such as preventing deadlock or ordering priorities. The algorithms operate in a realistic asynchronous computer network environment in which there are numerous possible interactions among overlapping instances of the algorithms.

The importance of the notion of knowledge in reasoning about distributed systems has been recently pointed out by several works. It has been argued that a distributed computation can be understood and analyzed by considering how it affects the state of knowledge of the system. We show that there are a variety of definitions which can reasonably be applied to what a process can know about he global state. We also move beyond the semantic definitions, and present the first proof methods for proving knowledge asser-tions. Both shared memory and message passing models are considered. 1.

Fairness has become one of the main issues in the theory of non-determinism and concurrency. Recently, the problem of proof rules for fair termination of programs (and some of its variants) has attracted considerable attention ([AO83], [APS82], [GFK83], [GFMR81], [LPS81], [P83]). However, though the main interest and motivation for the consideration of fair termination stems from concurrency, almost all of the recent results are formulated in terms of nondeterministic programs. The main reason for this is the elegance of formalisms for structured nondeterminism, such as Guarded Commands [DIJ76], and their convenience for syntax directed proofs. Other attempts use transition-systems as the program model, and temporal logic as the underlying reasoning formalism ([QS82], [P83]), thereby giving up the structured, syntax-directed, approach.

Optimizing a computer program is defined as improving the execution time without disturbing the correctness. We show how to use invariants from a proof of correctness in order to change the statement in and around the program's loops. This approach is shown to systematize existing optimization methods, and to sometimes allow stronger optimizations than are possible under the standard transformation approach.