• CoIn Project information

    Component-based methodology is founded on a paradigm stating that complex systems can be obtained by assembling components. The methodology is essential for rigorous system design. A crucial constituents of the methodology are methods for formal verification of component-based systems. In this project we concentrate on formal verification of component-interaction properties. To this end, components are modeled using Component-Interaction Automata (CI Automata, or CoIn Automata for short) as abstractions that ignore implementation details and describe properties relevant to their interaction logic. Complex systems are built by composition of simpler components. The composition can be formalized as an operation that takes in components and provides the decription of a new, more complex component.

    The aim of the project is to develop a semantic framework for component-based modeling and describing the dynamic behaviour of components and their interactions. Futhermore, we aim at providing algorithms and techniques for formal verification of their temporal properties. The ultimate goal of the project is to come up with a tool for automatic verification of component-interaction properties of component-based systems.

  • CoIn Team

  • Former members

  • Links

  • Meetings

    The group meets each Thursday at 14:00 in Room C408.

  • Selected publications

    N. Beneš, L. Brim, I. Černá, J. Sochor, P. Vařeková and B. Zimmerová. Partial Order Reduction for State/Event LTL. In Proceedings of the International Conference on Integrated Formal Methods (IFM'09), volume 5423 of LNCS, pages 307-321. Springer-Verlag, February 2009. [ bib ]

    P. Vařeková, B. Zimmerova, P. Moravec, and I. Černá. Formal Verification of Systems with an Unlimited Number of Components. In IET Software journal, Volume 2, Issue 6, pages 532-546. Institution of Engineering and Technology (IET), December 2008. [ url | bib ]

    N. Beneš, I. Černá, J. Sochor, P. Vařeková and B. Zimmerova. A Case Study in Parallel Verification of Component-Based Systems. In Proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'08), volume 220 of ENTCS, pages 67-83. Elsevier Science Publishers, December 2008. ISSN 1571-0661. [ bib ]

    B. Zimmerova, P. Vařeková, N. Beneš, I. Černá, L. Brim and J. Sochor. The Common Component Modeling Example: Comparing Software Component Models, chapter Component-Interaction Automata Approach (CoIn), volume 5153 of LNCS, pages 146-176. Springer-Verlag, August 2008. [ bib ]

    I. Černá, P. Vařeková, and B. Zimmerova. Component Substitutability via Equivalencies of Component-Interaction Automata. In Proceedings of the Workshop on Formal Aspects of Component Software (FACS'06), volume 182 of ENTCS, pages 39-55. Elsevier Science Publishers, June 2007. ISSN 1571-0661. [ bib ]

    L. Brim, I. Černá, P. Vařeková, and B. Zimmerova. Component-interaction automata as a verification-oriented component-based system specification. In ACM SIGSOFT Software Engineering Notes, New York, USA : ACM Press, Volume 31, Issue 2, March 2006. [ bib ]

    Other publications and presentations can be found here.

  • Models

    • Models and other information from our participation in the CoCoME modelling contest can be found on the CoCoME page.
    • CI models of Control-User systems created from previously published models of component-based systems.