Symbolic Bounded Analysis for Component Behavioural Protocols
Pascal Poizat, Jean-Claude Royer, Gwen Salaün · 2005
Explicit behavioural protocols are now accepted as a mandatory feature of components to address architectural analysis. Behavioural protocol languages must be able to deal with data types and with rich communication means. Symbolic Transition Systems are an adequate component model which takes into account dynamic aspects and data types. However, verification of components described with STS protocols is di#cult since they possibly involve di#erent sources of infinity. In this paper, we propose a notion of symbolic bounded analysis. This approach tests boundedness of a possibly infinite system, and then generates a finite simulation for it. Afterwards, standard model-checking techniques can be used for verification purposes.