PostScript
Bounded Analysis and Decomposition for Behavioural Descriptions of Components
Pascal Poizat, Jean-Claude Royer, Gwen Salaün
Proceedings of the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems FMOODS 2006 (Bologna, Italy), June 2006.
Abstract:
Explicit behavioural interfaces are now accepted as a mandatory feature of components to address architectural analysis. Behavioural interface description languages should be able to deal with data types and with rich communication means. Symbolic Transition Systems (STS) support the definition of component models which take into account control, concurrency, communication and data types. However, verification of components described with protocol modelled by STS, especially model-checking, is difficult since they possibly involve different sources of infinity. In this paper, we propose the notions of bounded analysis and bounded decomposition. They can be used to test boundedness of systems and to generate finite simulations for them so that standard model-checking techniques may be applied for verification purposes.
| 15 pages | |
PostScript |