Provably Correct Business Rules and Processes (PCBRP)

Provably Correct Business Rules and Processes (PCBRP) is a project of the Software System Research Group (SSRG).

Overview

Aim: Innovative technology for combined business rules and business process modelling
Application and Benefit: We intend to support multiple phases in the software life cycle:
- Analysis of business rules for logical errors: identifying inconsistencies, redundancies and omissions. Absence of logical errors is a fundamental property.
- Life-cycle management: what-if reasoning and test-case generation to support business rules and process maintenance under change.
- Model-checking: validating business models on concrete runtime scenarios. This way, business rules and process models can be debugged early in the development cycle prior to implementation.
- Business process compliance: validating business processes on business rules. Compliance checking at design time is useful for debugging business process models; compliance monitoring at runtime allows the checking of concrete execution paths and their possible continuations.
- Business logic automation: adopting a declarative approach to business process modeling via business rules and process fragments enables more flexible execution planning than with traditional business process models.
Approach: Our approach rests on the folllowing three guidelines:
- Semantic Technologies: business models that contain logical errors or do not faithfully model the business are of little use. Our approach is grounded in mathematical logic to provide a firm semantical basis and expressive knowledge representation language.
- Automation: in order to cut development costs and raise acceptance with non-technical users it is crucial to provide as much automation of these semantic technologies as possible. We are applying and developing a variety of corresponding automated reasoning methods.
- Compatibility: to gain acceptance in practice, it is important to provide interfaces through established technologies, such as BPMN and SBVR.

Activity

We focus on developing a new approach for business modelling, which is characterized as follows.

Expressiveness:
```
     Business Model = Rules + Processes + Data
```
Business rules and processes modelling are treated on a par, in a complementary way. Rich data types are supported for faithfully modelling data.

The diagram on the right illustrates that with a small fragment of a travel approval process.
Flexibility: We deviate from traditional BPMN-style modelling by offering process fragments as building blocks for bigger processes. Together with business rules for describing constraints and applicability conditions this supports flexible configuration of full process models in a concise way. Applications are for static analysis and for run-time process execution planning.
The BPMN-diagram on the right is derived from the fragments above as one possible configuration.
Declarativity and Reasoning Support:
Our formalisms are grounded in mathematical-logical foundations, such as first-order logic and temporal logic. Our tools implements novel combinations and extension of corresponding automated reasoning methods. They support, among others, the following tasks:
- Rules analysis (consistency, redundancy, completeness)
- Executing the model, from concrete or symbolic data
- (Dis)proving temporal properties, e.g. safety
- Planning from process fragments and rules
Natural Language Front-End: To support a case study in collaboration with NSW LPI on Land Conveyancing we have developed a controlled natural-language front-end for a suitable fragment of SBVR.
This allows us to represent in first-order logic sentences like

The Land Title Reference specified in each Subject Land Title in each eRegistry Instrument must be the same as the Land Title Reference specified in some of the CoRD/CT Details in the eLodgment Information Report included in the eLodgment Case that includes that eRegistry Instrument.