This page contains information about:
Model Checking BPMNModelling of business processes and workflows is an important area in software engineering. BPMN allows developers to take a process-oriented approach to modelling of systems. We have defined two semantic models (an untimed process semantics and a relative timed semantics) for this notation over the domain CSP. These semantic models allow BPMN diagrams to be formally analysed and compared. In particular, verifications can now be carried out against properties such as consistency and compatibility between business processes specified in BPMN via the FDR tool. This page contains a prototypical Haskell implementation of the semantic functions from BPMN to machine-readable CSP. Empirical Studies
We have developed a declarative model Empiricol 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. This page contains information about the Haskell implementation of the bidirectional transformation between this model and a subset of BPMN, by which graphical specification, simulation, automation and formalisation are made possible. Property Specification for BPMNWhile by exploiting CSP's refinement orderings business process developers may formally compare their BPMN models. BPMN is not a specification language and it is difficult and sometime impossible to construct behavioural properties against which BPMN models may be verified. This paper consider a pattern-based approach for capturing these behavioural properties. We have defined a property specification language PL for capturing a generalisation of Dwyer et al.'s Property Specification Patterns and a corresponding translation from PL into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP specification for simple refinement checking. Source Codeto be added...
Manualto be added...Literatures Doctorate (DPhil) Thesis
Journal Publications
Conference and Workshop Publications
|