Parallel and Real-Time Research Group (PART)

Our research interests encompass all the aspects of parallel computations, including distributed systems. We are also interested in real-time computations. Unsurprising, our main focus is therefore at the intersection of these two areas, that is, in the domain of parallel and distributed real-time computations.

We approach the mentioned areas from three perspectives: complexity-theoretic, formal methods and testing, and systems. Our main drive is currently on formal methods and conformance testing, but we are also involved in complexity-theoretic approaches and to some degree in systems.

In a first variant of conformance testing (e.g., model checking), the specification consists in a logical formula, which is checked against the implementation; in a second variant (e.g., model-based testing) the specification takes an algebraic form and is then compared with the implementation either directly or via systematic test suites. A mixed, logic and algebraic approach has been tried more or less incipiently in the area of untimed (non-real-time) systems. One of the research directions we are pursuing is such a unified approach for real time. In particular, a hybrid approach to real-time specification should become possible: we will allow logic specifications for those parts of the system most suitable for such, and algebraic specifications for those parts which are more suitable for such a description.

Conformance testing is mostly focused on finite-state systems and is thus suitable for the verification of hardware and communication protocols, and less suitable for the verification of software. Conformance testing of infinite systems—more suitable for software verification—has received however sustained attention recently, though most of this attention is on the logical (model checking) side. Another direction in our research is the study of algebraic, compositional approaches to this area. Our work on the matter is not real time, but we plan to extend it into the real-time domain soon. Our work on the matter is based on visibly pushdown languages, but plans to extend it to context-free constructs and beyond exist.

In all, we are investigating more or less in parallel algebraic approached to the conformance testing of infinite-state systems, and also unified approaches (logic and algebraic) of classical (finite-state) systems. One day these will be joined together into a nice unified theory of conformance testing for infinite-state systems.

We are also interested in the complexity theory of massively parallel systems. Recent, continuing work on the matter includes the characterization of models with reconfigurable busses as opposed to models with shared memory.