Formal support for design and analysis of reactive, disturbed, real-time, hybrid, and cyber-physical systems; Software testing and verification; Model driven software development; Service oriented computing.