Tallinn University of Technology

Formal methods group

Cooperation with formal methods group

The Formal Methods Group is a research subgroup of the High-Assurance Software Laboratory. 

Formal methods are mathematically rigorous (commonly tool-supported) techniques for the specification, development, and verification of software and hardware systems in order to ensure correct behavior, reliability and trustworthiness of the design. Formal methods evolve in symbiosis with AI.

OUR EXPERTISE:

  • Software testing and verification
  • Machine learning and analysis of the human motor functions
  • Autonomous land and underwater robots navigation and task automation

WHICH PROBLEMS CAN WE SOLVE?

  • Modelling, verification, model-based testing and synthesis of autonomous systems operating under critical time, safety and security constraints.
  • Robotic and autonomous systems software development and automated testing, incl. simultaneous localization and mapping (SLAM), decision making under uncertainty, autonomous control, navigation, cyber-physical systems digital twins, picking and placing objects, and visual servoing.
  • Digitization of the gross- and fine-motor tests to support diagnostics and monitoring of neurologic and cognitive disorders, capture and machine learning of motor activities and fatigue detection.

HOW CAN WE HELP YOU

Software testing and verification

Machine learning and analysis of the human motor functions

Autonomous land and underwater robots navigation and task automation

Providing software quality assurance support by system/requirements modelling, proving correctness of design solutions, and generating test suites.

Developing provably correct software for autonomous and robotic systems.

Providing expertise in the following fields: formulating machine learning (ML) and AI problems, building AI and ML workflows, choosing goodness criteria and support model testing; capturing and analysing human motions.

REFERENCES AND PREVIOUS PROJECTS: