Animating Formal Models in a Communicating Sequential Process Platform

I. Sakellariou, G. Eleftherakis, I. Vlahavas, P. Kefalas, “Animating Formal Models in a Communicating Sequential Process Platform”, 10th Panhellenic Conference on Informatics, Local Proceedings, P. Bozanis and E. Houstis (Eds.), pp. 174-183, 2005.

10th Panhellenic Conference on Informatics, Local Proceedings, P. Bozanis and E. Houstis (Eds.), pp. 174-183, 2005.

The X-machine formal method forms the basis for a specification/modeling language with a substantial potential value to software engineers. An X-machine is a more expressive and flexible state machine, capable of modeling both the dynamic and the static aspect of a system. Communicating X-machines provide a methodology for building communicating systems out of existing stand-alone X-machines. However, for practically using the model in an real-world system development process, a tool for demonstrating and informally verifying the properties of the modeled system is required. An ideal platform for efficiently implementing such a tool, should support, process oriented programming, efficient communication primitives and declarativeness. CSPCONS is a distributed CLP platform that supports program execution over multiple independent sequential CLP processes that synchronize though message and event passing. The present paper demonstrates the applicability of the cons programming model to the implementation of a communicating X-machine animator tool that will act as the basis for an extended set of tools that will support the formal mathematical analysis of the specified X-machine models.