| EPSRC Reference: |
GR/N35076/01 |
| Title: |
ADDING REFINEMENTS TO THE PRODUCT/PROCESS MODELLING LOGIC |
| Principal Investigator: |
Maibaum, Professor T |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Kings College London |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
15 March 2000 |
Ends: |
14 March 2001 |
Value (£): |
4,100
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The overall aim of this research is to provide a formal language in which to model business processes, including the virtual processes used in electronic commerce. The language supports the Mensurae method for formal description of processes, understood here as referrring to the technical and administrative activities of organisations. As such, it provides abstractions for the two main constructs of the method: products and processes. We associate a notion of refinement with specifications, allowing us to demonstrate that a process satisfies its specification. We conceptualize this relationship as being defined via a simple substitution notion for relational variables (representing abstract processes being concretized via relational expressions), accompanied by semantic conditions guaranteeing feasibility (preserving the implementability of the abstract specification over the underlying abstract machine). Process specifications are formulae in our logic in which realational variables, standing for processes may appear. Such a relational variable is said to be feasible if it can be realized over the abstract machine by substituting for it a ground term over the language of the abstract machine, representing a program executable on it. A refinement of the relational variable in the context of the formula is a relational term, not necessarily ground, which preserves this feasibility. The weakest precondition idea is adapted to give the basics of a method for finding refinements, rather than having to prove correctness for a substitution post facto.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
|