Property Specifications for Workflow Modelling
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...
| Päätekijät: | , |
|---|---|
| Aineistotyyppi: | Conference item |
| Julkaistu: |
2009
|
| _version_ | 1826290400324747264 |
|---|---|
| author | Wong, P Gibbons, J |
| author_facet | Wong, P Gibbons, J |
| author_sort | Wong, P |
| collection | OXFORD |
| description | 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 use it to construct behavioural properties against which BPMN models may be verified. This paper considers a pattern-based approach to expressing behavioural properties. We describe a property specification language PL for capturing a generalisation of Dwyer et al.'s Property Specification Patterns, and present a translation from PL 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. © Springer-Verlag Berlin Heidelberg 2009. |
| first_indexed | 2024-03-07T02:43:36Z |
| format | Conference item |
| id | oxford-uuid:ab47875a-e2a8-4081-861d-501d837f556c |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:43:36Z |
| publishDate | 2009 |
| record_format | dspace |
| spelling | oxford-uuid:ab47875a-e2a8-4081-861d-501d837f556c2022-03-27T03:20:57ZProperty Specifications for Workflow ModellingConference itemhttp://purl.org/coar/resource_type/c_5794uuid:ab47875a-e2a8-4081-861d-501d837f556cSymplectic Elements at Oxford2009Wong, PGibbons, JPreviously 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 use it to construct behavioural properties against which BPMN models may be verified. This paper considers a pattern-based approach to expressing behavioural properties. We describe a property specification language PL for capturing a generalisation of Dwyer et al.'s Property Specification Patterns, and present a translation from PL 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. © Springer-Verlag Berlin Heidelberg 2009. |
| spellingShingle | Wong, P Gibbons, J Property Specifications for Workflow Modelling |
| title | Property Specifications for Workflow Modelling |
| title_full | Property Specifications for Workflow Modelling |
| title_fullStr | Property Specifications for Workflow Modelling |
| title_full_unstemmed | Property Specifications for Workflow Modelling |
| title_short | Property Specifications for Workflow Modelling |
| title_sort | property specifications for workflow modelling |
| work_keys_str_mv | AT wongp propertyspecificationsforworkflowmodelling AT gibbonsj propertyspecificationsforworkflowmodelling |