Cookies on this website
We use cookies to ensure that we give you the best experience on our website. If you click 'Continue' we'll assume that you are happy to receive all cookies and you won't see this message again. Click 'Find out more' for information on how to change your cookie settings.
  • Model-driven architecture for cancer research

    16 October 2018

    It is a common phenomenon for research projects to collect and analyse valuable data using ad-hoc information systems. These costly-to-build systems are often composed of incompatible variants of the same modules, and record data in ways that prevent any meaningful result analysis across similar projects. We present a framework that uses a combination of formal methods, model-driven development and service-oriented architecture (SOA) technologies to automate the generation of data management systems for cancer clinical trial research, an area particularly affected by these problems. The SOA solution generated by the framework is based on an information model of a cancer clinical trial, and comprises components for both the collection and analysis of cancer research data, within and across clinical trial boundaries. While primarily targeted at cancer research, our approach is readily applicable to other areas for which a similar information model is available. © 2007 IEEE.

  • A comparison of replication strategies for reliable decentralised storage

    16 October 2018

    Distributed hash tables (DHTs) can be used as the basis of a resilient lookup service in unstable environments: local routing tables are updated to reflected changes in the network; efficient routing can be maintained in the face of participant node failures. This fault-tolerance is an important aspect of modern, decentralised data storage solutions. In architectures that employ DHTs, the choice of algorithm for data replication and maintenance can have a significant impact upon performance and reliability. This paper presents a comparative analysis of replication algorithms for architectures based upon a specific design of DHT. It presents also a novel maintenance algorithm for dynamic replica placement, and considers the reliability of the resulting designs at the system level. The performance of the algorithms is examined using simulation techniques; significant differences are identified in terms of communication costs and latency. © 2006 ACADEMY PUBLISHER.

  • Toward provably correct models of ventricular cell function

    16 October 2018

    Researchers in cardiac mechanics and electrophysiology develop computer models for analyzing complex experimental data. A key issue is model correctness: formally verifying that the model is performing as intended. We present an application of formal software engineering methods to an established electrophysiology model: the Beeler-Reuter (B-R) model of the mammalian ventricular myocyte. A formal specification fragment for the B-R model is developed, which captures the key drivers of the transmembrane potential, including four ionic currents (INa, Is, Ix1, and IK1) and a representation for the intracellular calcium ion concentration ( [Ca] ). Correctness-preserving transformations can be used to refine the specification into executable code, thereby assuring a provably correct implementation. The mathematical and logical tools presented here provide a rigorous approach to proving the correctness of ventricular cell models, thereby improving program implementation and verification.

  • Automatic maintenance of association invariants

    16 October 2018

    Many approaches to software specification and design make use of invariants: statements whose truth is preserved under various operations upon a system or component. Approaches that involve the construction of object-oriented or entity-relationship models require the expression of a particular kind of global invariant, concerning associations between objects or entities. This paper shows how association invariants can be expressed in a new, object-based formal language. It then explains how these expressions can be used to determine pre- and post-conditions for local operations, sufficient to ensure that the invariants are maintained. These conditions - and the program text to implement them - can be generated automatically. This makes it easier to produce correct implementations of an object-oriented design. © 2005 IEEE.

  • Teaching formal methods in context

    16 October 2018

    The Software Engineering Programme at Oxford teaches formal methods as an integral part of its programme of professional education in software engineering. This paper explains how the methods are taught - in the context of emerging trends in software development, and in the context of existing practice - and how their use is promoted through course design and motivating examples. © Springer-Verlag 2004.

  • Using state diagrams to describe concurrent behaviour

    16 October 2018

    The state diagram notation, a derivative of Harel's State-Charts, is an important component of the Unified Modeling Language (UML). It is the primary means of describing object behaviour: by associating a state diagram with a particular class, a designer may specify how objects of that class should perform sequences of actions in response to incoming events. This paper explains that, under the default interpretation, state diagrams are adequate only for designs in which: each object may admit at most one thread of execution; different threads of execution could never interfere; and it is impossible for an object to invoke an operation upon itself. The paper argues that these limitations are unsatisfactory. An alternative interpretation is then presented, in which separate diagrams are used to describe the object state and the transient, operation state. The resulting separation of concerns - between control flow and state abstraction - produces a simpler, more scalable approach to specification, and one that is adequate for the precise description of concurrent behaviour. © Springer-Verlag 2003.

  • Activity graphs and processes

    16 October 2018

    The widespread adoption of graphical notations for software design has created a demand for formally-based methods to support and extend their use. A principal focus for this demand is the Unified Modeling Language (UML), and, within UML, the diagrammatic notations for describing dynamic properties. This paper shows how one such notation, that of Activity Graphs, can be given a process semantics in the language of Communicating Sequential Processes (CSP). Such a semantics can be used to demonstrate the consistency of an object model and to provide a link to other methods and tools. A small example is included. © Springer-Verlag Berlin Heidelberg 2000.

  • Using relational and behavioural semantics in the verification of object models

    16 October 2018

    This paper shows how a combination of relational and behavioural semantics might be used in the creation and verification of object models. Specifications written in UML may be expressed in terms of abstract data types and processes; different notions of refinement may then be used to establish consistency between diagrams, or to verify that a design is faithful to the specification. © 2000 International Federation for Information Processing.

  • Concurrency and Refinement in the Unified Modeling Language

    16 October 2018

    This paper defines a formal semantics for a subset of the Unified Modeling Language (UML). It shows how suitable combinations of class, object, state, and sequence diagrams can be associated with patterns of interaction, expressed in the event notation of Communicating Sequential Processes (CSP). The diagram semantics is then extended to give a meaning to complete models - suitable combinations of diagrams - and thus a concurrency semantics for object models written in UML. This model semantics is in turn used to define a theory of refinement, based upon existing notions of data and process refinement.

  • Concurrency and refinement in the unified modeling language

    16 October 2018

    This paper shows how a formal notion of refinement may be defined for models, and model components, expressed in the Unified Modeling Language (UML). A formal, behavioural semantics is given to combinations of class, object, and state diagrams, using the notation of Communicating Sequential Processes (CSP); this semantics is adequate for the analysis of concurrent, communicating behaviour, and induces a notion of refinement for UML based upon existing notions of traces and failures refinement for CSP. © 2002 Published by Elsevier Science B. V.