1. |
- Andersen, Jörgen H., et al.
(author)
-
A Machine Verified Distributed Sorting Algorithm
- 1996
-
Reports (other academic/artistic)abstract
- We present a verification of a distributed sorting algorithm in ALF, an implementation of Martin Löf's type theory. The implementation is expressed as a program in a priortized version of CBS, (the Calculus of Broadcasting Systems) which we have implemented in ALF. The specification is expressed in terms of an ALF type which represents the set of all sorted lists and an HML (Hennesey-Milner Logic) formula which expresses that the sorting program will input any number of data until it hears a value triggering the program to begin outputting the data in a sorted fashion. We gain expressive power from the type theory by inheriting the language of data, state expressions, and propositions.
|
|
2. |
- Harcourt, Ed, et al.
(author)
-
A Framework for Representing Parameterised Processes
- 1995
-
Reports (other academic/artistic)abstract
- We describe a faithful representation of value-passing recursive parametric CCS processes in Alf, an implementation of Martin-Lof's constructive type theory. The representation is interesting because we borrow as much as possible from Alf including the domain of value and state expressions and the ability to evaluate them. Usually substitution of either channel values for channel variables and processes for process variables play a necessary role in the semantics. However, substitution is also borrowed from Alf by using higher-order functions. The main importance of this representation is that it allows us to borrow Alf's off-the-shelf theorems about data types and provides a uniform setting for doing various kinds machine assisted proofs, such as bisimulation proofs, equational reasoning, verification of Hennessy-Milner logic formulas. 1 Introduction Machine checked proofs of CCS processes require finite representations of the processes. However, for infinite value and state domains,...
|
|
3. |
- Prasad, K V S, 1952
(author)
-
A Calculus of Broadcasting Systems
- 1995
-
In: Science of Computer Programming. - 0167-6423. ; 25:2-3, s. 285-327
-
Journal article (peer-reviewed)abstract
- CBS is a simple and natural CCS-like calculus where processes speak one at a time and are heard instantaneously by all others. Speech is autonomous, contention between speakers being resolved non-deterministically, but hearing only happens when someone else speaks. Observationally meaningful laws differ from those of CCS. The change from handshake communication in CCS to broadcast in CBS permits several advances.1. Priority, which attaches only to autonomous actions, is simply added to CBS in contrast to CCS, where such actions are the result of communication.2. A CBS simulator runs a process by returning a list of values it broadcasts. This permits a powerful combination, CBS with the host language. It yields several elegant algorithms. Only processes with a unique response to each input are needed in practice, so weak bisimulation is a congruence.3. CBS subsystems are interfaced by translators; by mapping messages to silence, these can restrict hearing and hide speech.Reversing a translator turns its scope inside out. This permits a new specification for a communication link: the environment of each user should behave like the other user.This paper reports the stable aspects of an evolving study.
|
|
4. |
- Prasad, K V S, 1952
(author)
-
Broadcasting in Time
- 1996
-
In: Springer Lecture Notes in Computer Science (Coordination Languages and Models, First International Conference, COORDINATION '96). - 3540610529
-
Conference paper (peer-reviewed)abstract
- In the calculus of broadcasting systems (CBS), speech is autonomous, but hearing takes place only when the environment speaks. This paper develops a timed CBS (TCBS) where no time may pass if there is speech pending. A process wishing to speak can be forced, by attaching a time-out to it, to first listen for a specified length of time. TCBS subsumes CBS with priorities, and has an expansion theorem even if time is dense. A delay prefix operator can be derived up to weak bisimulation. TCBS casts light on issues in handshake communication: time abstracted bisimulation, and the relations between time and priority, between expansion theorems and density of time, and between delays and time-outs.
|
|
5. |
- Sundararajan, G., et al.
(author)
-
A Comparative Study of Tribological Behavior of Plasma and D-Gun Sprayed Coatings under Different Wear Modes
- 1998
-
In: Journal of Materials Engineering and Performance. ; 7:3, s. 343-351
-
Journal article (peer-reviewed)abstract
- In recent years, thermal sprayed protective coatings have gained widespread acceptance for a variety of industrial applications. A vast majority of these applications involve the use of thermal sprayed coatings to combat wear. While plasma spraying is the most versatile variant of all the thermal spray processes, the detonation gun (D-gun) coatings have been a novelty until recently because of their proprietary nature. The present study is aimed at comparing the tribological behavior of coatings deposited using the two above techniques by focusing on some popular coating materials that are widely adopted for wear resistant applications, namely, WC-12%Co, Al2O3, and Cr3C2-NiCr. To enable a comprehensive comparison of the above indicated thermal spray techniques as well as coating materials, the deposited coatings were extensively characterized employing microstructural evaluation, microhardness measurements, and XRD analysis for phase constitution. The behavior of these coatings under different wear modes was also evaluated by determining their tribological performance when subjected to solid particle erosion tests, rubber wheel sand abrasion tests, and pin-on-disk sliding wear tests. The results from the above tests are discussed here. It is evident that the D-gun sprayed coatings consistently exhibit denser microstructures and higher hardness values than their plasma sprayed counterparts. The D-gun coatings are also found to unfailingly exhibit superior tribological performance superior to the corresponding plasma sprayed coatings in all wear tests. Among all the coating materials studied, D-gun sprayed WC-12%Co, in general, yields the best performance under different modes of wear, whereas plasma sprayed Al2O3 shows least wear resistance to every wear mode.
|
|