On Conditions for Modular Verification in Systems of Synchronising Components

• Autorzy: Drábik P. , Maggiolo-Schettini A. , Milazzo P.
• Języki publikacji: EN

Abstrakty

EN

Property preservation is investigated as an approach to modular verification, leading to reduction of the property verification time for formal models. For modelling purposes, formalisms with multi-way synchronisations are considered. For the modular verification technique to work, a specific type of synchronisation is required for which a sufficient and necessary condition is identified. It is a requirement on the semantics of the formalism, which is restricted to permit simultaneous execution only of component moves that make reference to each other. Implications for modular verification of several well-known formalisms for concurrent systems are investigated.

Słowa kluczowe

EN

modular verification; synchronisation; automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 120, nr 3/4
• Strony: 259--274
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

Drábik P.

autor

Maggiolo-Schettini A.

autor

Milazzo P.

• Istituto di Informatica e Telematica, Consiglio Nazionale delle Ricerche, Via Giuseppe Moruzzi 1, 56124 Pisa, Italy,

Bibliografia

• [1] Attie, P. C.: Synthesis of large dynamic concurrent programs from dynamic specifications, CoRR, abs/0801.1687, 2008.
• [2] Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application, ATVA '08: Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, Springer-Verlag, Berlin, Heidelberg, 2008.
• [3] Borowiecki, M., Broere, I., Frick, M., Mihok, P., Peter, S.: A survey of hereditary properties of graphs, Discussiones Mathematicae Graph Theory, 17, 1997, 5-50.
• [4] Clarke, E. M., Emerson, E. A.: Design and synthesis of synchronization skeletons using branching time temporal logic, Logics of Programs, 1982, 52-71.
• [5] Clarke, E. M., Grumberg, O., Peled, D.: Model checking, MIT Press, 1999.
• [6] Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems, 19(2), 1997, 253-291.
• [7] Drábik, P., Maggiolo-Schettini, A., Milazzo, P.: Dynamic sync-programs for modular verification of biological systems, 2nd Int. Workshop on Non-Classical Models of Automata and applications (NCMA'10), Jena, Germany, 2010.
• [8] Drábik, P., Maggiolo-Schettini, A., Milazzo, P.: Modular verification of interactive systems with an application to biology, Scientific Annals of Computer Science, 21, 2011, 39-72.
• [9] Drábik, P., Maggiolo-Schettini, A., Milazzo, P.: On conditions for modular verification in systems of synchronizing components, Proceedings of Concurrency, Specification and Programming - XXth International Workshop, CS&P 2011 (M. Szczuka, L. Czaja, A. Skowron, M. Kacprzak, Eds.), Białystok University of Technology, Pultusk, Poland, 2011.
• [10] Feige, U., Kogan, S.: The hardness of approximating hereditary properties, 2005, Available on: http://research.microsoft.com/research/theory/feige/homepagefiles/hereditary.pdf.
• [11] Fidge, C.: A Comparative Introduction to CSP, CCS and LOTOS, Software Verification Research Centre, University of Queensland, Technical Report, 1994, 93-24.
• [12] Grumberg, O., Long, D. E.: Model checking and modular verification, ACM Transactions on Programming Languages and Systems, 16(3), 1994, 843-871.
• [13] Hillston, J.: A compositional approach to performance modelling, Cambridge University Press, 1996.
• [14] Hoare, C. A. R.: Communicating Sequential Processes, vol. 9, Prentice-Hall International, London, 1985.
• [15] Milner, R.: A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1982.
• [16] ter Beek, M., Kleijn, J.: Team Automata satisfying compositionality, FME 2003: Formal Methods, 2003, 381-400.