Research Assistant Positions at Different Levels Available
I am currently looking for research assistants for the NSFC project "Model Checking Large-scale Probabilistic Concurrent Real-time Systems" at postdoc/PhD/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 2020.
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.
Dr. Jun Sun Visited Our Group
Dr. Jun Sun from SUTD visited our group and gave a talk "Compositional Verification of Programs " on December 6, 2016.
The answer to the question - how do we verify real programs - is perhaps already answered by how we develop programs. We know that already - abstraction, composition and hierarchy. In developing a big program, each time we focus on a component of the system and use it abstractly afterwards. In this work, we explore the idea of compositional verification which aims to do the same for verifying programs. The idea is of compositional verification is to focus on verifying one component at a time, and establish system-level property based on properties on the verified components. The challenges are twofold. Firstly, a component doesn't function on its own and thus how do we obtain minimum knowledge of the rest of the system so that the component can be verified? Secondly, how do we decide what the components are?
Prof. Zhiming Liu Visited Our Group
Prof. Zhiming Liu from SWU visited our group and gave a talk "Contract-based Model of Software Architecture in Emerging Systems " on November 21, 2016.
The sustainable development of most economies and the quality of life of their citizens largely depend on the development and application of evolutionary digital ecosystems. The characteristic features of these systems are reflected in the so called Internet of Things (IoT), Smart Cities, Cyber-Physical Systems (CPS), Systems of Human-Machine-Things, and Data Centers. Compared to the challenges in traditional ICT applications that engineers used to face, system and software development is to develop and integrate new components or subsystems, new applications and front end services that depends on the infrastructures of existing systems. This has to deal with the complexity of ever evolving architectures digital components, physical components, together with sensors and smart devices controlled and coordinated by software. The architectural components are designed with different technologies, run on different platforms and interact through different communication technologies. Software runs in these systems for data processing and analytics, computation, and intelligent control. However, the critical requirements of applications of these systems should not be compromised, and thus critical components need to be “provably correct”. In this talk we discuss, for development software in these emerging systems, the need of a foundation for the combination of traditional software engineering, AI (or knowledge-based engineering) and the emerging Big Data technologies. We show how an interface theory could play a core role in this foundation for seamless combination of different models, methods and tools for software development, AI and Big Data, as well as for system integration.
FM 2016 at Cyprus
The 21st International Symposium on Formal Methods was held in Cyprus in November, 2016.
The details about the conference can be found here.
FACS 2016 at Besançon, France
The 13th International Conference on Formal Aspects of Component Software was held in Besançon, France in October, 2016.
The component-based software development approach has emerged as a promising paradigm to cope with the complexity of present-day software systems by bringing sound engineering principles into software engineering. However, many challenging conceptual and technological issues still remain in component-/service-based software development theory and practice. Moreover, the advent of cloud computing, cyber-physical systems, and of the Internet of things has brought to the fore new dimensions, such as quality of service, reconfiguration and robustness to withstand inevitable faults, which require established concepts to be revisited and new ones to be developed in order to meet the opportunities offered by those architectures.
FACS 2016 is concerned with how formal methods can be used to make component-based and service-oriented software development succeed. Formal methods have provided a foundation for component-based software by successfully addressing challenging issues such as mathematical models for components, composition and adaptation, or rigorous approaches to verification, deployment, testing, and certification.
The details about the conference can be found here.
Reasoning about Connectors in Coq
The paper "Reasoning about Connectors in Coq" by Zhang Xiyue, Hong Weijiang, Li Yi and Sun Meng has been accepted by FACS 2016, which will be held at Besancon, France, October 19-21, 2016.
Reo is a channel-based coordination model in which complex coordinators, called connectors, are compositionally built out of simpler ones. In this paper, we present a new approach to model connectors in Coq which is a proof assistant based on higher-order logic and lambda-calculus. The model reflects the original structure of connectors simply and clearly. In our framework, basic connectors (channels) are interpreted as axioms and composition operations are specified as inference rules. Furthermore, connectors are interpreted as logical predicates which describe the relation between inputs and outputs. With such definitions provided, connector properties, as well as equivalence and refinement relations between different connectors, can be naturally formalized as goals in Coq and easily proved using pre-defined tactics.
Towards Concolic Testing for Hybrid Systems
The paper "Towards Concolic Testing for Hybrid Systems" by Kong Pingfan, Li Yi, Chen Xiaohong, Sun Jun, Sun Meng and Wang Jingyi has been accepted by FM 2016, which will be held in Cyprus, November 7-11, 2016.
Hybrid systems exhibit both continuous and discrete behavior. Analyzing hybrid systems is known to be hard. Inspired by the idea of concolic testing (of programs), we investigate whether we can combine random sampling and symbolic execution in order to effectively verify hybrid systems. We identify a sufficient condition under which such a combination is more effective than random sampling. Furthermore, we analyze different strategies of combining random sampling and symbolic execution and propose an algorithm which allows us to dynamically switch between them so as to reduce the overall cost. Our method has been implemented as a web-based checker named HyChecker. HyChecker has been evaluated with benchmark hybrid systems and a water treatment system in order to test its effectiveness.
TASE 2016 at Shanghai, China
The 10th International Symposium on Theoretical Aspects of Software Engineering was held in Shanghai, China in July, 2016.
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.
2016 Autumn Seminar
The group seminar in 2016 Autumn term will be held every Tuesday, 13:00-15:00.
Details about the seminar schedule can be found here.
Yiwu Wang has Finished her Thesis Defense Successfully
Yiwu has successfully defended her master thesis on June 3. Congratulations!
Active Learning from Blackbox to Timed Connectors
The paper "Active Learning from Blackbox to Timed Connectors" by Li Yi, Sun Meng and Wang Yiwu has been accepted by TASE 2016, which will be held in ECNU, Shanghai, China, July 17-19, 2016.
Coordination models and languages play a key role in formally specifying the communication and interaction among different components in large-scale distributed and concurrent systems. In this paper, we propose an active learning framework to extract timed connector models from black-box system implementation. We first introduce parameterized Mealy machine(PMM) as an operational semantic model for channelbased coordination language Reo. PMM serves as a bridge between Reo connectors and Mealy machines. With the product operator, complex connectors can be constructed by joining basic channels and the PMMs of connectors can be transformed into Mealy machines. Moreover, we adapt L*, a well-known learning algorithm, to timed connectors (in the form of Mealy machines). The new algorithm has shown its efficiency in multiple case studies. This framework has been implemented in Golang.
2016 Spring Seminar
The group seminar in 2016 Spring term will be held every Tuesday, 13:00-15:00.
Details about the seminar schedule can be found here.