In this paper a mapping of canonical information model (SYNTHESIS language)
core in theoretical-model specification language based on first order
predicate logic and set theory --- Abstract Machine Language (AMN) --- is defined.
The mapping provides a set of AMN abstract machines corresponding to a canonical model module.
An algorithm of canonical model module structure transformation into
compositional structure of AMN machines set is defined.
Semantic functions and algorithms transforming elements of
canonical model abstract syntax into elements of AMN machines
are defined.
The mapping developed allows to apply B-technology
tools (B-Toolkit, Antelier B)
for semi-automated proving of canonical model specifications refinement.
Thus automation of proving a correctness of solving of
various problems over multiple heterogeneous data sources, services and
components is achieved. Among such problems are
search and construction of compositions of components refining
specification of requirements; commutative data model mapping;
canonical data models synthesis;
constructing mediators in heterogeneous environments.
|
