`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

• System Requirement Specification. The problem  is how to state the system requirements in a non-ambiguous and intuitive way. The specification/modeling notations and languages that I have been working with include Unified Modeling Language (UML), (Harel's) Statecharts, Message Sequence Charts, Live Sequence Charts, the Z language, Object-Z, Communicating Sequential Processes (CSP), Timed CSP, Timed Automata, Timed Communicating Object-Z, etc. 
• System Analysis. The problem how to automatically (or semi-automatically) reveal inconsistency in the system specification/design. The techniques that I have been working with include model checking (on-the-fly explicit model checking, bounded model checking, etc.) and theorem proving.
• System Synthesis. The problem is to automatically synthesize prototypes from a given system specification which guarantees satisfaction of critical properties. I have been working with sequence diagrams (in particular, Live Sequence Charts) in this part.

The application domains of my research include reactive systems, embedded systems, semantic web and web services and lately wireless sensor networks. Besides paper writing, I also developed a number of tools to realize some of my research ideas (useful at certain extent). Check out my publication list or the following website (i.e., an analyzer which is being actively developed).

• Process Analysis Toolset (PAT)

• 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.

• C. Q. Chen, J. S. Dong and J. Sun. A Verification System for Timed Interval Calculus, The 30th International Conference on Software Engineering (ICSE 2008), Germany, 2008. Accepted.
• C. Q. Chen, J. S. Dong and J. Sun. A Machine-Assisted Proof Support for Validation Beyond Simulink, The 9th International Conference on Formal Engineering Methods (ICFEM 2007), Florida, 2007. PDF.Bibtex.
• H. Wang, S. C. Qin, J. Sun, J. S. Dong. Realizing Live Sequence Charts in SystemVerilog, The 1st IEEE & IFIP Theoretical Aspects of Software Engineering Conference (TASE 2007), Shanghai, Jun. 2007. 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. PDF, Bibtex.
• J. 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, Jun. 2006. PDF, Bibtex
• Y. F. Li, J. Sun, G. Dobbie, H. Wang and J. Sun. Reasoning about ORA-SS Data Models using the Semantic Web, Journal of Data Semantics VII, Lecture Notes in Computer Science, Springer, 2006. PDF, Bibtex
• Y. Liu and J. 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). PS, Bibtex
• H. Wang, J. S. Dong, J. Sun and J. Sun, Reasoning Support for Semantic Web Ontology Family Languages Using Alloy. Multi-Agent and Grid Systems - An International Journal, vol. 2, no. 4, 2006. PDF, Bibtex
• J. S. Dong, Y. Z. Feng, J. Sun and J. Sun, Context Awareness Systems Design and Reasoning. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (IEEE-ISoLA 2006), Paphos, Cyprus, November, 2006. PDF, Bibtex
• J. S. Dong, Y. Liu, J. Sun and X. Zhang, Verification of Computation Orchestration via Timed Automata. 8th International Conference on Formal Engineering Methods (ICFEM'06), Macau, November 2006. PDF, Bibtex
• J. S. Dong, P. Hao, J. Sun and X. Zhang, A Reasoning Method for Timed CSP based on Constraint Solving. 8th International Conference on Formal Engineering Methods (ICFEM'06), Macau, November 2006. PDF, Bibtex
• J. S. Dong, Y. Z. Feng, J. Sun and J. Sun, Sensor Based Design for Smart Space. The First International Conference on Mobile Computing, Communications and Applications (ICMoCCA'06), Korean. PDF, Bibtex
• Y. F. Li, J. Sun, G. Dobbie, J. Sun and H. Wang, Validating Semistructured Data using OWL. The Seventh International Conference on Web-Age Information Management (WAIM 2006). PDF, Bibtex
• J. S. Dong, Y. Z. Feng, Y. F. Li and J. Sun,  A Tools Environment for Developing and Reasoning about Ontologies. 12th ASIA-PACIFIC Software Engineering Conference (APSEC 2005), Tai Bei, Tan Wan, December 2005. PDF, Bibtex
• J. Sun, Yuan Fang Li, J. 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. PDF, Bibtex
• J. Sun and J. S. Dong, Synthesis of Distributed Processes from Scenario-based Specifications. Formal Methods 2005 (FM'05), University of Newcastle upon Tyne, UK. PS, Bibtex
• J. Sun and J. S. 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. PDF, Bibtex
• J. Sun and J. S. Dong, Model Checking Live Sequence Charts. The 10th International Conference on Engineering of Complex Computer Systems (ICECCS'05), Shanghai, China. June 2005. PDF, Bibtex
• J. S. Dong, P. Hao, S. C. Qin, J. Sun and Y. Wang, Timed Patterns: TCOZ to Timed Automata. The 6th International Conference on Formal Engineering Methods (ICFEM'04), Seattle, WA, USA. Nov. 2004. PDF, Bibtex
• J. S. Dong, S. C. Qin and J. 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. PDF, Bibtex
• J. S. Dong, J. Sun, 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. PDF, Bibtex
• J. S. Dong, Y. F. Li, J. Sun, J. Sun and 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. PDF, Bibtex

Tools

• J. S. Dong, X. Zhang, J. Sun and P. Hao. Reasoning About Timed CSP Models. Formal Methods 2006.

Thesis

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

• Web Master of 4^th International Conf. on Formal Engineering Methods (ICFEM`03).
• Session Chair of 4<sup>th</sup> International Conf. on Complex Computer Systems (ICECCS'05).
• International Referee of FAC, SOSYM,CORDIE'06, ICECCS'06, ACSC05, TSE, ICTAC'05, WLFM'05, FORTE'05, SEFM'05, SEKE'05, FME'05, SEKE'05, ZB'05, ASWEC'05, SEFM`04, ICFEM`03, APSEC`03, ATVA`03, ICECCS `04, IFM`04, ICFEM`04, ATVA'04, APSEC'04, ISoLA'04, ICDCIT'04.
• Attended ICFEM'03, IFM'04, ICECCS'05, FM2005, ICFEM 2007, TASE 2007.

Work Experience

• Research Fellow, National University of Singapore (Present).
• Software Engineer, Techron Integrated Systems Pte., Ltd, Singapore.  Build a web-based Facility Booking System using ASP and MS SQL Server.
• Research Assistant, National University of Singapore. Apply formal methods tools and methodologies to validate semantic web ontology.
• 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: 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.

• My Online Album.
• Everything about me.

People

• My advisor's Homepage.
• Yuan Fang Li's Homepage.
• Jing Sun's Homepage.
• Hai Wang's Homepage.

Works

• PhD Thesis.
• Verifying and Synthesis of Live Sequence Charts.