Research Areas

We have particular interest in the following research areas:

Formal Methods
We use formal mathematical notations for verifying properties of software and systems. In this way we pursue higher reliability and robustness levels. Among several notations, we have particular interest in the CSP (Communicating Sequential Processes) process algebra.
Model Checking
Based on formal notations, models are created and then analysed to evaluate if they conform to the desired properties. We have particular interest in symbolic model checking for enhancing the performance of traditional model checking approaches.
Theorem Proving
We also have interest in the use of proof assistants and automated theorem provers to prove properties of the system besides dealing with proof obligations.
Component Software Development
To avoid scalability issues, we pursue the compositional application of formal methods. Thus we can design, develop and verify software and systems based on their components.
Model Software Engineering
Besides enabling the analysis of properties of systems, the construction of formal (and semi-formal) models might guide the software engineering / development process. In this way, we create an environment for model-based software engineering.
Software Testing
When it is not possible to only rely upon formal methods, we apply testing techniques to assure the desired levels of reliability. We have been studying many testing perspectives including the formalization of the respective testing theories.
Safety Assessment
We also have interest in the application of formal method for helping the safety assessment of critical systems. In this area, we study how formal methods might enable and help companies to adhere to standards and recommendation practices of critical fields.
Software Development Processes
We also study and propose software development processes that integrate formal methods and testing approaches for enhancing the software reliability.
System of Systems
In the last years we have also analysed how the traditional formal methods and testing approaches should be applied in a context of system of systems. Thus we have interest in model-based strategies for developing and maintaining system of systems.

 
Our researches concern mainly the following application domains:


Avionics

Telecom