Related Communities:

Automation of refinement verification

Automation of refinement verification in information systems compositional design.

Author(s): Stupnikov S.A.
Published:Formal Methods and Models for Compositional Infrastuctures of Distributed Information Systems: The Systems and Means of Informatics, Special Issue. -- Moscow: IPI RAN, 2005. -- P. 96--119. (In Russian)

This paper considers a technique for providing of Abstract Machine Notation (AMN) formal semantics for the canonical information model (SYNTHESIS language) specifications. Such mapping is used for automation of refinement correctness proving during composition of information systems and mediators on the basis of existing program and information components in interoperable environments.

Program tools for automatic mapping of canonical specifications into AMN are introduced. The technique for using such tools for automation of refinement correctness proving while composition of IS and mediators on the base of components is considered and illustrated by an example.

Download: [ PostScript ]

Supported by Synthesis Group