Formal analysis of component-based systems
The principle of component-based development is very simple -- buy components realizing necessary functionality, and obtain the required system via their assembly. This principle is well known and basically widely used by all of us, for instance during computer-hardware assembly. The component-based development brings a number of benefits, including configurability, high development speed, and lower cost.
In the software world, however, component-based development becomes more challenging, because software components use to be very complex. When one needs to assemble components from different vendors, there is a high risk that the components are not going to cooperate together correctly. Even if the assembly task is successful and the components cooperate as expected, there is a need of methods evaluating future updates of the system, realized via replacement of existing components with new versions.
One of the possible methods for checking correctness of assembled system is system testing. While testing use to be successfully employed to uncover software faults, it can never give us the guarantee that there are actually no faults remaining in the system, because it does not examine the system fully. This is insufficient, if the hidden faults can have serious effects. A credible alternative method to checking system correctness is the formal analysis and verification, which is our main concern.
Our team search for the techniques and strategies helping in construction of correct and dependable component-based systems. We design formal models of components and develop automatic methods, which help us to answer questions about their behaviour and behaviour of the systems assembled of them.
The main research priorities
- Tools for design and modelling of component-based systems
- Verification of interaction properties of component-based systems
- Languages for description of interaction properties
Information for students
The domain of formal component-based engineering methods is very wide. In our team, we therefore welcome students of both bachelor and master study programme. Students interested in software engineering methods, as well as students interested in formal verification techniques can find their fulfillment in our team. If interested in more information, do not hesitate to contact any of the team members, or see this page.