Scientific facilities, in particular large-scale photon and neutron sources, have demanding requirements to manage the increasing quantities of experimental data they generate in a systematic and secure way. In this paper, we describe the ICAT infrastructure for cataloguing facility-generated experimental data which has been in development within STFC and DLS for several years. We consider the factors which have influenced its design and describe its architecture and metadata model, a key tool in the management of data. We go on to give an outline of its current implementation and use, with plans for its future development.

In this paper, we discuss the use of formal requirements-engineering techniques in capturing security requirements for a Grid-based operating system. We use KAOS goal model to represent two security goals for Grid systems, namely authorisation and single-sign on authentication. We apply goal-refinement to derive security requirements for these two security goals and we develop a model of anti-goals and show how system vulnerabilities and threats to the security goals can arise from such anti-models.

Abstract The verified software repository is dedicated to a long-term vision of a future in which all computer systems justify the trust that society increasingly places in them. This would be accompanied by a substantial reduction in the current high costs of programming error, incurred during the design, development, testing, installation, maintenance, evolution, and retirement of computer software. An important technical contribution to this vision will be a verifying compiler: a tool-set that automatically proves that a program will always meet its specification, insofar as this has been formalised, without even needing to run it. This has been a challenge for computing research for over 30 years, but the current state of the art now gives grounds for hope that it may be implemented in the foreseeable future. Achievement of the overall vision will depend also on continued progress of research into dependability and software evolution, as envisaged by the UKCRC Grand Challenge project in dependable systems evolution . The verified software repository is a first step towards the realisation of this long-term vision. It will maintain and develop an evolving collection of state-of-the-art tools, together with a representative portfolio of real programs and specifications on which to test, evaluate, and develop the tools. It will contribute initially to the inter-working of tools, and eventually to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering practice. It will build on the recognised achievements of practical formal development of safety-critical computer applications, and contribute to an international initiative in verified software, covering theory, tools, and experimental validation.

Abstract. VDM and B are two mature formal methods currently in use by industry and supported by commercial tools. Though the methods are foundationally similar, the coverage of their supporting tools differ significantly. The SPECTRUM project has investigated the feasibility of integrating support for the two methodologies. In this paper, we describe the project and report on some technical results.

Although the formal method VDM has been in existence since the 1970s, there are still no satisfactory tools to support verification in VDM. The paper deals with one possible means of approaching this problem by using the PVS theorem-prover. It describes a translation of a VDM-SL specification into the PVS specification language using, essentially, the very transparent translation methods described by Agerholm (1996). PVS was used to typecheck the specification and to prove some non-trivial validation conditions. Next, a more abstract specification of the same system was also expressed in PVS, and the original specification was shown to be a refinement of this one. The drawbacks of the translation are that it must be done manually (though automation may be possible), and that the "shallow embedding" technique which is used does not accurately capture the proof rules of VDM-SL. The benefits come from the facts that the portion of VDM-SL which can be represented is substantial and that it is a great advantage to be able to use the powerful PVS proof-checker.

VDM and B are two "model-oriented" formal methods. Each gives a notation for the specification of systems as state machines in terms of a set of states with operations defined as relations on that set. Each has a notion of refinement of data and operations based on the principles of reduction of nondeterminism and increase in definedness. The paper makes a comparison of the two notations through an example of a communications protocol previously formalized by G. Bruns and S. Anderson (1994). Two abstractions and two reifications of the original specification are given. Particular attention is paid to three areas where the notations differ: the use of postconditions that assume the invariant as opposed to postconditions that enforce it; the explicit "framing" of operations as opposed to the "minimal frame" approach; and the use of relational postconditions as opposed to generalized substitutions.>