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.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-34895-5_20
Chapter PDF
Similar content being viewed by others
References
Allen, R., Garlan, D.: A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology 6(3), 213–249 (1997)
Arnold, A.: Finite Transition Systems. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1994)
Bardin, S., Finkel, A., Leroux, J.: FASTer Acceleration of Counter Automata in Practice. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 576–590. Springer, Heidelberg (2004)
Barros, T., Henrio, L., Madelaine, E.: Behavioural Models for Hierarchical Components. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 154–168. Springer, Heidelberg (2005)
Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)
Bracciali, A., Brogi, A., Canal, C.: A Formal Approach to Component Adaptation. Journal of Systems and Software 74(1) (2005)
Brückner, I., Wehrheim, H.: Slicing an Integrated Formal Method for Verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 360–374. Springer, Heidelberg (2005)
Calder, M., Maharaj, S., Shankland, C.: A Modal Logic for Full LOTOS Based on Symbolic Transition Systems. The Computer Journal 45(1), 55–61 (2002)
Clarke, E.M., Grumberg, O., Long, D.E.: Model-Checking and Abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems 19(2), 253–291 (1997)
Delzanno, G.: An Overview of MSR(C): A CLP-based Framework for the Symbolic Verification of Parameterized Concurrent Systems. In: Proc. of WFLP 2002. ENTCS, vol. 76, Elsevier, Amsterdam (2002)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient Algorithms for Model Checking Pushdown Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
Finkel, A., McKenzie, P., Picaronny, C.: A Well-Structured Framework for Analysing Petri Nets Extensions. Information and Computation 195(1-2), 1–29 (2004)
Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. EASST Newsletter 4, 13–24 (2001)
Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Ingólfsdóttir, A., Lin, H.: A Symbolic Approach to Value-passing Processes. Handbook of Process Algebra, ch. 7. Elsevier, Amsterdam (2001)
Jeannet, B., Jéron, T., Rusu, V., Zinovieva, E.: Symbolic Test Selection Based on Approximate Analysis. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 349–364. Springer, Heidelberg (2005)
Kramer, J., Magee, J., Uchitel, S.: Software Architecture Modeling and Analysis: A Rigorous Approach. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 44–51. Springer, Heidelberg (2003)
Leue, S., Mayr, R., Wei, W.: A Scalable Incomplete Test for the Boundedness of UML RT Models. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 327–341. Springer, Heidelberg (2004)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design 6(1), 11–44 (1995)
Mateescu, R.: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 81–96. Springer, Heidelberg (2003)
Moschoyiannis, S., Shields, M.W., Krause, P.J.: Modelling Component Behaviour with Concurrent Automata. In: Proc. of FESCA 2005. ENTCS, vol. 114(3), pp. 199–220 (2005)
Poizat, P., Royer, J.-C.: Korrigan: a Formal ADL with Full Data Types and a Temporal Glue. Technical Report 88-2003, LaMI, CNRS et Université d’Evry Val d’Essonne (September 2003)
Poizat, P., Royer, J.-C., Salaün, G.: Symbolic Bounded Analysis for Component Behavioural Protocols. Technical report, Écoles des Mines de Nantes (2005), Available at: http://www.emn.fr/x-info/jroyer/rrBounded.pdf
Schneider, F.B.: Enforceable Security Policies. ACM Transactions on Information and System Security 3(1), 30–50 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Poizat, P., Royer, JC., Salaün, G. (2006). Bounded Analysis and Decomposition for Behavioural Descriptions of Components. In: Gorrieri, R., Wehrheim, H. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2006. Lecture Notes in Computer Science, vol 4037. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11768869_5
Download citation
DOI: https://doi.org/10.1007/11768869_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34893-1
Online ISBN: 978-3-540-34895-5
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
