Mediation systems modeling and verification

A mediation system is designed to support interoperability from distributed, heterogeneous data sources. Research on data integration has provided a set of rich and well-understood schema mediation languages to define either the mediation schema or the contents of data sources. However, the mediation system is a highly dependable complex system, but little work is dedicated to assuring system behavior correctness. Due to the huge program size and complexity of system, it is not possible to formally verify the system properties at the source code level. So the mediation system requires rigorous modeling and analysis techniques to assure the system correctness and properties at the design level. This paper defines and analyzes mediation systems by the software architecture model (SAM), a formal systematic software architecture specification and analysis methodology that is able to define and analyze different system aspects using different formalisms. In this paper, the behaviors of mediation systems are captured by Petri net and the architecture properties are specified and analyzed by temporal logic.