`Would you tell me, please, which way I ought to go from here?'
`That depends a good deal on where you want to get to', said the cat.
`I don't much care where' said Alice.
`Then it doesn't matter which way you go', said the Cat.
`So long as I get somewhere, ' Alice added as an explanation.
`Oh, you're sure to do that,' said the Cat, `if you only walk long enough.'
- Alice's Adventures in Wonderland, Lewis Carroll

Currently, I am focusing on model checking techniques. I founded a model checker named Process Analysis Toolkit (PAT). PAT is more than one model checker supporting one modeling language. It is designed to support multi-languages. That is, given a new modeling language with syntax and (operational) semantics, the PAT can be quickly tuned to be a model checker for the new language. By far, PAT has served as an advanced model checker for CSP# (i.e. a modeling language designed for concurrent systems, which combines high-level process constructs with sequential programs), RTS (i.e. a modeling language designed for compositional real-time systems, which extends Timed CSP with data operations, additional timed process constructs, etc) and an abstract language for Web service orchestration and choreography. PAT has attracted more than 280 downloads from worldwide.

I am interested in becoming a lecture/assistant-professor somewhere on earth in the near future. Please contact me if you have information.

• Lee Kuan Yew Postdoctoral Fellowship 2007. National University of Singapore.
• Doctor of Philosophy 2006. National University of Singapore.
• Dean's Graduate Award 2005, School of Computing, National University of Singapore.
• Bachelor of Computing (with Honor), School of Computing, National University of Singapore, July 1998 - June 2002.
• Ministry of Education Scholarship, Singapore, 1997-2002.

1. [PDF, Bibtex] Chun Qing Chen, Jin Song Dong and Jun Sun A Verification Framework for Interval-based Specifications . ACM Transactions on Software Engineering and Methodology. Accepted. 
2. [PDF, Bibtex] Chun Qing Chen, Jin Song Dong and Jun Sun. A Formal Framework for Modeling and Validating Simulink Diagrams. Formal Aspects of Computing. Accepted.    
3. [PDF, Bibtex] Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun and Wang Yi. Timed Automata Patterns. IEEE Transactions on Software Engineering, vol. 34, no. 6, pp 844-859, Nov./Dec. 2008. 
4. [PDF, Bibtex] Jun. Sun and Jin Song Dong. Design Synthesis from Interaction and State-Based Specifications, IEEE Transactions on Software Engineering, vol. 32, no. 6, pp. 349-364, 2006.
5. [PDF, Bibtex] Jun. Sun, Yang Liu, Jin Song Dong and Jing Sun. Compositional Encoding for Bounded Model Checking, Frontiers of Computer Science in China, volume 2, number 4, papges 368-379, 2008.
6. [PDF, Bibtex] Yuan Fang Li, Jing Sun, G. Dobbie, Hai H. Wang and Jun Sun. Reasoning about ORA-SS Data Models using the Semantic Web, Journal of Data Semantics VII, Lecture Notes in Computer Science, Springer, 2006.
7. [PS, Bibtex] Yang Liu and Jun Sun, Algorithmic Design Using Object-Z for Twig XML Queries Evaluation. Electronic Notes in Theoretical Computer Science, vol 151, issue 2, pp. 107-124, May, 2006. An early version appeared at International Workshop on Web Languages and Formal Methods (WLFM'05).
8. [PDF, Bibtex] Hai H. Wang, Jin Song Dong, Jing Sun and Jun Sun, Reasoning Support for Semantic Web Ontology Family Languages Using Alloy. Multi-Agent and Grid Systems - An International Journal, vol. 2, no. 4, 2006. 

Refereed Conference Papers

9. [PDF, Bibtex] Jun Sun, Yang Liu, Jin Song Dong and Jun Pang. PAT: Towards Flexible Verification under Fairness. The 21th International Conference on Computer Aided Verification (CAV 2009), Grenoble, France, June 2009. Accepted.
10. [PDF, Bibtex] Yang Liu, Jun Pang, Jun Sun and Jianhua Zhao. Verification of Population Ring Protocols in PAT. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009). Tianjin, China. July 2009. Accepted.
11. [PDF, Bibtex] Jun Sun, Yang Liu, Jin Song Dong and Chun Qing Chen. Integrating Specification and Programs for System Modeling and Verification. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009). Tianjin, China. July 2009. Accepted.
12. [PDF, Bibtex] Shao Jie Zhang, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen and Yanhong A. Liu. Formal Verification of Scalable NonZero Indicators. The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE 2009). USA. Accepted.
13. [PDF, Bibtex] Chun Qing Chen, Jin Song Dong and Jun Sun. A Verification System for Timed Interval Calculus, The 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 2008.    
14. [Bibtex, Details] Yang Liu, Jun Sun and Jin Song Dong. An Analyzer for Extended Compositional Processes. ICSE Companion. Leipzig, Germany, May 2008.
15. [PDF, Bibtex] Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi and Xian Zhang. Specifying and Verifying Sensor Networks: an Experiment of Formal Methods. The 10th International Conference on Formal Engineering Methods (ICFEM 2008). Japan, Oct 2008.
16. [PDF, Bibtex] Jun Sun, Yang Liu, Jin Song Dong and Hai H. Wang. Specifying and Verifying Event-based Fairness Enhanced Systems. The 10th International Conference on Formal Engineering Methods (ICFEM 2008). Japan, Oct 2008.
17. [PDF, BibTex, Details] Jun Sun, Yang Liu and Jin Song Dong. CSP Model Checking Revisited: Introducing a Process Analysis Toolkit. The third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008), Greece, October 13-15, 2008.
18. [PDF, BibTex, Details] Jun Sun, Yang Liu, Jin Song Dong and Jing Sun. Bounded Model Checking of Compositional Processes. The 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), Nanjing, China, June 17-19, 2008. Note that the experimental results presented in this paper on FDR can be improved significantly with a slightly different modeling. 
19. [PDF, Bibtex] Stephen Wong, Jing Sun, Ian Warren and Jun Sun. A Scalable Approach to Multi-Style Architectural Modeling and Verification. The 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008), Belfast, Northern Ireland, 2008.
20. [PDF, Bibtex] Hai H. Wang and Nick Gibbins and Terry Payne and Ahmed Saleh and Jun Sun. A Formal Model of Semantic Web Service Ontology (WSMO) Execution. The 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008), Belfast, Northern Ireland, 2008.
21. [PDF, Bibtex] Chun Qing Chen, Jin Song Dong and Jun Sun. A Machine-Assisted Proof Support for Validation Beyond Simulink, The 9th International Conference on Formal Engineering Methods (ICFEM 2007), Florida, 2007.
22. [PDF, Bibtex] Hai H. Wang, Shen Chao Qin, Jun Sun, Jin Song Dong. Realizing Live Sequence Charts in SystemVerilog, The 1st IEEE & IFIP Theoretical Aspects of Software Engineering Conference (TASE 2007), Shanghai, Jun. 2007.
23. [PDF, Bibtex] H. Wang, N. Gibbins, T. Payne, A. Saleh and J. Sun. A Formal Semantics Model of the Semantic Web Service Ontology (WSMO),  The 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Jul. 2007.
24. [PDF, Bibtex] Jin Song Dong, Yu Zhang Feng, Jing Sun and Jun Sun, Context Awareness Systems Design and Reasoning. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (IEEE-ISoLA 2006), Cyprus, November, 2006.
25. [PDF, Bibtex] Jin Song Dong, Yang Liu, Jun Sun and Xian Zhang, Verification of Computation Orchestration via Timed Automata. 8th International Conference on Formal Engineering Methods (ICFEM'06), Macau, November 2006.
26. [PDF, Bibtex] Jin Song Dong, Ping Hao, Jun Sun and Xian Zhang, A Reasoning Method for Timed CSP based on Constraint Solving. 8th International Conference on Formal Engineering Methods (ICFEM'06), Macau, November 2006.
27. [PDF, Bibtex] Jin Song Dong, Yu Zhang Feng, Jing Sun and Jun Sun, Sensor Based Design for Smart Space. The First International Conference on Mobile Computing, Communications and Applications (ICMoCCA'06), Korean.
28. [PDF, Bibtex] Yuan Fang Li, Jing Sun, G. Dobbie, Jun Sun and Hai H. Wang, Validating Semistructured Data using OWL. The Seventh International Conference on Web-Age Information Management (WAIM 2006).
29. [PDF, Bibtex] Jin Song Dong, Yu Zhang Feng, Yuan Fang Li and Jun Sun,  A Tools Environment for Developing and Reasoning about Ontologies. 12th ASIA-PACIFIC Software Engineering Conference (APSEC 2005), Tai Bei, Tan Wan, December 2005.
30. [PDF, Bibtex] Jun Sun, Yuan Fang Li, Jing Sun and Hai Wang, Visualizing and Simulating Semantics Web Services Ontologies. 7th International Conference on Formal Engineering Methods (ICFEM'05), Manchester, United Kingdom, November 2005.
31. [PS, Bibtex, Details] Jun Sun and Jin Song Dong, Synthesis of Distributed Processes from Scenario-based Specifications. Formal Methods 2005 (FM'05), University of Newcastle upon Tyne, UK.
32. [PDF, Bibtex] Jun Sun and Jin Song Dong, Extracting FSMs from Object-Z Specifications with History Invariants. The 10th International Conference on Engineering of Complex Computer Systems (ICECCS'05), Shanghai, China. June 2005.
33. [PDF, Bibtex] Jun Sun and Jin Song Dong, Model Checking Live Sequence Charts. The 10th International Conference on Engineering of Complex Computer Systems (ICECCS'05), Shanghai, China. June 2005.
34. [PDF, Bibtex] Jin Song Dong, Ping Hao, Shen Chao Qin, Jun Sun and Yi Wang, Timed Patterns: TCOZ to Timed Automata. The 6th International Conference on Formal Engineering Methods (ICFEM'04), Seattle, WA, USA. Nov. 2004.
35. [PDF, Bibtex] Jin Song Dong, Shen Chao Qin and Jun Sun. Generating Message Sequence Charts from an Integrated Formal Specification Language. The 4th International Conference on Integrated Formal Methods (IFM'04), LNCS, Springer-Verlag, Canterbury, UK, April 2004.
36. [PDF, Bibtex] Jin Song Dong, Jun Sun, Hai H. Wang. C. H. Lee and H. B. Lee, Analyzing Semantic Web Ontology: A Military Case Study. The 15th International Conference on Software Engineering and Knowledge Engineering (SEKE'03), San Francisco, USA, July 2003.
37. [PDF, Bibtex] Jin Song Dong, Yuan Fang Li, Jing Sun, Jun Sun and Hai H. Wang. XML-based Static Type Checking and Dynamic Visualization for TCOZ. The 4th International Conference on Formal Engineering Methods (ICFEM'02), pages 311-322, Oct 2002.

Thesis

• [PDF, Bibtex, Details] Jun Sun, Complementary Formalisms - Synthesis, Verification and Visualization, Department of Computer Science, School of Computing, National University of Singapore, 2006.

*Copyright Notice. The documents distributed have been provided by the contributing authors as a means to ensure timely dissemination of technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, not withstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

• 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009)  
• 8th IEEE/ACIS International Conference on Computer and Information Science (ICIS 2009)
• First International Conference on Mobile Computing, Communications and Applications (ICMOCCA 2007)

Conference Attendance

• 30th International Conference on Software Engineering (ICSE 2008), May 2008, Leipzip, Germany.
• 2nd IEEE Theoretical Aspects of Software Engineering Conference (TASE 2008), June 2008, Nanjing, China.
• 9th International Conference on Formal Engineering Methods (ICFEM 2007), Nov 2007, Boca Raton, Florida, USA.
• First IEEE Theoretical Aspects of Software Engineering Conference (TASE 2007), June 2007, Shanghai, China.
• Formal Methods 2005 (FM 2005), July 2005, Newcastle, UK.
• 10th International Conference on Engineering of Complex Computer Systems (ICECCS 2005), June 2005, Shanghai, China.
• 4th International Conference on Integrated Formal Methods (IFM 2004), April 2004, Canterbury, Kent, UK.
• 5th International Conference on Formal Engineering Methods (ICFEM 2003), Nov 2003, Singapore.

Work Experience

• Jun 2007 - Present, Lee Kuan Yew Postdoc Fellow, National University of Singapore.
• Jun 2006 - May 2007, Research Fellow, National University of Singapore.
• Aug 2002 - May 2006, Research Assistant, National University of Singapore. Apply formal methods tools and methodologies to validate semantic web ontology.
• Software Engineer, Techron Integrated Systems Pte., Ltd, Singapore.  Build a web-based Facility Booking System using ASP and MS SQL Server.
• Part-time Teaching Assistant, National University of Singapore. Teach programming methodology (Java).

Technical Skills

• Specification Language: MSC/LSC, Statechart, UML, Z/Object-Z, CSP/Timed-CSP
• Programming Language: C#, SPEC#, Java, C/C++, Visual Basic, Prolog, TCL/TK, Ilog, SystemC, Verilog etc.
• System Design: Rational Rose (UML), Esterel Studio, Ptelomy, Rhapsody, etc.
• Web Development: XML, JavaScript, HTML, ASP, Perl.