Database of Case Studies Achieved Using CADP

Validation of Semantic Composability in Simulation Models

Organisation: National University of Singapore

Method: CoDES
Labeled Transition Systems

Tools used: CADP (Construction and Analysis of Distributed Processes)
SPIN

Domain: Component-based Systems.

Period: 2009 - 2010

Size: n/a

Description: Component-based simulation has been of interest in the modeling and simulation research community in recent years. Models developed using reused components are appealing because of shorter development time and their flexibility in meeting diverse user needs. While there are many benefits of component-based modeling, several challenges including semantic composability and semantic composition validation remain. The validation of composable simulations is a non-trivial problem. Challenges arise from the fact that composition is not a closed operation with respect to validation, compositions have emergent properties, and reused simulation components were developed in conflicting contexts. Validation must also address logical aspects such as deadlock, safety, and liveness, temporal aspects such as the behavior of components and compositions over time, and formal aspects such as the need to provide a formal measure of the validity of compositions.

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.

Conclusions: A formal validation process is proposed, based on a new formalization of simulation composability. A component is represented as a function of its states over time, an attribute of paramount importance in simulation. The validation process formally compares the composition execution schedule to that of a perfect composition. This is based on a new semantic metric relation, which considers semantically related composition states. The first two layers of the validation approach were fully automated and integrated in the CoDES framework, thanks to existing verification tools such as SPIN and CADP. The current work addresses the semantic validation of simulation model developed using base components, and future work aims at extending the validation process to include the more complex reused model components.

Publications: [Szabo-Teo-See-09] Claudia Szabo, Yong Meng Teo, and Simon See. "A Time-based Formalism for the Validation of Semantic Composability". Proceedings of the Winter Simulation Conference, pages 1411-1422. IEEE Computer Society Press, December 2009.
Available on-line at: http://www.comp.nus.edu.sg/~teoym/pub/09/WinterSim2009-TR.pdf
or from our FTP site in PDF or PostScript

[Szabo-Teo-09] Claudia Szabo and Yong Meng Teo. "An Approach for Validation of Semantic Composability in Simulation Models". Proceedings of the 23rd ACM/IEEE/SCS Workshop on Principles of Advanced and Distributed Simulation PADS'2009, pages 3-10. IEEE Computer Society Press, June 2009.
Available on-line at: http://www.comp.nus.edu.sg/~teoym/pub/09/Semantic-composability-PADS2009-full-version.pdf
or from our FTP site in PDF or PostScript

[Szabo-Teo-10] Claudia Szabo and Yong Meng Teo. "On Validation of Semantic Composability in Data-Driven Simulation". Proceedings of the 24th ACM/IEEE/SCS Workshop on Principles of Advanced and Distributed Simulation PADS'2010, pages 1-8. IEEE Computer Society Press, May 2010.
Available on line at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5471654
or from our FTP site at PDF or PostScript

[Szabo-Teo-11] Claudia Szabo and Yong Meng Teo. "An Analysis of the Cost of Validating Semantic Composability". Proceedings of the 25th ACM/IEEE/SCS Workshop on Principles of Advanced and Distributed Simulation PADS'2011, pages 1-8. IEEE Computer Society Press, June 2011.
Available on line at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5936769
or from our FTP site at PDF or PostScript
Contact:
Prof. Yong-Meng Teo
Department of Computer Science
National University of Singapore
Computing 1, #03-68,
13 Computing Drive
Singapore 117590
Tel: (65) 6516 2830
Fax: (65) 6779 1610
Email: teoym@comp.nus.edu.sg



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page