Title: Build Your Own Model Checker in One Month
Presenters: Jin Song Dong and Jun Sun
Duration: half day
Time: Monday afternoon, 20 June 2011
Model checking has established as an effective method for automatic system analysis and verification. It is making its way into many domains and methodologies. Applying model checking techniques to a new domain (which probably has its own dedicated modeling language) is, however, far from trivial. The PAT framework is designed to facilitate development of customized model checkers. It has an extensible and modularized architecture to support new languages (and their operational semantics), new state reduction or abstraction techniques, new model checking algorithms, etc. Since its introduction 4 years ago, PAT has attracted more than 1100 registered users and has been applied to develop model checkers for 11 different languages (including concurrent systems, real-time systems, probabilistic systems, web services, sensor network, security protocols, stateflow diagram and C# language). In this tutorial, we will briefly survey a variety of model checking techniques. Then we will show how to develop a model checker for a language combining real-time and probabilistic features using PAT step-by-step, and show that it could take as short as one month to develop your own model checker with reasonable efficiency.
Jin Song Dong received Bachelor and PhD degrees in computing from the University of Queensland in 1992 and 1996. From 1995-1998, he was a Research Scientist at the Commonwealth Scientific and Industrial Research Organization (CSIRO) in Australia. Since 1998 he has been in the Computer Science Department at the National University of Singapore (NUS) where he is currently an Associate Professor as well as the NGS Supervisor. Jin Song's research is in areas of software engineering and formal methods. Jin song is steering committee member of the International Conference on Formal Engineering Methods (ICFEM) and the Asia Pacific Software Engineering Conference (APSEC). He was the General Chair for the 8th ATVA (2010) and 4th SSIRI (2010). He also acts as Program Co-Chair for the 7th APSEC (2000), 5th and 12th ICFEM (2003, 2010), 6th IFM (2007) and 12th ICECCS (2007).
Jun Sun received Bachelor and PhD degrees in computing science from National University of Singapore (NUS) in 2002 and 2006. In June 2007, he received the LEE KUAN YEW postdoctoral fellowship in the Computer Science Department at the National University of Singapore. In Septemper 2010, he joined Singapore University of Technology and Design as an Assistant Professor. He is also a visiting scientist at MIT. Jun's research is in areas of software engineering and formal methods, in particular, formal specification, formal verification and formal synthesis. He has more than 40 publications, including articles in IEEE Trans. on SE and ACM Trans. on SE as well as papers in CAV, ICSE and FM.