bluuebunny/crossref_metadata_2025_split huggingface dataset:
Axiomatic treatment of processes with shared variables revisited
Authors: Owe Olaf 
Published: February 2005

Abstract
The aim of this paper is to develop simple and practically useful formalisms for reasoning about processes with shared variables. Our approach is based on the axiomatic system described by Neelam Soundararajan. In contrast to that work, our formalism is first derived from a model; this guarantees soundness and completeness of the formal proof system, with respect to the model. As an additional advantage the rules become simpler than those of Soundararajan; in particular, the local assertions may freely refer to shared variables; and we remove the explicit use of the compatibility predicate.
Next we augment the formalism by allowing global invariants, which may refer to shared variables (including shared histories), but with a different semantics than in the local assertions. The augmented system makes reasoning simpler in the sense that reasoning about the past is replaced by reasoning about the present. Finally we suggest a sufficiently complete set of mythical (auxiliary) variables free from embedded program structure. We demonstrate our formalism on some examples.
An implementation of syntax directed functional programming on nested-stack machines
Authors: Fassbender Heinz , Vogler Heiko 
Published: February 2005

AbstractThis paper contributes to the field of functional programming languages. We investigate the call-by-name and call-by-need implementation of a restricted type of functional programming, calledsyntax directed functional programming; the target of this implementation is an abstract machine that is based on nested stacks. In fact, the technical kernel of this paper is a refinement of an automata theoretical result that, roughly speaking, investigates the well-known relationship “recursion = iteration + stack” in the framework of tree transducers. More precisely, in the underlying result the class of functions computed by total deterministic macro tree-to-string transducers with the call-by-name computation strategy is characterized by total deterministic checking-tree nested-stack transducers. Note that total deterministic macro tree-to-string transducers are term rewriting systems by means of which the reduction semantics of syntax directed functional programming languages can be described.
Equality of agent expressions is preserved under an extension of the universe of actions
Authors: Massart T. , Devillers R. 
Published: February 2005

Abstract
In a basic agent calculus, equality often links the agents which provide the same external behaviour in any context. Since the universe of agents and the universe of contexts depend on the used action set, equality depends a priori on this set of actions. We show here that if we select from the universe of agents, two agents which are equal, they are also equal if we extend the universe of actions (and consequently if we extend the universe of agents and contexts).
A demonstrably correct compiler
Authors: Stepney Susan , Whitley Dave , Cooper David , Grant Colin 
Published: February 2005

Abstract
As critical applications grow in size and complexity, high level languages, rather than better-trusted assembly languages, will be used in their development. This adds potential for extra errors to creep in, especially in the now necessary compiler. To avoid these new errors, it is necessary to have a formal specification of the high level language, and a formal development of its compiler. We outline what we believe is a practical route for achieving a demonstrably correct compiler, and describe a prototype compiler we have built by this route for a small, but non-trivial, language.
Theories for mechanical proofs of imperative programs
Authors: Hesselink Wim H. 
Published: February 2005

Abstract
For convenient application of a first-order theorem prover to verification of imperative programs, it is important to encapsulate the operational semantics in generic theories. The possibility to do so is illustrated by two theories for the Boyer-Moore theorem prover Nqthm.
The first theory is an Nqthm version of the classical while-theorem. Here the main interest is to show how one can use Nqthm's facilities to constrain and to functionally instantiate for the development and application of a generic theory. The theory is illustrated by a linear search program.
The second theory is a finitary approach to progress for shared-memory concurrent programs. It is illustrated by Peterson's algorithm for mutual exclusion of two processes. The proof of progress for Peterson's algorithm is new. The assertion of bounded fairness is slightly stronger than the conventional notion of weak fairness. This new concept may have other applications.
Verifying programs in the calculus of inductive constructions
Authors: Parent-Vigouroux Catherine 
Published: February 2005

AbstractThis paper deals with a particular approach to the verification of functional programs. A specification of a program can be represented by a logical formula [Con86, NPS90]. In a constructive framework, developing a program then corresponds to proving this formula. Given a specification and a program, we focus on reconstructing a proof of the specification whose algorithmic contents corresponds to the given program. The best we can hope is to generate proof obligations on atomic parts of the program corresponding to logical properties to be verified. First, this paper studies a weak extraction of a program from a proof that keeps track of intermediate specifications. From such a program, we prove the determinism of retrieving proof obligations. Then, heuristic methods are proposed for retrieving the proof from a natural program containing only partial annotations. Finally, the implementation of this method as a tactic of theCoqproof assistant is presented.
The semantics of the combination of atomized statements and parallel choice
Authors: Knijnenburg Peter M. W. , Kok Joost N. 
Published: February 2005

Abstract

In this paper we define a uniform language
ℒ
that is an extension of the language underlying the process algebra
PA
. One of the main extensions of this language over
PA
is given by so-called atomizing brackets. If we place these brackets around a statement then we treat this statement as an atomic action. Put differently, these brackets remove all interleaving points. We present a transition system for the language and derive its operational semantics. We show that there are several options for defining a transition system such that the resulting operational semantics is a conservative extension of the semantics for
PA
. We define a semantic domain and a denotational model for the language. Next we define a closure operator on the semantic domain and show how to use this closure operator to derive a fully abstract denotational semantics. Then the algebraic theory of the language is considered. We define a collection of axioms and a term rewrite system based on these axioms. Using this term rewrite system we are able to identify normal forms for the language. It is shown that these axioms capture the denotational equality. It follows that if two terms are provably equal then they have the same operational semantics. Finally, we show how to extend the axiomatization in order to axiomatize its operational equivalence.
Verification of schedulability for real-time programs
Authors: Liu Zhiming , Joseph Mathai , Janowski Tomasz 
Published: February 2005

Abstract

Assume that a real-time program
P
T
consisting of a number of parallel processes is executed on a system having a set
Pr
of processors which are shared between the processes by a real-time scheduler
S
T
. Assume that P
T
must meet some timing deadlines. We show that such an implementation of
P
T
can be represented as a transformationL(
P
T
) and that the deadlines of
P
T
will be met if they are satisfied by the timing properties of the transformed program. The condition for feasibility of a real-time program executed under a scheduler is formalized and rules are provided for verification. The scheduler
S
T
can be specified
generically
and applied to different programs, making it unnecessary to introduce low-level operations such as scheduling primitives into the programming language. Thus real-time program specification and Schedulability can be considered in the same framework and the timing properties of a program can be determined at the specification level. By separating the specification of the scheduler from that of the program, the feasibility of an implementation can be proved by considering a scheduling policy rather than its implementation details.
Response to “the formal specification of safety requirements for storing explosives”
Authors: Larsen Peter Gorm 
Published: February 2005

Abstract
This short communication is a response to [MuS93] investigating their ACS system specification. The main point in this paper is that executing specifications can be used as a feasible way of validating them. It is essential to have tool support which enables one to write a generally not executable specification, and then prototype (parts of) it directly in the specification language, without translating it into some other prototyping language.
Action transducers and timed automata
Authors: Lynch Nancy , Vaandrager Frits 
Published: February 2005

Abstract

The
timed automaton model
of [LyV92, LyV93] is a general model for timing-based systems. A notion of
timed action transducer
is here defined as an automata-theoretic way of representing operations on timed automata. It is shown that two timed trace inclusion relations are substitutive with respect to operations that can be described by timed action transducers. Examples are given of operations that can be described in this way, and a preliminary proposal is given for an appropriate language of operators for describing timing-based systems.
Automatic verification of a class of systolic circuits
Authors: Abdulla Parosh 
Published: February 2005

Abstract
Systolic circuits have attracted considerable attention as a means of implementing parallel algorithms in areas such as linear algebra, signal processing, pattern matching, etc. A systolic circuit is composed of a number of computation cells which are connected in a regular pattern. Each cell can perform computations, store data and communicate with other cells in the circuit. We define a language to describe implementations and specifications of a class of systolic circuits whose cells compute over a commutative ring, and present a decision method to check whether or not a circuit implementation fulfils a specification. The main advantage of our approach, compared with earlier work in the field, is that the verification is performed automatically, without user interaction. We give an example of how the method may be applied to verify a convolution circuit.
Type inference with non-structural subtyping
Authors: Palsberg Jens , Wand Mitchell , O'Keefe Patrick 
Published: February 2005

Abstract

We present an O(n
3
) time type inference algorithm for a type system with a largest type
Τ
, a smallest type ⊥, and the usual ordering between function types. The algorithm infers type annotations of least shape, and it works equally well for recursive types. For the problem of typability, our algorithm is simpler than the one of Kozen, Palsberg, and Schwartzbach for type inference
without
⊥. This may be surprising, especially because the system with ⊥ is strictly more powerful.
Equivalence of formal semantics definition methods
Authors: Caswell M. J. A. 
Published: February 2005

Abstract
There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves.
Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.
A strict functional language with cyclic recursive data
Authors: Nishimura Susumu 
Published: February 2005

Abstract
The paper proposes a strict functional language to program with cyclic recursive data structures. In the language, each recursive datum is represented by a system of equations. Cyclic structures are naturally expressed by this representation, and the language provides a general mechanism that transforms several such systems of equations into a single new system of equations. An operational semantics and a polymorphic type system for the language are given, and a type soundness proof is sketched. Finally, it is also shown that the language can be implemented in a data-parallel fashion.
Presupposition failure — A comedy of errors
Authors: van Eijck Jan 
Published: February 2005

AbstractPresuppositions of utterances are the pieces of information you convey with an utterance no matter whether your utterance is true or not. We first study presupposition in a very simple framework of updating propositional information, with examples of how presuppositions of complex propositional updates can be calculated. Next we move on to presuppositions and quantification, in the context of a dynamic version of predicate logic, suitably modified to allow for presupposition failure. In both the propositional and the quantificational case, presupposition failure can be viewed as error abortion of procedures. Thus, a dynamic assertion logic which describes the preconditions for error abortion is the suitable tool for analysing presupposition.
Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
Authors: Stølen Ketil , Dederichs Frank , Weber Rainer 
Published: February 2005

Abstract

This paper presents an assumption/commitment specification technique and a refinement calculus for networks of agents communicating asynchronously via unbounded FIFO channels in the tradition of Kahn.

We define two types of assumption/commitment specifications, namely simple and general specifications.

It is shown that semantically, any deterministic agent can be uniquely characterized by a simple specification, and any nondeterministic agent can be uniquely characterized by a general specification.

We define two sets of refinement rules, one for simple specifications and one for general specifications. The rules are Hoare-logic inspired. In particular the feedback rules employ invariants in the style of a traditional while-rule.

Both sets of rules have been proved to be sound and also (semantic) relative complete.

Conversion rules allow the two logics to be combined. This means that general specifications and the rules for general specifications have to be introduced only at the point in a system development where they are really needed.
Architectural CCS
Authors: Krishnan Padmanabhan 
Published: February 2005

AbstractIn this article, we discuss the effect of architectures on behaviours and the notions of equivalence for CCS terms. Two types of architectures are considered viz, shared memory systems and distributed memory systems. Processes can be logically migrated in shared memory systems while in distributed memory systems, processes are bound to a location and require explicit migration. Communication in shared memory systems can follow the CCS principle. A complete equational characterisation of the bisimulation equivalence induced by the execution on multiprocessors requires an extended syntax; which captures the process of compiling and loading. To permit a realistic description of communication in distributed systems, asynchronous actions are required. Due to this the complete axiomatisation for the bisimulation equivalence is more sensitive to the causal structure of the processes. A practical interpretation to the complete axiomatisation of the bisimulation equivalence is also given.
Progress assumption in concurrent systems
Authors: Costa J. F. , Sernadas A. 
Published: February 2005

Abstract

A denotational semantics and a sound and complete inequational proof systems for processes with varying degrees of liveness is presented. New insights on
quiescence
are given concerning the Jonsson characterisation of input/output system. A theory of
transational behaviour
of the type
carry out until the end
is developed as an application of this concept of process with liveness requirements. The proposed model fully reflects the parallel composition of
transactional requirements
, giving the expected composite requirements.
A blocking model for reactive objects
Authors: Duke Roger , Bailes Cecily , Smith Graeme 
Published: February 2005

Abstract
Objects can be viewed as entities reacting concurrently with their environment through the sending and receiving of messages. In this paper a model for such reactive objects is constructed where messages may be blocked either by the object or by the environment. This model differentiates between output messages controlled by the object, and input messages controlled by the environment. The model is applied to define an object compatibility lattice structure enabling the construction of objects satisfying best possible compatibility requirements.
The NDB database specified in the RAISE specification language
Authors: George Chris 
Published: February 2005

Abstract
This paper answers a challenge designed to test the modularization features of specification languages. The RAISE Specification Language (RSL) is shown to have the power necessary to meet the challenge.
Basic features of RSL, particularly those useful for the problem, are introduced. Two solutions to the problem are exhibited. The first follows the structure of the challenge problem very closely and is model-based in style. The second shows how RSL may be written in an algebraic style.
An example of a proof of implementation is also given.
Modularising the specification of a small database system in extended ML
Authors: Kazmierczak Edmund 
Published: February 2005

Abstract
A case study in the modular specification and refinement of a small database system is presented in Extended ML. Two similar requirements specifications are given and a program development step from each these is presented. The structure resulting from the first program development step is similar to that given in [FiJ90] and is presented as an answer to the challenge problem given in that paper, while the second development step is presented as a possible alternative which is more suited to the Extended ML style of program development. In the context of these two development steps the module facilities of Extended ML, their role in specification and program development and their ability to meet the challenge of [FiJ90] are examined.
On sequential composition, action prefixes and process prefix
Authors: Baeten J. C. M. , Bergstra J. A. 
Published: February 2005

Abstract
We illustrate the difference between sequential composition in process algebra axiomatisations like ACP and action prefixing in process calculi like CCS. We define both early and late input in a general framework extending ACP, and consider various subalgebras, some very close to value passing CCS, another one close to CSP.
Why would cement porosity reduction be clinically irrelevant, while experimental data show the contrary
Authors: Janssen D. , Stolk J. , Verdonschot N. 
Published: February 2005

AbstractLaboratory bench tests have shown that porosity reduction increases the fatigue life of bone cement specimens. Clinically, however, the effect porosity reduction is subject to debate. We hypothesized that the discrepancy between clinical and experimental findings is related to differences in the stress distribution, which is typically uniform in experimental test specimens, while stress concentrations exist in cement around hip implants. We simulated fatigue failure of cement in a finite element model of an experimental test specimen and of a transverse slice of a total hip arthroplasty with a sharp‐cornered stem. Four levels of porosity were introduced. In the fatigue test specimen model, the fatigue life clearly was dependent on the level of porosity, while in the transverse slice model, the level of porosity had virtually no effect on failure of the cement mantle. The results of the simulations confirmed our hypothesis. In simulations of laboratory tests, pores clearly acted as crack initiators, while in the simulation of a real total hip reconstruction, crack formation was governed by local stress singularities. This explains why the beneficial effect of cement porosity reduction on the lifetime of total hip reconstructions may be hard to detect clinically. © 2005 Orthopaedic Research Society. Published by Elsevier Ltd. All rights reserved.
Object-oriented biological system integration: a SARS coronavirus example
Authors: Shegogue Daniel , Zheng W. Jim 
Published: February 2005

Abstract

Motivation
The importance of studying biology at the system level has been well recognized, yet there is no well-defined process or consistent methodology to integrate and represent biological information at this level. To overcome this hurdle, a blending of disciplines such as computer science and biology is necessary.

Results
By applying an adapted, sequential software engineering process, a complex biological system (severe acquired respiratory syndrome-coronavirus viral infection) has been reverse-engineered and represented as an object-oriented software system. The scalability of this object-oriented software engineering approach indicates that we can apply this technology for the integration of large complex biological systems.

Availability
A navigable web-based version of the system is freely available at http://people.musc.edu/~zhengw/SARS/Software-Process.htm

Contact
zhengw@musc.edu

Supplementary information
Supplemental data: Table 1 and Figures 1–16.