Automata-Based Compositional Analysis of Component Systems. Design and Implementation Issues

Specifying a real-world component system is a complex manual process. It is essential to be able to verify the correctness and robustness of its behavior, before it becomes operational. We propose a new way of specifying a component system, based on the concept of interface, that can be seen as a tool from analysis and design to programming and for type specification. We construct an algorithm that constructs the model, and can be used to deduct properties about the system: correctness, termination, deadlock free.