I am a PhD student at the Programming Languages and Software Engineering Lab working under Prof Chin Wei Ngan. I started my graduate studies in Aug 2010.
(Contact Info: asankhaya at nus.edu.sg)
Currently working on Verification of Heap Manipulating Programs
Based on the informal specification released by Boston Scientific we formally model the pacemaker in PROMELA using the SPIN model checking tool. Each component of the pacemaker is modeled as a separate process in PROMELA. We model all the 18 modes of the pacemaker along with advanced features like rate controlled pacing and hysteresis. Using LTL properties we verify desired behavior of the system, all timing requirements from the specification are successfully verified in our model. Taking guidance from the PROMELA model we also show how it is possible to generate C code for the implementation. The implementation is then validated against the PROMELA model using the same tool SPIN. This is the first attempt which we know of where the pacemaker software is verified and validated entirely end to end (from requirements to implementation) using formal methods. In addition to our original sequential model (PROMELA and C) we show that it is possible to extend the model to Concurrent and Distributed setting. This allows us to capture many more behaviors of the system and thus generate a more flexible model.
Previously, I worked on Code Analysis Tool for .NET (CAT.NET 2.0) Details Download