Symbolic Testing of Embedded Software Systems
Model-driven engineering (MDE) is a promising new paradigm in system development. Its potential stems from its emphasis on using high-level modelling languages for specifying, designing and developing systems, while automating many of the downstreams activities like programming, simulation and testing. A large family of commercial softwares are available which support this paradigm. This has led to a wide-spread adoption of model-based approach in the Industry, particularly in the safety-critical embedded domain. For example, Matlab Simulink is now a de facto standard development platform in the automotive and aerospace domain.
Symbolic testing has proved to be a very successful testing methology in program testing. There are a number of characteristics in such models which add new challenges to applying symbolic testing and as also provide opportunities to simplify the process.
In this project, we apply symbolic testing to test models designed with Matlab Simulink and similar languages.
Verification of Refinements of Embedded Software Architecture
Embedded software architectures typically describe the physical components of the embedded system along with the software components and are extensively being used to describe the architecture of software residing in automotive, avionics and other embedded applications. Such architectures are defined in a modular fashion like all others, with detailed architectural constructs evolving with successive refinements. We are exploring the problem of formally modeling and verifying embedded software architectures with the aim of proving a refined architecture to be correct with respect to its abstract architecture, in terms of satisfying a set of specified properties. This project is currently using AADL as a benchmark language for embedded software architecture. EventB is used to formally represent such architectures and refinements are being shown to be correct with respect to their semantics as represented by EventB.
Specification, Verification and Validation of Web-Applications
Representational State Transfer (REST) is the latest architectural style catching a lot of attention in the domain of web-service design and implementation. Web-services, due to their distributed, loosely-coupled, and syndicated architecture, provide very unique challenges to software engineers at every stage of SDLC, beginning with specification all the way upto testing.
In this project, we are dealing with the challenges of formal specification and automated testing of web-services, specifically RESTful web-services -- the web-services following the REST architecture.