Zespół modelowania i analizy zajmuje się zagadnieniami związanymi z modelowaniem i analizą formalną współbieżnych systemów dyskretnych, przede wszystkim w odniesieniu do asynchronicznych wbudowanych układów i systemów sterowania w czasie rzeczywistym. W ramach badań wykorzystywany jest szereg modeli formalnych, takich jak automaty skończone i czasowe, modele grafowe, klasyczne sieci Petriego oraz szeroki wachlarz uogólnionych sieci, m.in. różnego rodzaju intepretowane sieci, sieci czasowe, kolorowane, RTCP-sieciW zespole jest rozwijany formalny język modelowania systemów współbieżnych Alvis.

W zakresie metod analizy formalnej w zespole są wykorzystywane i rozwijane rozmaite podejścia, takie jak model checking („sprawdzanie modelu”), konstruowanie i analiza pełnych i zredukowanych przestrzeni stanów systemów, analiza symboliczna, redukcja systemów i analiza strukturalna.

Innymi obszarami badań są m.in. zagadnienia związane z dekompozycją systemów współbieżnych na podsystemy sekwencyjne oraz synchronizacją i determinizmem w systemach współbieżnych.