Research Interests

Application of formal methods in verificaton of real-time safety-critical systems

• Modelling: and Verification: A major element of my research is the development and application of languages and techniques for modelling a system - being software, hardware or a combination of the two. It draws from knowledge representation techniques in AI, formal specification languages in software engineering and modelling methods from the automatic control area. I consider architectural decomposition as a major ingredient for modular modelling and iterative refinement of system design. My recent work concerns discrete models of an embedded system, as well as hybrid models of the software and its physical environment, where both discrete and continuous elements are represented explicitly. I am also interested in techniques and tools for verification of safety-critical embedded systems. My recent work includes the study of applications of temporal logic, symbolic model checking, and automata-based decompositional proof techniques.

• Tools and languages: In connection with research cooperation projects I have been involved in the study, development and application of several modelling and verification techniques. Among these are discrete models (Statecharts, Esterel, I/O machines, Transition systems, Petri nets, Rule-based systems), hybrid models (incorporating both continuous and discrete elements: Hybrid transition systems, Hybrid automata, Extended Duration Calculus), as well as physical modelling techniques based on the language of Bond graphs. For current activities in these areas see my activities page.

•  Dependability in distributed architectures: Several major application areas are  inherently distributed or increasingly solved by adoption of distributed architectures. This introduces new research problems when dependability is a requirement. In safety-critical systems the interaction of fault-tolerance and real-time requirements is of prime interest. Another recent research interest for me is the interaction of  quality of service requirements and fault-tolerance in distributed applications. Software implementation of replication and group services in the middleware, and their impact on other system requirements such as timeliness and availability is a current active area.

Together with  professor Zebo Peng  we  pursue a common interest in the area of application of formal methods in hardware/software co-design of embedded systems.