Research Areas

  • Formal Modeling and Verification of Safety Critical Systems
    Dr. Arpit Sharma

    The design of complex software and hardware systems is a nontrivial task and is usually accomplished with some kind of formal modeling to gain confidence on the behavior of system under design. Such formal models are essentially developed with the focus on either proving the functional correctness, like something bad or unintended will never happen, or establishing certain bounds focused on the performance of the system under design. My research focuses on model checking and model-based testing of safety-critical software and hardware systems.

    Model checking is an automated verification method guaranteeing that a mathematical model of a system satisfies a formally described property. Model-based testing (MBT) is a most promising approach to systematic testing of software systems. The system under test is described as a formal model, and MBT theories describe notions of correctness of an implementation w.r.t. a model.