Formal reuse and validation of information system specifications/Réutilisation et validation formelle des spécifications de systèmes d'information

点击翻译按钮获取中文摘要

Information systems (IS) are prevalent in today's economy. A typical example of IS, and probably the most important one, is the Enterprise Resource Planning system (ERP), with its 18 billion $ worldwide market. To manage costs, enterprises are buying COTS (commercial of the shelf) IS like ERPs, but that forces them to adapt their business process to the COTS, reducing their flexibility and ability to develop innovative business strategies, and locking them with a single vendor with little bargaining power for controlling maintenance costs. This proposal aims at providing a more flexible way of designing IS that better match the rapidly evolving environment that organisations are facing. We want to build on the platform that we have developed over the past five years, called APIS, and extend its capabilities for building an IS, from the user interface to services and databases. There are three axes we want to address: reuse, validation and instrumentation. Reuse is a key productivity and quality issue in IS building. For instance, Hertz's car rental system is probably very similar to Budget's, but not exactly the same. We want to study reuse mechanisms at the specification level, so that one can build a generic specification, e.g., for a car rental system, and instantiate it and tailor it for a specific enterprise environment, while preserving the properties and the capabilities specified at the generic level. The APIS platform eliminates most of the need for design and implementation, which means that unit, integration and system testing are also eliminated. However, there is still a need to perform validation and acceptance testing, to make sure that the system specification is the appropriate one, that it satisfies business requirements. This can be done manually, by designing tests scenarios. We could go a step further by using modern verification technology, either by using theorem proving or model checking.