This work proposes a three-layered approach to semantic validation with increasing accuracy and complexity. In the first layer, the composed model is abstracted as a composition of concurrent processes and desired logical properties are validated by a model checker. In the second layer, a metasimulation of the composition is executed over time to validate safety and liveness. The third layer, called perfect model validation, provides a formal, but more complex guarantee of correctness. The validation in each layer exploits the results or guarantees provided by the previous layers. Major abstraction trade-offs and drawbacks in one layer are addressed in the subsequent layers. All layers assume that the component communication is correct and meaningful.

A component is represented formally as a function of states over time. This function is unfolded over the simulation time using sampled values for the time attributes. The mathematical functional composability of the component functions is validated using a new composability definition. If the functions are composable, then an interleaved execution schedule of all functions is obtained, which represents a simulation run of the composition. To validate the composition, it is considered that for each type of base component there exists a perfect model in the repository, formally represented as a perfect function of its states over time. The perfect functions are defined by application domain experts, when the application domain is added to the CoDES framework. The perfect functions are composed and a simulation run of the perfect composition is obtained by repeating the above process. The simulation of the composition and the perfect composition are represented using Labeled Transition Systems (LTSs). In this context, the semantic composability is formally defined in terms of the comparison of the LTSs modulo bisimulation relations. If the two LTSs are not strongly bisimilar, the constraints in the second stage are relaxed by defining a semantic metric relation that considers only LTS nodes for which the semantic distance is smaller than a threshold value. Then, if the semantic metric relation is a weak bisimulation between the two LTSs, then the composition is semantically valid.

The approach is demonstrated using a single-server queue example consisting of Queueing Networks base components. Each component has an attached implementation described in a metacomponent. The components are encoded in Promela and checked for safety and liveness using the SPIN model checker. As regards perfect model validation, the interleaved execution schedules obtained for both composition and perfect composition are represented as LTSs and compared modulo strong bisimulation using the BISIMULATOR tool of CADP.