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.
Modeling and Verification of Component Connectors in Coq
The paper "Modeling and Verification of Component Connectors in Coq" by Li Yi and Sun Meng has been published in Science of Computer Programming. vol. 113(3), pages 285-301, 2015. This is an extended version of our FACS 2013 paper.
Connectors have emerged as a powerful concept for composition and coordination of concurrent activities encapsulated as components and services. Compositional coordination languages, like Reo, serve as a means to formally specify and implement connectors. They support large-scale distributed applications by allowing construction of complex component connectors out of simpler ones. In this paper, we present a new approach to modeling and verification of Reo connectors via Coq, a proof assistant based on higher-order logic and λ-calculus. Basic notions in Reo, like nodes and channels, are defined by inductive types. By tracing the data streams, we provide a method for simulation of the behavior and output of a given Reo connector. With input constraints specified, connectors' properties can be proved by induction. Furthermore, properties specified in LTL can be verified using a simulation-based model-checking approach. An access control system is investigated to show our approach.
Prof. Jos Baeten Visited Our Group
Prof. Jos Baeten from CWI visited our group and gave a talk "Computability Revisited" on December 22, 2015.
Classical computability theory disregards runtime interaction completely. The strong Church-Turing thesis states that anything a computer can do can also be done by a Turing machine, given enough time and memory. This thesis is invalidated by e.g. a self-driving car, as all possibly crossing pedestrians cannot be put on the Turing tape before starting, and resulting actions cannot be postponed until after finishing. Concurrency theory gives us a proper treatment of interaction. The talk surveys what happens when computability theory is integrated with concurrency theory, which theorems remain valid and which theorems should be adapted. The Reactive Turing Machine is introduced as a model of computability with interaction.
Dr. Leslie Lamport Visited PKU
Dr. Leslie Lamport (2013 Turing Award winner) visited PKU and gave a talk "Programming should be more than coding" at Stanford center on October 30, 2015. Details can be found here.
Prof. Holger Hermanns Visited Our Group
Prof. Holger Hermanns from Saarland University visited our group and gave two talks "Concurrent Programming Education in the Post-Java Era" and "How Good is Your Embedded Design, if at all?" on October 20, 2015.
Dr. Guangdong Bai Visited Our Group
Dr. Guangdong Bai visited our group from September15 to October 15, 2015 and gave a talk "Extracting Model from Implementations of Web Authentication Protocols" on October 13, 2015.
Dr. Bai is a research fellow at National University of Singapore. His research interests mainly focus on Formal Methods on Security, Mobile Security, Web Security, and System Security.
Towards a Coalgebraic Semantics of Behavioral Adaptation in Component-based Software Systems
The paper "Towards a coalgebraic semantics of behavioral adaptation in component-based systems" by Sun Meng has been accepted by CSMA 2015, which will be held in Hangzhou, China, November, 2015.
In this paper we present a coalgebraic model for behavioral adaptation in component-based systems. Bisimulation equivalence and refinement relationship are used to ensure that a component can replace another one. When the behavior of two components can not be matched perfectly, behavioral adaptation might be used to allow substitution of components. In this case, bisimulation is not enough to fit our purposes and a natural transformation between the behavioral functors for components is necessary for behavioral adaptation.
2015 Autumn Seminar
The group seminar in 2015 Autumnterm will be held every Tuesday, 13:00-15:00.
Details about the seminar schedule can be found here.
A Framework for Off-Line Conformance Testing of Timed Connectors
The paper "A Framework for Off-Line Conformance Testing of Timed Connectors" by Li Shaodong, Chen Xiaohong, Wang Yiwu and Sun Meng has been awarded as the best paper at TASE 2015, which was held in Nanjing, China, September 12-14, 2015.
Coordination is playing a key role in complex cyberphysical systems (CPSs). The complexity and importance of coordination models and languages for CPSs necessarily lead to a higher relevance of testing during development of CPSs. Model based testing is a promising technology to test the conformance or non-conformance relation between the implementation-under-test (IUT) and its specification. In this paper, we present an approach to test the conformance relation tiococ(Timed Input-Output Conformance) between the implementation of a timed Reo connector and its specification given by a timed constraint automaton (TCA). An algorithm to generate test cases from a TCA is proposed and the testing approach is implemented in UPPAAL.
TASE 2015 at Nanjing, China
The 9th International Symposium on Theoretical Aspects of Software Engineering will be held in Nanjing, China in September, 2015.
Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to the various aspects of software engineering, for instance, software dependability in trusted computing, interaction with physical components in cyber physical systems, distribution in cloud computing applications, etc. Hence, new concepts and methodologies are required to enhance the development of software engineering from theoretical aspects. TASE 2015 aims to provide a forum for people from academia and industry to communicate their latest results on theoretical advances in software engineering.
The details about the conference can be found here.
LEDS 2015 at Xi'an
The 5th Colloquium on Logic in Engineering Dependable Software，LEDS2015 was held in Xi'an, China in September, 2015. This year the colloquium was chaired by Prof. Zhenhua Duan and Prof. Yunwei Dong.
Details about the conference can be found here.
FOCLASA 2015 at Madrid, Spain
The 14th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems will be held at Madrid， Spain, September 5, 2015.
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 26th International Conference on Concurrency Theory, CONCUR 2015.
Li Shaodong Visited Singapore University of Technology and Design, 2015
A student in our group, Mr. Li Shaodong visited Singapore University of Technology and Design in 2015.
The visit was hosted by Dr. SUN Jun at SUTD.
2015 Spring Seminar
The group seminar in 2015 Spring term will continue on the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen.
Details about the seminar schedule can be found here.