bluuebunny/crossref_metadata_2025_split huggingface dataset:
The heritability of cause‐specific mortality: a correlated gamma‐frailty model applied to mortality due to respiratory diseases in Danish twins born 1870–1930
Authors: Wienke Andreas , Holm Niels V. , Christensen Kaare , Skytthe Axel , Vaupel James W. , Yashin Anatoli I. 
Published: December 2003

AbstractThe genetic influence on susceptibility to diseases of the respiratory system and all‐cause mortality was studied using data for identical (MZ) and fraternal (DZ) twins. Data from the Danish Twin Register include 1344 MZ and 2411 DZ male twin pairs and 1470 MZ and 2730 DZ female twin pairs born between 1870 and 1930, where both individuals were alive on 1 011943. We used the correlated gamma‐frailty model. Proportions of variance in frailty attributable to genetic and environmental factors were assessed using the structural equation model approach. For all‐cause mortality the correlation coefficients of frailty for MZ twins tend to be higher than for DZ twins. For mortality with respect to respiratory diseases this effect was only seen in females, whereas males showed the opposite effect. Five standard biometric models are fitted to the data to evaluate the magnitude and nature of genetic and environmental factors on mortality. Using the best fitting biometric model heritability for cause of death was found to be 0.58 (0.07) for all‐cause mortality (AE‐model) and zero for diseases of the respiratory system for males. Heritability was 0.63 (0.11) for all‐cause mortality (DE‐model) and 0.18 (0.09) for diseases ofthe respiratory system (DE‐model) for females. The analysis confirms the presence of a strong genetic influence on individual frailty associated with all‐cause mortality. For respiratory diseases, no genetic influence was found in males and only weak genetic influence in females. The nature of genetic influences on frailty with respect to all‐cause mortality is probably additive in males and dominant in females, whereas for frailty with respect to deaths caused by respiratory diseases in females, there are genetic factors present which are caused by dominance. Environmental influences are non‐shared with exception of frailty with respect to respiratory diseases in males, where the shared environment plays an important role. Copyright © 2003 John Wiley & Sons, Ltd.
Evaluation of Cox's model and logistic regression for matched case‐control data with time‐dependent covariates: a simulation study
Authors: Leffondré Karen , Abrahamowicz Michal , Siemiatycki Jack 
Published: December 2003

AbstractCase‐control studies are typically analysed using the conventional logistic model, which does not directly account for changes in the covariate values over time. Yet, many exposures may vary over time. The most natural alternative to handle such exposures would be to use the Cox model with time‐dependent covariates. However, its application to case‐control data opens the question of how to manipulate the risk sets. Through asimulation study, we investigate how the accuracy of the estimates of Cox's model depends on the operational definition of risk sets and/or on some aspects of the time‐varying exposure. We also assess the estimates obtained from conventional logistic regression. The lifetime experience of a hypothetical population is first generated, and a matched case‐control study is then simulated from this population. We control the frequency, the age at initiation, and the total duration of exposure, as well as the strengths of their effects. All models considered include a fixed‐in‐time covariate and one or two time‐dependent covariate(s): the indicator of current exposure and/or the exposure duration. Simulation results show that none of the models always performs well. The discrepancies between the odds ratios yielded by logistic regression and the ‘true’ hazard ratio depend on both the type of the covariate and the strength of its effect. In addition, it seems that logistic regression has difficulty separating the effects of inter‐correlated time‐dependent covariates. By contrast, each ofthe two versions of Cox's model systematically induces either a serious under‐estimation or a moderate over‐estimation bias. The magnitude of the latter bias is proportional to the true effect, suggesting that an improved manipulation of the risk sets may eliminate, or at least reduce, the bias. Copyright © 2003 JohnWiley & Sons, Ltd.
Construction of a global score quantifying allelic imbalance among biallelic SIDP markers in bladder cancer
Authors: Panhard Xavière , Dominique Sébastien , Gaub Marie‐Pierre , Ravery Vincent , Grandchamp Bernard , Mentré France 
Published: December 2003

AbstractThe purpose of this paper is the construction of an adapted statistical test for urinary detection of bladder cancer basedon the assessment of allelic imbalance using biallelic Short Insertion/Deletion Polymorphism DNA markers. This test is based on the comparison of several of these markers, analysed from urinary DNA, to the distribution of their analogues in blood, which is taken as reference. A reproductibility study is first performed in blood in order to make a selection among the 23 available markers and 18 are retained. A global score based on the χ2 distribution is then built to test for allelic imbalance among all informative markers for each patient. It avoids the count of DNA abnormalities marker by marker and allows to take into account the degree of abnormality of each marker. That method is preliminarily evaluated on a sample of 53 patients and 27 controls. The estimated specificity (96.3%) on that reduced sample is satisfactory, whereas sensitivity (60.4%) could be improved by an augmentation of the number of tested markers. Several issues regarding the validity of the method are discussed. Copyright © 2003 John Wiley & Sons, Ltd.
The analysis of asthma control under a Markov assumption with use of covariates
Authors: Saint‐Pierre P. , Combescure C. , Daurès JP. , Godard P. 
Published: December 2003

AbstractIn studies of disease states and their relation to evolution, data on the state are usually obtained at in frequent time points during follow‐up. Moreover in many applications, there are measured covariates on each individual under study and interest centres on the relationship between these covariates and the disease evolution. We developed a continuous‐time Markov model with use of time‐dependent covariates and a Markov model with piecewise constant intensities to model asthma evolution. Methods to estimate the effect of covariates on transition intensities, to test the assumption of time homogeneity and to assess goodness‐of‐fit are proposed. We apply these methods to asthma control. We consider a three‐state model and we discuss in detail the analysis of asthma control evolution. Copyright © 2003 John Wiley & Sons, Ltd.
Structural Refinement of Systems Specified in Object-Z and CSP
Authors: Derrick John , Smith Graeme 
Published: December 2003

Abstract.
This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.
ArcAngel: a Tactic Language for Refinement
Authors: Oliveira Marcel , Cavalcanti Ana , Woodcock Jim 
Published: December 2003

Abstract.
Morgan's refinement calculus is a successful technique for developing software in a precise and consistent way. This technique, however, can be hard to use, as developments may be long and repetitive. Many authors have pointed out that a lot can be gained by identifying commonly used development strategies, documenting them as tactics, and using them as single transformation rules. Also, it is useful to have a notation for describing derivations, so that they can be analysed and modified. In this paper, we present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics, and some of its algebraic laws. Apart from Angel, a general-purpose tactic language that we are extending, no other tactic language has a denotational semantics and proof theory of its own.
Combining Component Specifications in Object-Z and CSP
Authors: Derrick John , Boiten Eerke 
Published: December 2003

Abstract.

This paper discusses the separation of components from the contexts in which they are used, and how this separation can be supported whilst using different specification languages. There are a number of ways in which this might be possible and here we show how the technique of promotion in Object-Z can be used to combine components which are specified using process algebras. We outline two approaches. The first is to separate out a single specification into a number of distinct
viewpoints
(i.e., partial specifications), each possibly written in a different notation. These viewpoints can be developed separately, but combined if necessary by a process of translation and unification. The alternative approach we discuss is to use a single hybrid language which is composed of a combination of notations, which we illustrate here by combining CSP and Object-Z. We illustrate both approaches with a simple example, and also consider how such component-based descriptions can be refined, which involves addressing the question of compositionality.
An Introduction to Real-Time Object-Z
Authors: Smith Graeme , Hayes Ian 
Published: December 2003

Abstract.
This paper presents Real-Time Object-Z: an integration of the object-oriented, state-based specification language Object-Z with the timed trace notation of the timed refinement calculus. This integration provides a method of formally specifying and refining systems involving continuous variables and real-time constraints. The basis of the integration is a mapping of the existing Object-Z history semantics to timed traces.
Compositional Comparison of Formal Software Specifications Using Transformation Systems
Authors: Große-Rhode Martin 
Published: December 2003

Abstract.
In a model-based software systems development formal specifications of the components of the system are developed. Thereby different specifications are used to represent the different aspects or views of the components, possibly following different paradigms. These heterogeneous viewpoint specifications have to be integrated in order to obtain a consistent global specification of the whole system. In this paper transformation systems are introduced as a common semantic domain where specifications written in different languages can be interpreted and formally compared. A transformation system is a transition system where the transitions are labelled by sets of actions and the states are labelled by algebras representing the data states. Development relations and composition operations for transformation systems are investigated, and it is shown that compatible local developments of components induce a global development of their composition. As an application two specifications of the alternating bit protocol are formally compared component-wise, one given in the process calculus CCS, the other one in the parallel programming language UNITY.
A Collection of Papers and Memoirs Celebrating the Contribution of Rod Burstall to Advances in Computer Science
Authors: RYDEHEARD DAVID E. , SANNELLA DONALD T. 
Published: December 2003

Formal Aspects of Computing
are dedicated to Professor Rod Burstall, and, as a collection of papers, memoirs and incidental pieces, form a Festschrift for Rod. The contributions are made by some of the many who know Rod and have been in uenced by him. The research papers included here represent some of the areas in which Rod has been active, and the editors thank their colleagues for agreeing to contribute to this Festschrift.
Should ML be Object-Oriented?
Authors: MacQueen David 
Published: December 2003

Abstract.At a fundamental level, functional and object-oriented programming languages are all ‘higher-order’, in the sense that they support computing with values that are themselves pieces of program code encapsulated with a local environment. In functional languages these ‘active’ values are functions, while in object-oriented languages they are objects. Both styles of higher-order language claim to provide good support for writing adaptable programs, but functional and object-oriented languages achieve this adaptability in different ways: functional programs rely on parameterisation at the value, type and module level, while object-oriented languages rely primarily on subtyping and implementation inheritance. Here we compare these two approaches, mainly in terms of the features and properties of their type systems, and consider the benefits and disadvantages of unifying (or merging) the two paradigms by adding object-oriented features to ML as a base language. We argue that while some of the simpler aspects of object-oriented languages are compatible with ML, adding a full- edged class-based object system to ML leads to an excessively complex type system and relatively little expressive gain, especially if we aim to preserve that mostly functional style of programming that is a major advantage of ML.
The List Introduction Strategy for the Derivation of Logic Programs
Authors: Pettorossi Alberto , Proietti Maurizio 
Published: December 2003

Abstract.
We present a new program transformation strategy based on the introduction of lists. This strategy is an extension of the tupling strategy which is based on the introduction of tuples of fixed length. The list introduction strategy overcomes some of the limitations of the tupling strategy and, in particular, it makes it possible to transform general recursive programs into linear recursive ones also in cases when this transformation cannot be performed by the tupling strategy. The linear recursive programs we derive by applying the list introduction strategy have in most cases very good time and space performance because they avoid repeated evaluations of goals and unnecessary constructions of data structures.
Dependently Typed Records in Type Theory
Authors: Pollack Robert 
Published: December 2003

Abstract.The languagePebbleof Burstall and Lampson proposed dependent types as the underlying principle in a unified framework to explain facilities for programming in the large, such asmodulesandsignatures, as well as for programming in the small. This proposal soon extended to large scale formal proof development as well. In fact, the functional approach to modularity has turned out to be a hard problem, which is still far from a fully satisfactory solution. This paper discusses aspects of this approach, including representations of records, informative signatures, sharing, and subtyping. My main contribution in this paper is to show that structures with dependent types and manifest fields (roughly ML style modules) are internally definable in a type theoretic framework extended with inductive-recursive definition. This shows that powerful modules follow from general principles without module-specific assumptions.
Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor
Authors: Whittle Jon , Bundy Alan , Boulton Richard 
Published: December 2003

Abstract.

C

Y

NTHIA
is a transformation-based editor for a functional subset of ML that lies somewhere between a structure editor and a framework for formal program development. Users construct programs from existing code by applying editing commands that make a semantic analysis of the program's behaviour, e.g., whether it is terminating. All analysis is done using the
Oyster
system, which is an implementation of proofs-as-programs. We concentrate on identifying analyses that can be done fully automatically (e.g., using a decision procedure) and hence can be hidden from the user. As a result,
C

Y

NTHIA
represents progress towards a goal of program editors that make an intelligent analysis of their code, but in a way that requires no extra input from the programmer.
The Ancient Theory of Mind
Authors: Barendregt Henk 
Published: December 2003

Abstract.
Happiness and suffering are both the result of two factors combined: the situation in which one is placed and our consciousness of it. Happiness is not only of personal importance, it is also a necessary factor for ensuring peace in society. Therefore it is important to know the two possible ways for the pursuit of happiness: applied science, which focuses on how situations can be controlled, and spirituality, which focuses on developing the various types of consciousness one can have. The notion of purified consciousness is formulated in terms of psychology, neurophysiology, logic and meditative practice.
On Verification of Parallel Message-Passing Processes
Authors: Krogdahl Stein , Lysne Olav 
Published: December 2003

Abstract.
One way to reason about parallel processes is to assume that the execution of each process is subdivided into ‘small enough’ steps, and that these are executed in an interleaved fashion, thus obtaining a sequential program. The steps should be so small that for any parallel execution there will, in a suitable sense, exist a corresponding interleaved execution ending in the same state. The usual way to ensure this is to require that each step should contain at most one global access. However, if the global entities are communication channels, then larger steps may in some cases be allowed, and this may make reasoning about the programs easier. This paper explores these cases, and discusses consequences or verification and deadlock avoidance.
On the Use of Data Refinement in the Development of Secure Communications Systems
Authors: Butler Michael 
Published: December 2003

Abstract.
We report on experiences gained from the application of data refinement techniques to the development of examples of secure communications systems. The aim was to the carry the development from initial abstract specification of security services through to detailed designs. The development approach was based on action systems, with B and CSP being used as concrete notations. The security services in question are a confidential communications service and an authenticated transaction service. Refinements include explicit representations of intruder behaviour. The paper makes several interrelated contributions. It demonstrates the feasibility of applying a refinement approach to this type of problem, including an effective way of combining B and CSP in refinements. It introduces a more systematic approach to the development of abstraction invariants and refinement checking. Finally, it illustrates the limitation, when modelling security protocols, of a formalism that does not deal with probability.
Local Invariance
Authors: Pitt David H. , Shields Michael 
Published: December 2003

Abstract.
A local invariant is a set of states of a transition system with the property that every action possible from each of its states takes the system back into the local invariant, unless it is an ‘exit’ action, each of which is accessible from every state in the set via a sequence of non-‘exit’ actions. This idea supports a form of abstraction construction, abstracting away from behaviour internal to the local invariants themselves, that involving their non-‘exit’ actions. In this way, for example, it is possible to construct from a system one which exhibits precisely the externally visible behaviour. This abstraction is reminiscent of hiding in process algebra, and we compare the notion of abstraction with that of observational equivalence in process calculus.
Dynamical Quantities in Net Systems
Authors: Genrich Hartmann J. 
Published: December 2003

Abstract.
The paper presents some known material of higher-level Petri nets in analogy to the dynamics of physical systems. Its aim is to widen the view on the role of the incidence matrix in the analysis of net systems. Rather than focusing on constant state quantities (S-invariants) and cyclic actions (T-invariants), i.e. on solutions of the homogeneous equation systems based on the incidence matrix, it studies dynamical quantities of net systems in general.
Editorial
Authors: COOKE JOHN , MAHARAJ SAVI , ROMIJN JUDI , SHANKLAND CARRON 
Published: December 2003

This issue of Formal Aspects of Computing contains nine papers, all related to the formal specification and the analysis of the ‘Tree Identify’ protocol of the IEEE 1394 High Performance Serial Bus.
In March 2001 a workshop on this topic was held in association with the FME conference in Berlin. All but the first paper in this issue are derived from presentations given at that workshop. The mechanisms for invitations to submit papers for this issue and their subsequent refereeing etc. are detailed in the first paper which also introduces the task that was undertaken.
IEEE 1394 Tree Identify Protocol: Introduction to the Case Study
Authors: Maharaj Savi , Romijn Judi , Shankland Carron 
Published: December 2003

Abstract.
We introduce a comparative case study on the application of formal methods and techniques to the Tree Identify Protocol of the IEEE standard 1394 serial multimedia bus. The Tree Identify Protocol makes an ideal subject for this purpose because it is small yet complex, and may be modelled in a variety of ways. We provide an informal explanation of the protocol, describe how the case study was conducted, and give an overview of the results.
Specification and Verification of the Tree Identify Protocol of IEEE 1394 in Rewriting Logic
Authors: Verdejo Alberto , Pita Isabel , Martí-Oliet Narciso 
Published: December 2003

Abstract.
We present three descriptions, at different abstract levels, of the tree identify protocol from the IEEE 1394 serial multimedia bus standard. The descriptions are given using the language Maude based on rewriting logic. Particularly, the time aspects of the protocol are studied. We prove the correctness of the protocol in two steps. First, the descriptions are validated by an exhaustive exploration of all the possible states reachable from an initial configuration of a network, checking that always only one leader is chosen. Then, we give a formal proof showing that the desirable properties of the protocol are always fulfilled by any network, provided that the network is connected and acyclic.
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV
Authors: Schuppan Viktor , Biere Armin 
Published: December 2003

Abstract.
This case study contains a formal verification of the IEEE 1394 FireWire tree identify protocol. Crucial properties of finite models of the protocol have been validated with state-of-the-art symbolic model checkers. Various optimisation techniques were applied to verify concrete and generic configurations.