scholarly journals Proving Monitors Revisited: A First Step Towards Verifying Object Oriented Systems1

1986 ◽  
Vol 9 (4) ◽  
pp. 371-399
Author(s):  
Rob Gerth ◽  
W.P. De Roever
Keyword(s):  
Message Passing ◽  
Object Oriented ◽  
Axiomatic Characterization ◽  
Synchronous Communication ◽  
Proof Systems ◽  
Shared Variables ◽  
Soundness And Completeness ◽  
Sequential Processes ◽  
Object Oriented Systems

An axiomatic characterization of monitors, based on assumption-commitment style reasoning, is given that is sound and (relatively) complete. This characterization is based on the fundamental notions of cooperation and interference, but does not use them as second order notions. The cooperation test was originally conceived to capture the proof theoretical analogue of distributed message passing between disjoint processes, as opposed to the interference freedom test, being the proof theoretical analogue of concurrency based on interference by jointly shared variables. Since then, the cooperation test has been applied to characterize synchronous communication in Hoare’s Communicating Sequential Processes, Ichbia’s Ada, and Wirth’s Modula-2, supported by soundness and completeness proofs. An overview is given of the rationale underlying this characterization, culminating in the development of proof systems for a new monitor based programming language for concurrency (Communicating Modules, CM) which combines distributed message passing between processes with interference through local variables of a process which are shared between its sub-processes. As such this is a first step towards the formal verification of object oriented systems. In this context, we also show how the method, traditionally cauched in terms of proof outlines, can be rendered syntax directed in a precise and formal way. In a separate paper, the proof system has been shown to be sound and (relatively) complete.

scholarly journals A logical characterization of asynchronously communicating agents

1990 ◽  
Vol 19 (309) ◽  
Author(s):  
Søren Christensen
Keyword(s):  
Distributed Systems ◽  
Temporal Logic ◽  
Message Passing ◽  
Partial Orders ◽  
Soundness And Completeness ◽  
Sequential Processes

<p>In this paper we study the behaviour of distributed systems. We consider systems composed of a <em>fixed</em> number of sequential processes communicating by asynchronous message passing. The behaviour is represented by a subclass of partial orders called <em>asynchronously communicating agent structures</em>, abbreviated ACA structures.</p><p>We present a logical characterization of ACA structures in the framework of temporal logic.</p><p>The modalities of the logic capture the concepts of <em>communication</em>, <em>concurrency</em> and <em>locality</em>.</p><p>We define an axiomatic basis for the logic and show both soundness and completeness.</p>

A unifying type-theoretic framework for objects

1995 ◽  
Vol 5 (4) ◽  
pp. 593-635 ◽  
Author(s):  
Martin Hofmann ◽  
Benjamin Pierce
Keyword(s):  
Message Passing ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Theoretic Characterization ◽  
Abstract Framework

AbstractWe give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit constructor for object types and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a basis for justifying and comparing previous encodings of objects based on recursive record types (Cardelli, 1984; Cardelli, 1992; Bruce, 1994; Cook et al., 1990; Mitchell, 1990a) and encodings based on existential types (Pierce & Turner, 1994).

scholarly journals Towards a Theory of Regular MSC Languages

1999 ◽  
Vol 6 (52) ◽  
Author(s):  
Jesper G. Henriksen ◽  
Madhavan Mukund ◽  
K. Narayan Kumar ◽  
P. S. Thiagarajan
Keyword(s):  
Message Passing ◽  
Finitely Generated ◽  
Message Sequence Charts ◽  
Proper Subclass ◽  
Finite State ◽  
Sequence Graph ◽  
System Requirements ◽  
Sequential Processes ◽  
Theoretic Characterization

Message Sequence Charts (MSCs) are an attractive visual formalism<br /> widely used to capture system requirements during the early<br />design stages in domains such as telecommunication software. It is<br />fruitful to have mechanisms for specifying and reasoning about <br />collections of MSCs so that errors can be detected even at the requirements<br /> level. We propose, accordingly, a notion of regularity for <br />collections of MSCs and explore its basic properties. In particular, we<br />provide an automata-theoretic characterization of regular MSC <br />languages in terms of finite-state distributed automata called bounded<br />message-passing automata. These automata consist of a set of <br />sequential processes that communicate with each other by sending and<br />receiving messages over bounded FIFO channels. We also provide a<br />logical characterization in terms of a natural monadic second-order<br />logic interpreted over MSCs.<br />A commonly used technique to generate a collection of MSCs is<br />to use a Message Sequence Graph (MSG). We show that the class of<br />languages arising from the so-called locally synchronized MSGs constitute<br /> a proper subclass of the languages which are regular in our sense.<br />In fact, we characterize the locally synchronized MSG languages as<br />the subclass of regular MSC languages that are finitely generated.

Lightweight checkpointing for concurrent ML

2010 ◽  
Vol 20 (2) ◽  
pp. 137-173 ◽  
Author(s):  
LUKASZ ZIAREK ◽  
SURESH JAGANNATHAN
Keyword(s):  
Message Passing ◽  
Large Scale ◽  
Software Systems ◽  
Transient Faults ◽  
Standard Ml ◽  
Shared Variables ◽  
Communication Events ◽  
Linguistic Abstraction ◽  
Viable Mechanism

AbstractTransient faults that arise in large-scale software systems can often be repaired by reexecuting the code in which they occur. Ascribing a meaningful semantics for safe reexecution in multithreaded code is not obvious, however. For a thread to reexecute correctly a region of code, it must ensure that all other threads that have witnessed its unwanted effects within that region are also reverted to a meaningful earlier state. If not done properly, data inconsistencies and other undesirable behavior might result. However, automatically determining what constitutes a consistent global checkpoint is not straightforward because thread interactions are a dynamic property of the program. In this paper, we present a safe and efficient checkpointing mechanism for Concurrent ML (CML) that can be used to recover from transient faults. We introduce a new linguistic abstraction, called stabilizers, that permits the specification of per-thread monitors and the restoration of globally consistent checkpoints. Safe global states are computed through lightweight monitoring of communication events among threads (e.g., message-passing operations or updates to shared variables). We present a formal characterization of its design, and provide a detailed description of its implementation within MLton, a whole-program optimizing compiler for Standard ML. Our experimental results on microbenchmarks as well as several realistic, multithreaded, server-style CML applications, including a web server and a windowing toolkit, show that the overheads to use stabilizers are small, and lead us to conclude that they are a viable mechanism for defining safe checkpoints in concurrent functional programs.

Early generation of performance models for object-oriented systems

2000 ◽  
Vol 147 (3) ◽  
pp. 61 ◽  
Author(s):  
V. Cortellessa ◽  
G. Iazeolla ◽  
R. Mirandola
Keyword(s):  
Object Oriented ◽  
Performance Models ◽  
Early Generation ◽  
Object Oriented Systems

Testing Refactoring Implementations of Object-Oriented Systems

2018 ◽  
Vol 6 (7) ◽  
pp. 530-534
Author(s):  
B. Nagaveni ◽  
A. Ananda Rao ◽  
P. Radhika Raju
Keyword(s):  
Object Oriented ◽  
Object Oriented Systems

The object-oriented systems life cycle

1990 ◽  
Vol 33 (9) ◽  
pp. 142-159 ◽  
Author(s):  
Brian Henderson-Sellers ◽  
Julian M. Edwards
Keyword(s):  
Life Cycle ◽  
Object Oriented ◽  
Object Oriented Systems

An Axiomatic Characterization of a Class of Petri Nets

1991 ◽  
Vol 14 (4) ◽  
pp. 477-491
Author(s):  
Waldemar Korczynski
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Axiomatic Characterization ◽  
Algebraic Characterization

In this paper an algebraic characterization of a class of Petri nets is given. The nets are characterized by a kind of algebras, which can be considered as a generalization of the concept of the case graph of a (marked) Petri net.

Sign in / Sign up

Export Citation Format

Share Document