Abstract Cloud computing is a conceptual paradigm that is receiving a great deal of interest from a variety of major commercial organisations. By building systems which run within cloud computing infrastructures, problems related to scalability and availability can be reduced.
Abstract Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists.
Abstract We propose what is essentially a recasting of Circus, the Z-and-CSP-based concurrent language for refinement, into a B context by means of a modest extension of classical B which introduces a new structural component called a reactive-B process.
Abstract The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design.
Abstract We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose.
Abstract This paper introduces the subject of secrecy models development by transformation, with formal validation. In an enterprise, constructing a secrecy model is a participatory exercise involving policy makers and implementers.
Abstract One of the key research challenges in autonomic computing is to define rigorous mathematical models for specifying, analyzing, and verifying high-level self-* policies. This paper presents the FracToy formal methodology to specify self-configurable component-based systems, and particularly both their component-based architectural description and their self-configuration policies.
Abstract The B method [1] is gaining visibility in formal methods community due to excellent support for refinement. However, the traceability between the requirements and the formal model is still an issue of this method.
Abstract Event-B does not provide specific support for the modelling of problems that require some structuring, such as, local variables or sequential ordering of events. All variables need to be declared globally and sequential ordering of events can only be achieved by abstract program counters.
Abstract Recently, Space Systems Finland has undertaken formal Event B development of a part of the on-board software for the BepiColombo space mission. As a result, lack of modularisation mechanisms in Event B has been identified as a serious obstacle to scalability.
Abstract A natural encoding of synchronous message exchange with direct wait-control is proved to be equivalent in a distributed environment to a refinement which uses semaphores to implement wait control. The proof uses a most general scheduler, which is left as abstract and assumed to satisfy a few realistic, explicitly stated assumptions.
Abstract Despite the rich literature on network architecture and communication system design, the current practice of describing architectures remains informal and idiosyncratic. Such practice has evolved based on idiomatic terminology and hence, it is failing to provide a formal framework for representing and for reasoning about network architectures.
Abstract Many authors have drawn parallels between the relational model of data and the formal description technique Z, yet none of these contributions have managed to be both close to the relational model in terms of providing a practical means of database design and fully formal in terms of providing an appropriate metamodel.
Abstract The use of formal methods for software development is escalating over the period of time. The input to this formal specification phase is often the documents obtained during the requirements analysis activity which are either textual or semi-formal.
Abstract Safety properties of a system may be specified by constraining the sequences of interactions of the system with its environment. This paper shows how to encode specifications in such a style using Alloy.
Abstract Few tools are available to help with the difficult task of validating that a Z specification captures its intended meaning. One tool that has been proven to be useful for validating specifications is the Alloy Analyzer, an interactive tool for checking and visualising Alloy models.
Abstract Component-based software engineering is a practical approach to address the issue of building large software by combining existing and new components. However, building reliable software systems from components requires to verify the consistency of components and the correctness of their assemblies.