@misc{ifmextend,
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  note = "Extended version. Submitted for publication.",
  title = "Property Specifications for Workflow Modelling",
  year = "2009",
}


    
      @article{bpmn09,
  abstract = "We present two formalisations of the Business Process Modelling Notation (BPMN). In particular, we introduce a semantic model for BPMN in the process algebra CSP; we then study an augmentation of this model in which we introduce relative timing information, allowing one to specify timing constraints on concurrent activities. By exploiting CSP refinement, we are able to show some relationships between the timed and the untimed models. We then describe a novel empirical studies model, and the transformation to BPMN, allowing one to apply our formal semantics for analysing different kind of workflows. To provide a better facility for describing behaviour specification about a BPMN diagram, we also present a pattern-based approach using which a workflow designer could specify properties which could otherwise be difficult to express. Our approach is specifically designed to allow behavioural properties of BPMN diagrams to be mechanically verified via automatic model-checking as provided by the FDR tool. We use two examples to illustrate our approach.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  doi = "10.1016/j.scico.2009.09.010",
  journal = "Science of Computer Programming",
  month = "sep",
  note = "Special issue on FOCLASA 2008",
  title = "Formalisations and Applications of BPMN",
  year = "2009",
}


    
      @inproceedings{pattern,
  abstract = "Previously we provided two formal behavioural semantics for Business Process Modelling Notation (BPMN) in the process algebra CSP. By exploiting CSP's refinement orderings, developers may formally compare their BPMN models. However, BPMN is not a specification language, and it is difficult and sometimes impossible to construct behavioural properties against which BPMN models may be verified. This paper considers a pattern-based approach for capturing these behavioural properties. We describe a property specification language <em>PL</em> for capturing a generalisation of Dwyer et al.'s Property Specification Patterns, and present a translation from <em>PL</em> into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP for simple refinement checking. We demonstrate its application via a simple example.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 7th International Conference on Integrated Formal Methods",
  doi = "10.1007/978-3-642-00255-7_5",
  month = "February",
  note = "Invited for special issue in Science of Computer Programming. Technical report version available at \url{http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/psp.pdf}",
  series = "LNCS",
  title = "Property Specifications for Workflow Modelling",
  volume = "5423",
  year = "2009",
}


    
      @unpublished{confirm,
  author = "Peter Y. H. Wong",
  note = "Confirmation of Status Report",
  school = "Computing Laboratory, University of Oxford",
  title = "{Formalisations and Applications of Business Process Modelling Notation}",
  year = "2008",
}


    
      @inproceedings{qsic2008,
  abstract = "We describe a process-algebraic approach to verifying process interactions for business collaboration described in Business Process Modelling Notation. We first overview our process semantics for BPMN in the language of Communicating Sequential Processes; we then use a simple example of business collaboration to demonstrate how our semantic model may be used to verify compatibility between business participants in a collaboration, and we also discuss some theoretical results.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 8th International Conference on Quality Software.",
  doi = "10.1109/QSIC.2008.6",
  month = "August",
  note = "Preliminary versions were presented at 3rd International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems and 2nd European Young Researchers Workshop on Service Oriented Computing, June 2007",
  pages = "126-131",
  publisher = "IEEE Computer Society",
  title = "{Verifying Business Process Compatibility}",
  url = "http://www.comlab.ox.ac.uk/peter.wong/pub/qsic2008.pdf",
  year = "2008",
}


    
      @inproceedings{bpmn-time,
  abstract = "We describe a relative-timed semantic model for Business Process Modelling Notation (BPMN). We define the semantics in the language of Communicating Sequential Processes (CSP). This model augments our untimed model by introducing the notion of relative time in the form of delays chosen non-deterministically from a range. We illustrate the application by an example. We also show some properties relating the timed semantics and BPMN's untimed process semantics by exploiting CSP refinement. Our timed semantics allows behavioural properties of BPMN diagrams to be mechanically verified via automatic model-checking as provided by the FDR tool.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 7th International Workshop on the Foundations of Coordination Languages and Software Architectures.",
  doi = "10.1016/j.entcs.2009.06.029",
  month = "July",
  note = "Invited for special issue in Science of Computer Programming. A shorter version of this paper was presented at the 3rd European Young Researchers Workshop on Service Oriented Computing, London, United Kingdom, June 2008. Extended version available at \url{http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmntime.pdf}.",
  series = "ENTCS",
  title = "{A Relative Timed Semantics for BPMN}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/foclasa2008.pdf",
  volume = "229",
  year = "2008",
}


    
      @inproceedings{transform,
  abstract = "In this paper we describe a graphical approach for formally specifying temporally-ordered activity routines designed for calendar scheduling. We introduce a workflow model \emph{OWorkflow}, for constructing specifications of long running empirical studies such as clinical trials in which observations for gathering data are performed at strict specific times. These observations, either manually performed or automated, are often interleaved with scientific procedures, and their descriptions are recorded in a calendar for scheduling and monitoring to ensure each observation is carried out correctly at a specific time. We also describe a bidirectional transformation between \emph{OWorkflow} and Business Process Modelling Notation (BPMN) diagrams, by which graphical specification, simulation, automation and formalisation are made possible.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 1st International Conference on Model Transformation (Theory and Practice of Model Transformations)",
  doi = "10.1007/978-3-540-69927-9_6",
  month = "July",
  note = "Extended version available at \url{http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/transext.pdf}.",
  series = "LNCS",
  title = "{On Specifying and Visualising Long-Running Empirical Studies.}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/icmt2008.pdf",
  volume = "5063",
  year = "2008",
}


    
      @inproceedings{bpmn-csp,
  abstract = "Business Process Modelling Notation (BPMN), developed by the Business Process Management Initiative (BPMI), intends to bridge the gap between business process design and implementation. However, the specification of the notation does not include a formal semantics. This paper shows how a subset of the BPMN can be given a process semantics in Communicating Sequential Processes. Such a semantics allows developers to formally analyse and compare BPMN diagrams. A simple example of a business process is included.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 10th International Conference on Formal Engineering Methods.",
  doi = "10.1007/978-3-540-88194-0_22",
  month = "October",
  note = "Extended version available at \url{http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmnsem.pdf}.",
  series = "LNCS",
  title = "{A Process Semantics for BPMN}",
  volume = "5256",
  year = "2008",
}


    
      @unpublished{transfer,
  author = "Peter Y.H. Wong",
  note = "Transfer Dissertation.",
  school = "Computing Laboratory, University of Oxford",
  title = "{Towards BPM-based Support for Clinical Trials}",
  year = "2007",
}


    
      @inproceedings{workflow,
  abstract = "This paper describes a process algebraic approach to specification and refinement of workflow processes. In particular, we model both specification and implementation of workflows as CSP processes. CSP's behavioural models and their respective refinement relations not only enable us to prove correctness properties of an individual workflow process against its behavioural specification, but also allows us to design and develop workflow processes compositionally. Moreover, coupled with CSP is an industrial strength automated model checker FDR, which allows behavioural properties of workflow models to be proved automatically. This paper details some CSP models of van der Aalst et al.'s control flow workflow patterns, and illustrates behavioural specification and refinement of workflow systems with a business process scenario.",
  author = "Peter Y. H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 6th International Symposium on Software Composition",
  doi = "10.1007/978-3-540-77351-1_5",
  month = "March",
  series = "LNCS",
  title = "{A Process-Algebraic Approach to Workflow Specification and Refinement}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/sc2007.pdf",
  volume = "4829",
  year = "2007",
}


    
      @inproceedings{sosornet,
  abstract = "In workflow management, one of the key challenges is to provide a formal semantics to workflow specification and to unify workflow coordination at both orchestration and choreography levels. This paper describes the formalisation of workflow processes using the process algebra CSP. We presents the formalisaton of van der Aalst et al.'s twenty control flow workflow patterns. A business process scenario, focusing on orchestration and choreography, is examined. The result of the case study is a CSP model which gives precise semantics to both static and dynamic control flows of the business processes orchestrations and choreographies. CSP's behavioural models and their respective refinement relations make it suitable for modelling complex services orchestration and choreography. Moreover, coupled with CSP is an industrial strength automated model checker FDR, which gives CSP an advantage over other process algebras in automatic verification.",
  address = "Manchester, United Kingdom",
  author = "Peter Y. H. Wong",
  booktitle = "1st Service-Oriented Software Research Network (SOSoRNet) Workshop",
  month = "June",
  title = "{Towards A Unified Model for Workflow Processes}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/model_abstract.pdf",
  year = "2006",
}


    
      @mastersthesis{msc,
  abstract = "The rapid development in the capability of hardware components of computational systems has led to a significant increase in the energy consumption of these computational systems. This has become a major issue especially if the computational environment is either resource-critical or resource-limited. Hence it is important to understand the energy consumption within these environments. This thesis describes an investigatory approach to power analysis and documents the development of an energy consumption analysis technique at the application level, and the implementation of the Power Trace Simulation and Characterisation Tools Suite (PSim). PSim uses a program characterisation technique which is inspired by the Performance Application Characterisation Environment (PACE), a performance modelling and prediction framework for parallel and distributed computing.",
  address = "United Kingdom",
  author = "Peter Y. H. Wong",
  month = "February",
  school = "University of Warwick",
  title = "{An Investigation in Energy Consumption Analyses and Application-Level Prediction Techniques}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/msc.pdf",
  year = "2006",
}


    
      @inproceedings{crlIspa,
  abstract = "This paper introduces an XML-based generic Context Request Language (CRL), whose construction is part of a web services framework in the domain of mobile context sensing. The paper describes an implementation of the technique that is in accordance with the formal mathematical representational model, using first-order temporal language [6]. The language is an attempt to introduce intelligence into context-aware computing by defining context-sensing elements into logical entities. The use of first-order calculus in this language definition serving on web service technology allows users to utilize context aggregation and to embed user control in contextual information. By carrying out on-the-fly context inferences at the middleware level, we can achieve a complete separation of concerns between user application and context sensing. Moreover, the declaration of contextual knowledge based on situations and events within the predicate domain allows users to express changes in contextual information and to quantify these elements among times and durations.",
  address = "Hong Kong, China",
  author = "Alvin T.S. Chan and Peter Y.H. Wong and Siu Nam Chuang",
  booktitle = "Proceedings of 2nd International Symposium on Parallel and Distributed Processing and Applications",
  month = "December",
  series = "LNCS",
  title = "{CRL: A Context-aware Request Language for Mobile Computing}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/crlIspa.pdf",
  volume = "3358",
  year = "2004",
}


    
      @unpublished{bsc,
  abstract = "A performance prediction system (PACE - Performance Analysis Characterisation Environment) has been implemented to characterise the performance of C, Fortran and Mathematica codes. With the current increase in the popularity of the Java platform, PACE is being extended to characterise and predict distributed Java applications within dynamic heterogeneous environments. With the modern implementations of the Java Virtual Machine being able to carry out on-the-fly optimisations, Java methods are to be characterised as a control flow of bytecode blocks, rather than individual bytecodes. These bytecode blocks are then benchmarked to create a bank of predictive data for evaluating performance critical Java applications. This report describes the implementation of defining and monitoring these bytecode blocks and also evaluates the techniques that have been used.",
  address = "United Kingdom",
  author = "Peter Y. H. Wong",
  month = "July",
  note = "Bachelor Final Year Project Report.",
  school = "University of Warwick",
  title = "{Bytecode Monitoring of Java Programs}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/project.pdf",
  year = "2003",
}