A proposal for developing a large patient population cohort for longterm safety monitoring in rheumatoid arthritis

This paper proposes the creation of an objectively acquired reference database to more accurately characterize the incidence and longterm risk of relatively infrequent, but serious, adverse events. Such a database would be maintained longitudinally to provide for ongoing comparison with new rheumatologic drug safety databases collecting the occurrences and treatments of rare events, We propose the establishment of product-specific registries to prospectively follow a cohort of patients with rheumatoid arthritis (RA) who receive newly approved therapies. In addition, a database is required of a much larger cohort of RA patients treated with multiple second line agents of sufficient size to enable case-controlled determinations of the relative incidence of rare but serious events in the treated (registry) versus the larger disease population, The number of patients necessary for agent-specific registries and a larger patient population adequate to supply a matched case-control cohort will depend upon estimates of the detectability of an increased incidence over background. We suggest a system to carry out this proposal that will involve an umbrella organization. responsible for establishment of this large patient cohort, envisioned to be drawn from around the world.

Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Structural refinement of systems specified in object-z and CSP

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.