@inProceedings{CIA:SAVCBS-05, author = "Lubo\v{s} Brim and Ivana \v{C}ern\'{a} and Pavl\'{i}na Va\v{r}ekov\'{a} and Barbora Zimmerova", title = "{{C}omponent-{I}nteraction Automata as a Verification-Oriented Component-Based System Specification}", booktitle = "Proceedings of the ESEC/FSE Conference on Specification and Verification of Component-Based Systems (SAVCBS'05)", publisher = "Iowa State University, USA", pages = "31--38", year = "2005", month = "September", url = "http://www.cs.iastate.edu/~leavens/SAVCBS/2005/SAVCBS05.pdf", note = "Published also in ACM SIGSOFT Software Engineering Notes, Volume 31, Issue 2 (March 2006)", abstract = "In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-oriented model connected to verification tools at the end. After examining current general formal models with respect to their suitability for description of component-based systems, we propose a new verification-oriented model, Component-Interaction automata, and discuss its features. The model is designed to preserve all the interaction properties to provide a rich base for further verification, and allows the system behaviour to be configurable according to the architecture description (bindings among components) and other specifics (type of communication used in the synchronization of components)." } @article{CIA:SAVCBS-05-SEN, author = "Lubo\v{s} Brim and Ivana \v{C}ern\'{a} and Pavl\'{i}na Va\v{r}ekov\'{a} and Barbora Zimmerova", title = "{{C}omponent-{I}nteraction Automata as a Verification-Oriented Component-Based System Specification}", journal = "ACM SIGSOFT Software Engineering Notes", volume = "31", number = "2", pages = "1--8", year = "2006", month = "March", note = "SESSION: Specification and Verification of Component-Based Systems (SAVCBS 2005), Article No. 4", abstract = "In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-oriented model connected to verification tools at the end. After examining current general formal models with respect to their suitability for description of component-based systems, we propose a new verification-oriented model, Component-Interaction automata, and discuss its features. The model is designed to preserve all the interaction properties to provide a rich base for further verification, and allows the system behaviour to be configurable according to the architecture description (bindings among components) and other specifics (type of communication used in the synchronization of components)." }