Industrial deployment of system engineering methods providing high dependability and productivity


About Deploy Project


Workpackage 4 ó Deployment in the business information sector

Motivation and context.

Business information systems are characterised by operating with huge sets of data, with a strong focus on maintaining data consistency throughout the lifetime of business objects, such as an order, a delivery, or an invoice.

The use of formal methods in this sector is not widespread as business software is usually not considered to be safety critical, in contrast, e.g., to systems in the traffic sector. In some areas of business software, an economically optimal defect rate greater than zero has been acceptable, especially since the software has undergone an adaptation phase at the customer site anyway, where relevant flaws could be fixed by consultants. This is different from sectors like the space sector where this is impossible. Finally, the system size of business applications is usually much larger than in other areas; this fact makes the application of formal methods more difficult for scalability reasons.

For the above reasons, management and developers in this sector are traditionally sceptical about employing formal means of development. However, there are signals that this attitude is going to change. SMEs, the market of which becomes increasingly important, cannot or do not want to employ large numbers of IT consultants to adapt and fix code. Ensuring a high degree of quality, however, requires more precise models that could, with predictable and acceptable costs, be provided using formal methods. Nevertheless, convincing developers and managers in the business information sector requires real evidence of success; DEPLOY aims to provide this.


We will evaluate the benefits and the problems posed by deploying formal methods in the business information sector and develop a deployment strategy that is most suitable for this sector. We will identify which areas and types of products would benefit best from the formal development and will select one application component which will be object of the further investigations.

We intend to focus on business applications which are reusing behaviour implemented inside of a platform. This platform is based on SAPís Enterprise Service-Oriented Architecture (Enterprise SOA), SAPís blueprint for an adaptable, flexible, and open IT architecture for developing services-based, enterprise-scale business solutions. Such applications heavily rely on contracts between service providers and consumers or modifiers. These contracts and their implementations could be precisely defined and made sound and secure with the help of the DEPLOY methods.

The following results should be obtained in the course of DEPLOY:

  • A formal specification on several kinds of refinement levels of the chosen application, of used platform services, and of extensibility mechanisms, maintaining integrity and security of platform and application.
  • A clear documentation of the benefits of formal method application, in terms of quality and development efficiency compared to traditional development.
  • A deployment strategy facilitating the use of formal methods in the further projects that develop business information software. The strategy should be based on existing processes, tools, and languages used in industrial practice: We aim to define a formal methods enhanced variant of one of the processes used at SAP, such as the Product Innovation Lifecycle25 (PIL), which describes the management of SAPís software products throughout their entire lifetime, including invention, definition, development, deployment, and optimisation phases. Of particular importance is research on how requirements are traced within these processes and how the formal method can be integrated with informal and semi-formal domain specific in-house tools and languages.

Description of Work

This sub-project is split into seven tasks which are devoted to (1) exchanging information with the academic community, to (2) the actual deployment, and to (3) measurement of success as well as integration activities:

Tasks T4.1-T4.2 on Technology Transfer: In these tasks the transfer of knowledge from the Event-B experts to SAP is organised. Moreover SAP will investigate which of their application domains is most suitable to the application of formal methods. In addition, the transfer of general requirements to WP6-WP10 is captured here.

Tasks T4.3-T4.5 on Deployment: This work includes two consecutive deployment tasks, pilot deployment and enhanced deployment, as well as of research on sector specific issues. The pilot deployment builds the basic functionality limited to the essential parts of the selected application, while the enhanced deployment extends the scope of the pilot and focuses on integration with existing semi-formal and informal tools and languages. Sector specific issues to be addressed will encompass security, e.g. user management, and the adaptation of the formal method to Enterprise SOA.

Tasks T4.6-T4.7 on Method Assessment and Process Integration: These tasks validate the expected benefits of applying the formal method in terms of development efficiency and dependability. Moreover they are concerned with integrating the results obtained in T4.3-T4.5 into a development process applied at SAP.

Deploy-Project - All right reserved