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.
  • 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.

  • A comparison or refinement orderings and their associated simulation rules

    16 October 2018

    In this paper we compare the refinement orderings, and their associated simulation rules, of state-based specification languages such as Z and Object-Z with the refinement orderings of event-based specification languages such as CSP. We prove with a simple counter-example that data refinement, established using the standard simulation rules for Z, does not imply failures refinement in CSP. This contradicts accepted results. Having explored the differences between the simulation rules for establishing data refinement and those for establishing the refinement of action systems and state-transition systems - models in which refinement is equivalent to failures refinement within CSP - we present a new set of simulation rules for data types. These alternative rules are both sound and jointly complete with respect to the stable failures refinement ordering. Furthermore we present an alternative refinement ordering for CSP, one in which refinement is equivalent to data, refinement in Z. © 2002 Published by Elsevier Science B. V.

  • Mutational signatures in esophageal adenocarcinoma define etiologically distinct subgroups with therapeutic relevance.

    16 October 2018

    Esophageal adenocarcinoma (EAC) has a poor outcome, and targeted therapy trials have thus far been disappointing owing to a lack of robust stratification methods. Whole-genome sequencing (WGS) analysis of 129 cases demonstrated that this is a heterogeneous cancer dominated by copy number alterations with frequent large-scale rearrangements. Co-amplification of receptor tyrosine kinases (RTKs) and/or downstream mitogenic activation is almost ubiquitous; thus tailored combination RTK inhibitor (RTKi) therapy might be required, as we demonstrate in vitro. However, mutational signatures showed three distinct molecular subtypes with potential therapeutic relevance, which we verified in an independent cohort (n = 87): (i) enrichment for BRCA signature with prevalent defects in the homologous recombination pathway; (ii) dominant T>G mutational pattern associated with a high mutational load and neoantigen burden; and (iii) C>A/T mutational pattern with evidence of an aging imprint. These subtypes could be ascertained using a clinically applicable sequencing strategy (low coverage) as a basis for therapy selection.

  • Automatic maintenance of association invariants

    16 October 2018

    Many approaches to software specification and design make use of invariants: constraints whose truth is preserved under operations on a system or component. Object modelling involves the definition of association invariants: constraints upon the sets of links corresponding to particular associations, most often concerning type, multiplicity, or symmetry. This paper shows how the definitions of operations may be extended to take account of association invariants, so that they may be properly considered when the operations are implemented. It introduces a formal, object-based modelling notation in which the process of extension and implementation, and thus the maintenance of association invariants, can be automated, making it easier to produce correct implementations of an object-oriented design. © Springer-Verlag 2008.