Research Assistant Positions at Different Levels Available for COSMOS and MONDAY

I am currently looking for research assistants for the COSMOS and MONDAY projects at both PhD and master level. The key criteria for the RA positions include good mathematical background and / or programming skills. The positions are available until the end of 2015.
Undergraduate students from mathematics / computer science / information science or other related disciplines are also welcome to join my group for internship of research. Please feel free to contact me.
LEDS 2014 at Guilin, China

LEDS 2014 is held at Guilin University of Electronic Technology, Guilin, China, Nov. 13-15, 2014. The symposium brings together researchers and engineers from both academia and industry in China to present and discuss their work in dependable software engineering. The detailed programme can be found here.
Formal Modeling and Verification of Complex Interactions in E-Government Applications

The paper "Formal Modeling and Verification of Complex Interactions in E-Government Applications" by Sun Meng and Li Yi has been accepted by ACM ICEGOV 2014, which will be held in Guimarães, Portugal, October 27-30, 2014.
With the dramatic transformation of society and the increasing size of government information resources, proper modeling and verification techniques for designing large-scale distributed electronic government (E-Government) applications to make them trustworthy, secure and efficient are playing a key role in the development of such applications. This paper focuses on using the integration of a promising coordination modeling framework Reo and the proof assistant Coq for modeling and verification of complex interactions in E-Government applications. An access control example is investigated to show our approach on modeling, simulating and verifying the dynamic behavior of E-Government applications.
Ocean University of China and Qingdao University, July 2014

Sun Meng visited College of Information Science and Engineering, Ocean University of China, and College of Information Engineering, Qingdao University in July 2014.
The visit was hosted by Prof. Li Jinhua at Qingdao University and Prof. Xu Jinliang at Ocean University of China.
FSEN 2015 at Tehran, Iran

FSEN is an international conference that aims to bring together researchers, engineers, developers, and practitioners from the academia and the industry to present and discuss their research work in the area of formal methods for software engineering. This conference seeks to facilitate the transfer of experience, adaptation of methods, and where possible, foster collaboration among different groups. The topics of interest cover all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry and promoting their integration with practical engineering techniques. Following the success of the previous FSEN editions, the next edition of the FSEN conference will take place in Tehran, Iran, April 22-24, 2015.
The dates for abstract and paper submissions are Oct. 24 and 31, 2014.
FOCLASA 2014 at Rome, Italy

The 13th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems will be held at Rome, Italy, September 6, 2014.
Modern software systems are distributed, concurrent, mobile, and often involve composition of heterogeneous components and stand-alone services. Service coordination and self-adaptation constitute the core characteristics of distributed and service-oriented systems. Coordination languages and formal approaches to modelling and reasoning about self-adaptive behaviour help to simplify the development of complex distributed service-based systems, enable functional correctness proofs and improve reusability and maintainability of such systems.
This year the workshop will be collocated with the 25th International Conference on Concurrency Theory, CONCUR 2014.
FACS 2014 at Bertinoro, Italy

The 11th International Symposium on Formal Aspects of Component Software will be held at Bertinoro, Italy, September 10-12, 2014.
This year the symposium will be co-located with the 11th International Conference on Integrated Formal Methods, iFM 2014.
ICFEM 2014 at Luxembourg

Since 1997, ICFEM has provided a forum for those interested in the application of formal engineering methods to computer systems. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, and to help advance the state of the art. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical, tangible benefit.
The goal of this conference is to bring together industrial, academic, and government experts, from a variety of user domains and software disciplines, to help advance the state of the art. Researchers, practitioners, tool developers and users, and technology transition experts are all welcome. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical, tangible as well as engineering benefit.
The conference will be held in Luxembourg, November 3-7, 2014.
IHMSC 2014 at Hangzhou, China

The 6th International Conference on Intelligent Human-Machine Systems and Cybernetics (IHMSC 2014) will take place at Zhejiang University in Hangzhou, China, August 26-27, 2014. The aim of this conference is to provide a forum for exchanges of research results, ideas for and experience of application among researchers and practitioners involved with all aspects of Human-Machine Systems and Cybernetics.
Two Students Visited Singapore University of Technology and Design, 2014

Two students in our group, Chen Xiaohong and Li Yi visited Singapore University of Technology and Design in 2014.
Both visits were hosted by Dr. SUN Jun at SUTD.
2014 Autumn Seminar
The group seminar in 2014 Autumn will be mainly focused on the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen.
Details about the seminar schedule can be found here.
A Hybrid Model of Connectors in Cyber-Physical Systems

The paper "A Hybrid Model of Connectors in Cyber-Physical Systems" by Chen Xiaohong, Sun Jun and Sun Meng has been accepted by ICFEM 2014, which will be held in Luxembourg, November 3-7, 2014.
Compositional coordination models and languages play an important role in cyber-physical systems (CPSs). In this paper, we introduce a formal model for describing hybrid behaviors of connectors in CPSs. We extend the constraint automata model, which is used as the semantic model for the exogenous channel-based coordination language Reo, to capture the dynamic behavior of connectors in CPSs where the discrete and continuous dynamics co-exist and interact with each other. In addition to the formalism, we also provide a theoretical compositional approach for constructing the product automata for a Reo circuit, which is typically obtained by composing several primitive connectors in Reo.
Model Checking Business Processes for Web Service Composition in mCRL2

The paper "Model Checking Business Processes for Web Service Compositions in mCRL2" by Sun Meng, Li Shaodong and Ou Yufei has been accepted by IHMSC 2014, which will be held in Hangzhou, August 26-27, 2014.
BPEL has emerged as the de facto industry standard for composing web services. In this paper, we focus on a core subset of BPEL, called BPEL*, and provide a set of rules for translating BPEL* into the process algebra language mCRL2, which can be used to verify properties of BPEL processes. An employee travel arrangement example is provided to show our approach.
2014 Spring Seminar

The group seminar in 2014 Spring term is focused on the book "Concurrency Theory" by Howard Bowman and Rodolfo Gomez.