by Nikola Beneš, Luboš Brim, Ivana Černá, Jiří Sochor, Pavlína Vařeková, Barbora Zimmerová, July 2008, 21 pages.
FIMU-RS-2008-07. Available as Postscript, PDF.
Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems.
by Pavlína Vařeková, Ivana Černá, A full version of the paper presented at conference CBSE 2008. July 2008, 27 pages.
FIMU-RS-2008-06. Available as Postscript, PDF.
Many real component-based systems, so called Control-User systems, are composed of a stable part (control component) and a number of dynamic components of the same type (user components). Models of these systems are parametrised by the number of user components and thus potentially infinite. Model checking techniques can be used to verify only specific instances of the systems. This paper presents an
by Ivana Černá, Pavlína Vařeková, Barbora Zimmerová, October 2006, 25 pages.
FIMU-RS-2006-08. Available as Postscript, PDF.
The paper introduces a Component-interaction automata language, which was designed for modelling of component interactions in hierarchical component-based software systems. The language supports modelling of important interaction attributes of such systems, and hence provides a rich base for further application of formal methods. Component-interaction automata provide a flexible form of component composition which can respect architectural assembly of the system, communication mechanisms, and other specifics of component-based systems. This allows the language to capture interactions in many different kinds of componentbased systems (built on different component models for instance). This paper provides a detailed study of the language including discussion of its practical application