@inproceedings{Davies*2009:Kathmandu,
abstract = "We report on the use of model-driven semantic technologies in support of a study into the effectiveness of paediatric vaccination against pneumococcal disease in Nepal.",
author = "Jim Davies, Jeremy Gibbons, Steve Harris, Jane Metz, Andrew J. Pollard, Matthew Snape",
booktitle = "Microsoft eScience Workshop",
month = "October",
title = "Model-Driven Support for a Vaccine Study in Kathmandu",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/vaccines.pdf",
year = "2009",
}
Warning - the bibtex entry below may be invalid:
Missing 'journal' field
@article{Crichton*2009:Model,
abstract = "The CancerGrid approach to clinical trials information systems is based on a metamodel developed from the CONSORT statement of best practice in reporting randomised controlled trials. The metamodel is instantiated with metadata elements drawn from a repository, to create a model of a particular clinical trial. The model is then used to derive automatically a trial management system customized for that trial: generating electronic case report forms, configuring randomisation and eligibility services, and parameterising the security subsystem. The key benefits of the approach are a uniform mechanism for trial registration and discovery, reduced cost and rapid implementation of information systems, and shared semantics leading to improved opportunities for meta-analysis. We describe our implementation of this approach, and outline two applications: for a breast cancer study in the UK, and for a rheumatoid arthritis study run by the US Veterans' Health Administration. ",
author = "Charles Crichton, Jim Davies, Jeremy Gibbons, Steve Harris, Andrew Tsui, James Brenton",
booktitle = "ICSE Workshop on Software Engineering and Health Care",
month = "May",
note = "To appear",
title = "Metadata-Driven Software for Clinical Trials",
url = "http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/consort.pdf",
year = "2009",
}
@inproceedings{Crichton*2009:Semantics,
abstract = "It has been argued that the challenges in electronic government are purely social: that existing methods and tools are perfectly adequate, and that electronic government projects fail because of people, not technology. While acknowledging that there are organisational and political challenges, this paper argues that there is also a significant,technical challenge, and a corresponding technology gap. It argues also that this challenge may be addressed through a combination of model-driven development and semantic technologies, and reports briefly upon a successful, prototypical application.",
address = "Hawaii",
author = "Charles Crichton, Jim Davies, Jeremy Gibbons, Steve Harris, Aadya Shukla, Andrew Tsui",
booktitle = "HICSS Workshop on Electronic Government",
month = "January",
title = "Semantics-Driven Development for Electronic Government Applications",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/hicss-sdd.pdf",
year = "2009",
}
@article{Davies&Gibbons2009:Formal,
abstract = "Interoperability is a key challenge in software engineering, whether expressed in terms of the compatibility of different systems and protocols, in terms of compliance to industry standards, or—increasingly—in terms of the ability to share and re-use data gathered in different contexts. Formal methods are mathematical techniques for the precise description of systems properties and behaviour, and have an important role to play in the future provision of interoperable systems and data. This paper describes that role, and examines the implications for present-day training and education.",
author = "Jim Davies and Jeremy Gibbons",
journal = "ACM Inroads",
month = "June",
note = "A revised version of "Formal Methods for Electronic Government" (FMET, 2008)",
number = "2",
pages = "60-64",
title = "Formal Methods for Future Interoperability",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/fmfi.pdf",
volume = "41",
year = "2009",
}
@inproceedings{Brenton*2008:Accelerating,
address = "Indianapolis, IN",
author = "James Brenton, Jim Davies, Jeremy Gibbons, Steve Harris",
booktitle = "Microsoft eScience Workshop",
month = "December",
title = "Accelerating Cancer Research Using Semantics-Driven Technology",
url = "http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/accelerating.pdf",
year = "2008",
}
@inproceedings{Davies*2008:Evolving,
address = "Indianapolis, IN",
author = "Jim Davies, Jeremy Gibbons, Steve Harris, Denise Warzel",
booktitle = "Microsoft eScience Workshop",
title = "Evolving Health Informatics: Semantic Frameworks and Metadata-Driven Architectures",
url = "http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/evolving.pdf",
year = "2008",
}
@inproceedings{ICEGOV2008STEG,
abstract = "Joined-up government depends fundamentally on semantics—on the computable representation of meaning, so that data is associated with appropriate metadata from the start, and this association is maintained as the data is manipulated. This paper summaries a tutorial and workshop on semantic technologies for supporting electronic government.",
address = "Cairo",
author = "Steve Harris and Jeremy Gibbons and Jim Davies and Andrew Tsui and Charles Crichton",
booktitle = "ICEGOV 2008",
editor = "Tomasz Janowski and Teresa Pardo",
month = "December",
pages = "45 -- 51",
publisher = "ACM Press",
title = "Semantic Technologies in Electronic Government",
url = "http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/semantech-egov.pdf",
year = "2008",
}
@inproceedings{Davies*2008:Metadata,
abstract = "Effective data sharing, across government agencies and other organisations, relies upon agreed meanings and representations. A key, technological challenge in electronic governance is to ensure that the meaning of data items is accurately recorded, and accessible in an economical—effectively, automatic—fashion. In response, a variety of data and metadata standards have been put forward: from government departments, from industry groups, and from organisations such as the ISO and W3C.
This paper shows how the leading standard for metadata registration—ISO11179—can be deployed without the need for a single, monolithic conceptualisation of the domain, and hence without the need for universal agreement upon a particular model of electronic governance. The advantages of this approach are discussed with regard to the UK eGovernment Interoperability Framework (eGIF) and the UK Integrated Public Sector Vocabulary (IPSV).",
address = "Cairo",
author = "Jim Davies, Steve Harris, Charles Crichton, Aadya Shukla, Jeremy Gibbons",
booktitle = "International Conference on Theory and Practice of Electronic Governance",
month = "December",
note = "Received a Best Paper Award",
title = "Metadata Standards for Semantic Interoperability in Electronic Government",
url = "http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/metadata-egov.pdf",
year = "2008",
}
@inproceedings{Zang*2008:WSRF,
abstract = "The CancerGrid consortium is developing open-standards cancer informatics to address the challenges posed by modern cancer clinical trials. This paper presents the service-oriented software paradigm implemented in CancerGrid to derive clinical trial information management systems for collaborative cancer research across multiple institutions. Our proposal is founded on a combination of a clinical trial (meta)model and WSRF (Web Services Resource Framework), and is currently being evaluated for use in early phase trials. Although primarily targeted at cancer research, our approach is readily applicable to other areas for which a similar information model is available.",
author = "Tianyi Zang and Radu Calinescu and Steve Harris and Andrew Tsui and Marta Kwiatkowska and Jeremy Gibbons and Jim Davies and Peter Maccallum and Carlos Caldas",
booktitle = "8th IEEE International Symposium on Cluster Computing (CCGrid)",
title = "WSRF-Based Modeling of Clinical Trial Information for Collaborative Cancer Research",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/wsrfmodeling.pdf",
year = "2008",
}
@article{sosym2008:davies,
abstract = "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.",
author = "James Welch and David Faitelson and Jim Davies",
doi = "10.1007/s10270-008-0085-0",
issn = "1619-1366",
journal = "Software and Systems Modeling ",
publisher = "Springer Berlin / Heidelberg",
title = "Automatic Maintenance of Association Invariants",
year = "2008",
}
@article{DBLP:journals/entcs/DaviesFW08,
author = "Jim Davies and David Faitelson and James Welch",
doi = "10.1016/j.entcs.2007.08.031",
journal = "Electronic Notes in Theoretical Computer Science",
pages = "151--170",
title = "Domain-specific Semantics and Data Refinement of Object Models",
volume = "195",
year = "2008",
}
@inbook{CalEtAl2007,
author = "Radu Calinescu and Steve Harris and Jeremy Gibbons and Jim Davies",
booktitle = "Innovations and Advanced Techniques in Computer and Information Sciences and Engineering",
editor = "Tarek Sobh",
pages = "385--390",
publisher = "Springer",
title = "Cross-Trial Query System for Cancer Clinical Trials",
year = "2007",
}
@inproceedings{Calinescu*2007:Model,
abstract = "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.",
author = "Radu Calinescu and Steve Harris and Jeremy Gibbons and Jim Davies and Igor Toujilov and Sylvia Nagl",
booktitle = "Software Engineering and Formal Methods",
doi = "10.1109/SEFM.2007.26",
month = "sep",
pages = "59-68",
title = "Model-Driven Architecture for Cancer Research",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/cgmda.pdf",
year = "2007",
}
@inproceedings{DBLP:conf/icegov/DaviesJOS07,
author = "Jim Davies and Tomasz Janowski and Adegboyega K. Ojo and Aadya Shukla",
booktitle = "First International Conference in the Theory and Practice of Electronic Government (ICEGOV) 2007",
doi = "10.1145/1328057.1328063",
pages = "5--11",
title = "Technological foundations of electronic governance",
year = "2007",
}
@inproceedings{DBLP:conf/icegov/CrichtonDGHS07,
abstract = "This paper explains how semantic frameworks can be used to support successful e-Government initiatives by connecting system design to a shared understanding of interactions and processes. It shows how metadata standards and repositories can be used to establish and maintain such an understanding, and how they can be used in the automatic generation and instantiation of components and services. It includes an account of a successful implementation at an international level, and a brief review of related approaches.",
author = "Charles Crichton and Jim Davies and Jeremy Gibbons and Steve Harris and Aadya Shukla",
booktitle = "First International Conference on Theory and Practice of Electronic Governance (ICEGOV) 2007",
doi = "10.1145/1328057.1328066",
editor = "Theresa Pardo and Tomasz Janowski",
month = "dec",
pages = "30--39",
publisher = "ACM",
title = "Semantic Frameworks for e-Government",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/sf-egov.pdf",
year = "2007",
}
@proceedings{Davies&Gibbons2007:Integrated,
booktitle = "Integrated Formal Methods",
editor = "Jim Davies and Jeremy Gibbons",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Integrated Formal Methods",
volume = "4591",
year = "2007",
}
@inproceedings{DBLP:journals/entcs/FaitelsonWD07,
abstract = "This paper explains how a declarative method language, based upon the formal notations of Z and B, can be used as a basis for automatic code generation. The language is used to describe the intended effect of operations, or methods, upon the components of an object model; each method is defined by a pair of predicates: a precondition, and a post-condition. Following the automatic incorporation of model invariants, including those arising from class associations, these predicates are extended--again, automatically--to address issues of consistency, definition, and dependency, before being translated into imperative programs. The result is a formal method for transforming object models into complete, working systems.",
author = "David Faitelson and James Welch and Jim Davies",
booktitle = "Proceedings of SBMF 2005",
doi = "10.1016/j.entcs.2007.03.021",
journal = "Electronic Notes in Theoretical Computer Science",
pages = "171--187",
publisher = "Electronic Notes in Theoretical Computer Science",
title = "From Predicates to Programs: The Semantics of a Method Language",
volume = "184",
year = "2007",
}
@inproceedings{DBLP:conf/IEEEares/LeslieDH06,
author = "Matthew Leslie and Jim Davies and Todd Huffman",
booktitle = "ARES",
doi = "10.1109/ARES.2006.108",
pages = "740-747",
publisher = "IEEE Computer Society",
title = "Replication Strategies for Reliable Decentralised Storage",
year = "2006",
}
@inproceedings{Davies*2006:Generation,
author = "Jim Davies and James Welch and Alessandra Cavarra and Edward Crichton",
booktitle = "Proceedings of the 11th IEEE Conference on the Engineering of Complex Computer Systems (ICECCS 2006)",
doi = "10.1109/ICECCS.2006.1690374",
publisher = "IEEE Computer Society",
title = "On the Generation of Object Databases using {B}ooster",
year = "2006",
}
@inproceedings{sbmf2006,
author = "Jim Davies and David Faitelson and James Welch",
booktitle = "Brazilian Symposium on Formal Methods (SBMF)",
title = "Domain-Specific Semantics and Data Refinement of Object Models",
year = "2006",
}
@article{Davies&Bolton2005:Singleton,
author = "Christie Bolton and Jim Davies",
journal = "Formal Aspects of Computing",
number = "2",
pages = "181-210",
title = "A Singleton Failures Semantics for {C}ommunicating {S}equential {P}rocesses",
volume = "18",
year = "2006",
}
@inproceedings{Welch*2005:Automatic,
author = "James Welch and David Faitelson and Jim Davies",
booktitle = "Proceedings of Software Engineering and Formal Methods (SEFM) 2005",
publisher = "IEEE Computer Society Press",
title = "Automatic Maintenance of Association Invariants",
year = "2005",
}
@article{DBLP:journals/entcs/DaviesCCNS05,
abstract = "This paper introduces an approach to software development in which a series of working implemen- tations are generated automatically from a series of formal specifications. The implementations are data stores, communicating through standard protocols. The specifications are precise object models, in which operations are described in terms of pre- and post-conditions. The approach is evolutionary, in the sense that the specification may evolve while the system is in use, in response to changes in requirements, and any changes to the specification are automatically reflected in the structure of the implementation, and in the representation of any data currently stored.",
author = "Jim Davies and Charles Crichton and Edward Crichton and David Neilson and Ib Holm S{\o}rensen",
doi = "10.1016/j.entcs.2005.03.004",
journal = "Electronic Notes in Theoretical Computer Science",
pages = "39-55",
title = "Formality, Evolution, and Model-driven Software Engineering",
volume = "130",
year = "2005",
}
@inproceedings{Brenton*2005:CancerGrid,
author = "James Brenton and Carlos Caldas and Jim Davies and Steve Harris and Peter Maccallum",
booktitle = "All Hands Meeting",
title = "{CancerGrid}: Developing Open Standards for Clinical Cancer Informatics",
year = "2005",
}
@article{DBLP:journals/infsof/Cavarra,
abstract = "This paper shows how object-oriented specifications, written in the Unified Modeling Language (UML) can be translated into formal, behavioural descriptions and used as a basis for automatic test generation. The behavioural descriptions are written in a language of communicating state machines: the Intermediate Format (IF). The translation from UML to IF is based upon an earlier formal semantics, written in the Abstract State Machine (ASM) notation. Descriptions written in IF can be automatically explored; the results of these explorations are test trees, ready for input to a variety of testing packages.",
author = "Alessandra Cavarra and Charles Crichton and Jim Davies",
doi = "10.1016/j.infsof.2003.09.004",
journal = "Information {\&} Software Technology",
number = "5",
pages = "309-314",
title = "A Method for the Automatic Generation of Test Suites from Object Models",
volume = "46",
year = "2004",
}
@proceedings{DBLP:conf/icfem/2004,
booktitle = "Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings",
editor = "Jim Davies and Wolfram Schulte and Michael Barnett",
isbn = "3-540-23841-7",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
title = "Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings",
volume = "3308",
year = "2004",
}
@inproceedings{DBLP:conf/tfm/DaviesSM04,
author = "Jim Davies and Andrew Simpson and Andrew Martin",
crossref = "",
pages = "185-202",
title = "Teaching Formal Methods in Context",
url = "http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3294{\&}spage=185",
year = "2004",
booktitle = "Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18-19, 2004, Proceedings",
editor = "C. Neville Dean and Raymond T. Boute",
isbn = "3-540-23611-2",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
booktitle = "Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18-19, 2004, Proceedings",
volume = "3294",
year = "2004",
}
@inproceedings{DBLP:conf/icse/SimpsonMGDM03,
author = "Andrew Simpson and Andrew Martin and Jeremy Gibbons and Jim Davies and Steve McKeever",
crossref = "",
pages = "628-633",
title = "On The Supervision and Assessment Of Part-Time Postgraduate Software Engineering Projects",
url = "http://computer.org/proceedings/icse/1877/18770628abs.htm",
year = "2003",
booktitle = "Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA",
publisher = "IEEE Computer Society",
booktitle = "Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA",
year = "2003",
}
@inproceedings{DBLP:conf/sac/DaviesCC03,
abstract = "This paper explains how object models written in the Unified Modeling Language (UML) can be translated into formal, behavioural descriptions and used as a basis for automatic test generation. The behavioural descriptions are written in a language of communicating state machines: the Intermediate Format (IF). The translation from UML to IF is based upon an earlier formal semantics, written in the Abstract State Machine (ASM) notation. Descriptions written in IF can be automatically explored; the results of these explorations are test trees, ready for input to a variety of testing packages.",
author = "Jim Davies and Charles Crichton and Alessandra Cavarra",
booktitle = "Proceedings of the 2003 ACM Symposium on Applied Computing (SAC), March 9-12, 2003, Melbourne, FL, USA",
crossref = "",
doi = "10.1145/952532.952748",
pages = "1104-1109",
publisher = "ACM",
title = "A Method for the Automatic Generation of Test Suites from Object Models",
year = "2003",
}
@article{DBLP:journals/fac/DaviesC03,
abstract = "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.",
author = "Jim Davies and Charles Crichton",
doi = "10.1007/s00165-003-0008-3",
journal = "Formal Aspects of Computing",
number = "2-3",
pages = "118-145",
publisher = "Springer London",
title = "Concurrency and Refinement in the Unified Modeling Language",
volume = "15",
year = "2003",
}
@inproceedings{DBLP:conf/icfem/DaviesC03,
abstract = "The state diagram notation, a derivative of Harel's StateCharts, 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.",
author = "Jim Davies and Charles Crichton",
booktitle = "5th International Conference on Formal Engineering Methods, ICFEM 2003",
copyright = "2003",
crossref = "",
doi = "10.1007/b94115",
editor = "Jin Song Dong and Jim Woodcock",
isbn = "978-3-540-20461-9",
issn = "1611-3349",
pages = "105-124",
publisher = "Springer Berlin / Heidelberg",
title = "Using State Diagrams to Describe Concurrent Behaviour",
volume = "2885/2003",
year = "2003",
}
@article{DBLP:journals/entcs/DaviesC02,
abstract = "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.",
author = "Jim Davies and Charles Crichton",
booktitle = "REFINE 2002, The BCS FACS Refinement Workshop (Satellite Eventof FLoC 2002)",
doi = "10.1016/S1571-0661(05)80494-3",
journal = "Electronic Notes in Theoretical Computer Science",
number = "3",
pages = "217-243",
title = "Concurrency and Refinement in the Unified Modeling Language",
volume = "70",
year = "2002",
}
@article{DBLP:journals/entcs/BoltonD02,
author = "Christie Bolton and Jim Davies",
journal = "Electronic Notes in Theoretical Computer Science",
number = "3",
title = "A comparison of refinement orderings and their associated simulation rules",
url = "http://www.elsevier.com/gej-ng/31/29/23/125/48/show/Products/notes/index.htt\#010",
volume = "70",
year = "2002",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/ifm/BoltonD02,
author = "Christie Bolton and Jim Davies",
crossref = "",
pages = "225-244",
title = "Refinement in {O}bject-{Z} and {CSP}",
url = "http://link.springer.de/link/service/series/0558/bibs/2335/23350225.htm",
year = "2002",
}
@book{Davies*2000:Millenial,
booktitle = "Millennial Perspectives in Computer Science",
editor = "J. Davies and A. Roscoe and J. Woodcock",
publisher = "Palgrave",
title = "Millennial Perspectives in Computer Science",
year = "2000",
}
Warning - the bibtex entry below may be invalid:
Missing 'chapter' or 'pages' field
Missing 'publisher' field
@inbook{Woodcock*2000:Abstract,
author = "J. Woodcock and J. Davies and C. Bolton",
crossref = "",
title = "Abstract data types and Processes",
year = "2000",
}
@inproceedings{DBLP:conf/ifm/BoltonD00,
author = "Christie Bolton and Jim Davies",
crossref = "",
pages = "77-96",
title = "Activity Graphs and Processes",
url = "http://link.springer.de/link/service/series/0558/bibs/1945/19450077.htm",
year = "2000",
booktitle = "Integrated Formal Methods, Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1-3, 2000, Proceedings",
editor = "Wolfgang Grieskamp and Thomas Santen and Bill Stoddart",
isbn = "3-540-41196-8",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
booktitle = "Integrated Formal Methods, Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1-3, 2000, Proceedings",
volume = "1945",
year = "2000",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/fmoods/BoltonD00,
author = "Christie Bolton and Jim Davies",
crossref = "",
pages = "163-182",
title = "Using Relational and Behavioural Semantics in the Verification of Object Models",
year = "2000",
}
@proceedings{DBLP:conf/fm/1999-2,
booktitle = "World Congress on Formal Methods",
editor = "Jeannette M. Wing and Jim Woodcock and Jim Davies",
isbn = "3-540-66588-9",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
title = "FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II",
volume = "1709",
year = "1999",
}
@proceedings{DBLP:conf/fm/1999-1,
booktitle = "World Congress on Formal Methods",
editor = "Jeannette M. Wing and Jim Woodcock and Jim Davies",
isbn = "3-540-66587-0",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
title = "FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I",
volume = "1708",
year = "1999",
}
@article{DBLP:journals/dc/LoweD99,
author = "Gavin Lowe and Jim Davies",
journal = "Distributed Computing",
number = "2-3",
pages = "91-103",
title = "Using {CSP} to Verify Sequential Consistency",
url = "http://link.springer.de/link/service/journals/00446/bibs/9012002/90120091.htm",
volume = "12",
year = "1999",
}
@inproceedings{Crichton*1999:When,
author = "Charles Crichton and Jim Davies and Jim Woodcock",
booktitle = "Proceedings of TOOLS",
doi = "10.1109/TOOLS.1999.787541",
title = "When to Trust Mobile Objects: Access Control in the {J}ini Software System",
year = "1999",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/ifm/BoltonDW99,
author = "Christie Bolton and Jim Davies and Jim Woodcock",
crossref = "",
pages = "273-292",
title = "On the Refinement and Simulation of Data Types and Processes",
year = "1999",
}
@inproceedings{Simpson*1998:Safety,
author = "A. Simpson and J. Woodcock and J. Davies",
booktitle = "Proceedings of the Ninth International Workshop on Software Specification and Design",
publisher = "IEEE Press",
title = "Safety through Security",
year = "1998",
}
@inproceedings{Simpson*1997:Mechanical,
author = "A. Simpson and J. Woodcock and J. Davies",
booktitle = "Proceedings of Formal Methods Pacific",
publisher = "Springer",
title = "The Mechanical Verification of Solid State Interlocking Geographic Data",
year = "1997",
}
@book{Woodcock&Davies96:Using,
author = "J. Woodcock and J. Davies",
publisher = "Prentice Hall International",
title = "Using {Z}: Specification, Refinement, and Proof",
year = "1996",
}
@article{DBLP:journals/tcs/DaviesS95,
author = "Jim Davies and Steve Schneider",
journal = "Theoretical Computer Science",
number = "2",
pages = "243-271",
title = "A Brief History of Timed {CSP}",
url = "http://dx.doi.org/10.1016/0304-3975(94)00169-J",
volume = "138",
year = "1995",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/forte/DaviesBS95,
author = "Jim Davies and Jeremy Bryans and Steve Schneider",
crossref = "",
pages = "383-397",
title = "Real-time {LOTOS} and Timed Observations",
year = "1995",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/concur/BryansDS95,
author = "Jeremy Bryans and Jim Davies and Steve Schneider",
crossref = "",
pages = "269-283",
title = "Towards a denotational semantics for {ET-LOTOS}",
year = "1995",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/forte/DaviesW94,
author = "Jim Davies and Matt Wallis",
crossref = "",
pages = "100-115",
title = "On the formal specification and verification of network routing algorithms",
year = "1994",
}
@article{DBLP:journals/fac/DaviesS94,
author = "Jim Davies and Steve Schneider",
journal = "Formal Aspects of Computing",
number = "6",
pages = "530-553",
title = "Recursion Induction for Real-Time Processes",
volume = "5",
year = "1994",
}
Warning - the bibtex entry below may be invalid:
Missing 'chapter' or 'pages' field
@inbook{Davies&Schneider1994:Realtime,
author = "J. Davies and S. Schneider",
booktitle = "Theories and Experiences for Real-time Systems",
publisher = "World Scientific",
title = "Real-time {CSP}",
year = "1994",
}
@book{Davies1993:Specification,
author = "J. Davies",
publisher = "Cambridge University Press",
title = "Specification and Proof in Real-time {CSP}",
year = "1993",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/concur/DaviesS92,
author = "Jim Davies and Steve Schneider",
crossref = "",
pages = "355-369",
title = "Using {CSP} to Verify a Timed Protocol over a Fair Medium",
year = "1992",
}
@inproceedings{DBLP:conf/ftrtft/DaviesJS92,
author = "Jim Davies and Dave Jackson and Steve Schneider",
crossref = "",
pages = "149-169",
title = "Broadcast Communication for Real-time Processes",
year = "1991",
booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems, Second International Symposium, Nijmegen, The Netherlands, January 8-10, 1992, Proceedings",
editor = "Jan Vytopil",
isbn = "3-540-55092-5",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems, Second International Symposium, Nijmegen, The Netherlands, January 8-10, 1992, Proceedings",
volume = "571",
}
@inproceedings{DBLP:conf/rex/SchneiderDJRRR91,
author = "Steve Schneider and Jim Davies and D. M. Jackson and George M. Reed and Joy N. Reed and A. W. Roscoe",
crossref = "",
pages = "640-675",
title = "Timed {CSP}: Theory and Practice",
year = "1992",
booktitle = "Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 3-7, 1991, Proceedings",
editor = "J. W. de Bakker and Cornelis Huizing and Willem P. de Roever and Grzegorz Rozenberg",
isbn = "3-540-55564-1",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
booktitle = "Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 3-7, 1991, Proceedings",
volume = "600",
}
Warning - the bibtex entry below may be invalid:
Missing 'booktitle' field
@inproceedings{DBLP:conf/mfps/DaviesS89,
author = "Jim Davies and Steve Schneider",
crossref = "",
pages = "129-159",
title = "Factorizing Proofs in Timed {CSP}",
year = "1989",
}
@inproceedings{Davies&Schneider1989:Factorising,
author = "J. Davies and S. Schneider",
booktitle = "Real-Time Systems: Theory and Practice",
publisher = "North-Holland",
title = "Factorising Proofs in Timed {CSP}",
year = "1989",
}