RFBR Grant 03-01-00821
Modeling of compositional specifications intended for automated proof of correctness of refinement of specifications of requirements by pre-existing components in course of a compositional development of information systems (REFINE)
Project starting date
Leonid Kalinichenko, Institute of Informatics Problems RAS, Moscow, Russia
- Institute of Informatics Problems RAS
The problem of compositional specification modeling is an important constituent of the compositional information systems (IS) development problem reusing pre-existing components. Basic idea of compositional IS development consists in construction of a composition of pre-existing components (of various kinds – data, services, processes) refining specification of the IS being developed. For the construction specifications of IS and of the pre-existing components are represented in the unified (canonical) model. Formal proof of refinement of specifications of IS by a composition of pre-existing components is the fundamental step of the compositional development process. Specification A refines specification D, if we can use A instead of D so that the user of D does not notice this substitution. According to the project, the development of methods and tools for specification modeling providing for semi-automatic proof of refinement applying formal methods is to be accomplished.
In frame of the project a problem of formalization of a fundamental step of the process of Information Systems (IS) compositional design has been solved. This step consists in a proof of refinement of a IS specification by a composition of pre-existing component specifications. The SYNTHESIS language is used in the project as a canonical model intended for unified representation of the requirement and component specifications. A formal denotational-axiomatic semantics for the canonical information model has been developed. In frame of the project an extension of the compositional design involving web-service components has been investigated and developed. Also ontological modeling facilities for compositional design have been refined. A mapping from the canonical model into the Abstract Machine Notation (AMN) has been developed for the formalization and automatic/interactive proof of the refinement. AMN is a formal specification language based on first order predicate logic and set theory. AMN constructions have been developed for the SYNTHESIS constructions mapping allowing to specify information, program and process components. Algorithms of translation of the SYNTHESIS modules into collections of the AMN abstract machines have been developed. A proof of correctness of the mapping stating the semantics of the specifications is preserved while constructing the mapping. A tool prototype aimed at the automatic mapping of the canonical specifications into the AMN has been implemented. Prototype implementation includes algorithms mapping canonical model abstract data types, process types, classes and full predicative specifications of functions (methods) into AMN. A methodology of the tool application for formal proof of correctness of IS compositional design has been obtained.