Research Assistant Positions at Different Levels Available
I am currently looking for research assistants for the NSFC projects "Formal Modeling and Verification of Complex Concurrent Behavior in Cyber-Physical Systems" and "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.
ICFEM 2018 at Gold Coast, Australia
The 20th International Conference on Formal Engineering Methods (ICFEM 2018) was held in Gold Coast, Australia on November 12-16, 2018. The Conference was chaired by Sun Jing (University of Auckland), and Sun Meng (Peking University).
Li Yi and Zhang Xiyue gave two talks "Component-based Formal Engineering in Mediator" and "Modeling and Verification of Component Connectors" at the Doctoral Symposium of ICFEM 2018.
Li Yi gave another talk "On Semantics for Mediator: A Coalgebraic Perspective" at the 8th International Workshop on SOFL+MSVL for Reliability and Security, which was co-located with ICFEM 2018, on November 16.
More details can be found here.
FMAC 2018 and YR-FMAC 2018 at Chongqing, China
The 3rd Colloquium on Formal Methods and Applications (FMAC 2018) and the Chinese Forum on Formal Methods for Young Researchers (YR-FMAC 2018) was held together in Chongqing, China on November 3-4, 2018.
The paper "Automatic Generation of SystemC Codes from Mediator" by Zhang Qi, Li Yi and Sun Meng was accepted by FMAC 2018 and Zhang Qi gave the oral presentation.
Li Yi and Zhang Xiyue gave two talks "Component-based Formal Engineering in Mediator" and "Modeling and Verification of Component Connectors" at YR-FMAC 2018, both are extended abstracts of the paper accepted by Doctoral Symposium at ICFEM 2018. The talk given by Li Yi on "Component-based Formal Engineering in Mediator" was awarded as the best presentation at YR-FMAC 2018.
More details can be found here.
Prof. Hamideh Afsarmanesh Visited Our Group
Prof. Hamideh Afsarmanesh from University of Amsterdam visited our group and gave a talk "Semi-automated Software Service Integration in Virtual Organizations" on October 19, 2018.
To enhance business opportunities, organizations involved in many service industries are increasingly active in pursuit of both on-line provision of their business services and collaborating with others. Collaborative networks of organizations in service industry sector, however, face many challenges when it comes to sharing and especially integration of their shared business services, and corresponding software services. Catering to the need for a service interoperability framework has therefore gained momentum in research for supporting Virtual Organizations (VOs). Central to such a framework, is the requirement to support generation of formal machine-readable specification for shared business processes. Such business process specifications provide the unambiguous definitions needed for developing their counterpart software services.
A main contribution of our research involves providing concise representations for functional behavior of services, as well as applying user specified/desired service behavior for the purpose of automated matchmaking/selection of existing services in the VO breeding environment (VBE). Our proposed framework provides both a model and an implementation architecture for provision and discovery, as well as for composition of shared services. As such, it supports semi-automated development of integrated value-added services in VOs. Automated selection of most suitable service(s) incorporates service quality a spects. Service integration/composition approach applies the VO business service model, further to deploying Reo circuits and ECT tools to define complex interaction protocols and coordination among business processes that are provided by different organizations.
Details of the talk can be found here.
Prof. Farhad Arbab Visited Our Group
Prof. Farhad Arbab from Leiden University and CWI visited our group and gave a mini-course "Interaction by Composition" on October 10 and 17, 2018.
Programming language constructs and abstractions, along with techniques for their efficient compilation, have dramatically advanced in the last half-century, to the extent that today we can program at the level of (parametric) types, classes, objects, mathematical functions, monads, or Horn clauses, when appropriate, and obtain executable code whose performance competes with---indeed often beats---that of code written by competent programmers in some low-level language. Protocols constitute an equally significant abstraction in specification of concurrent applications as do functions, types, and other computational constructs, and their concrete implementation has an equally significant impact on performance and scalability of an application as that of any high-level computational construct.
In spite of significant advances in concurrency theory, constructs and models for programming of concurrent applications have essentially stagnated in the past half-century. In contrast to advances in abstractions and constructs for sequential programming, no real abstract protocol constructs have evolved. Consequently, programmers today use the same cumbersome, error-prone concurrency constructs to express protocols in modern software as they did 50 years ago: processes, threads, locks, semaphores, monitors, rendezvous, etc. The unavailability of high-level protocol constructs in contemporary programming languages hampers full utilization of the enormous potential offered by massively parallel hardware platforms in real-life applications.
In this course, we describe an interaction-centric model of concurrency that turns interaction protocols into concrete first-class mathematical objects, expressed as relations that constrain communication actions of their engaged processes. This model serves as the formal foundation for a domain-specific language (DSL), called Reo, for programming concurrency protocols. A protocol in Reo manifests itself as a connector. Complex connectors result from direct composition of simpler ones, which in turn comprise of a network of primitive binary connectors, called channels. In Reo, interaction protocols become explicit, concrete, tangible pieces of software that can be specified, verified, composed, and reused, independently of the actors that they may engage in various applications. We explore different formal semantics of Reo, its various software development support tools, and discuss compilation and optimization techniques for generating efficient executable code from high-level protocol specifications in Reo.
Details of the talk can be found here.
Dr. Renato Neves Visited Our Group
Dr. Renato Neves from Minho University visited our group and gave a talk "Compositional Semantics for New Paradigms: Probabilistic, Hybrid and Beyond" on September 12, 2018.
We introduce a generic framework to systematically investigate the features of a given computational paradigm and its possible extensions. Our motivating examples are probabilistic and hybrid programming, two recent paradigms that combine atypical primitive operations – e.g. systems of differential equations, Bernoulli trials, wait calls – with classical program constructs. By applying our framework to these two cases we list all binary program operations they possess, and show precisely when and if important axioms, such as commutativity and idempotency, hold. We also examine the possibility of incorporating notions of failure and non-determinism: we show that it is possible to combine hybrid computations with non-deterministic ones via a suitable distributive law, and that there is no monad structure on PD (the composition of the powerset functor P with the finitely supported distribution functor D) whatsoever.
Details of the talk can be found here.
Prof. Bernhard Aichernig Visited Our Group
Prof. Bernhard Aichernig from TU Graz visited our group and gave a talk "Smart Black-box Testing - Combining Model Learning and Model-based Testing" on September 10, 2018.
Testing has always been a challenge due to (1) its incompleteness by nature, (2) the lack of good specifications and (3) by its high demand for resources. With the growing complexity of the systems-under-test the situation is not likely to improve. The combination of model-learning with model-based testing offers an opportunity to master this complexity. In my talk I will introduce this line of research and report about our recent results including applications in the Internet of Things. We will cover the learning and testing of several classes of models/systems including Mealy machines, Markov decision processes and timed automata. Our goal is a natural evolution of testing: with the trend of our environment becoming "smarter", e.g. smart homes, smart cars, smart production, smart energy, our testing process needs to become smart as well. We are seeing the advent of smart testing.
Details of the talk can be found here.
FORMATS 2018 at Beijing, China
The 16th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2018) was held at Beijing, China from September 4 to September 6, 2018, Co-located with CONCUR 2018, QEST 2018, SETTA 2018 and several workshops (see CONFESTA website for more detals).
The paper "A Relational Model for Probabilistic Connectors Based on Timed Data Distribution Streams" by Meng Sun and Xiyue Zhang was accepted by the conference.
Details of the conference can be found here.
LEDS 2018 at Yinchuan, China
The Colloquium on Logic in Engineering Dependable Software (LEDS 2018) was held in Yinchuan, China on August 17-20, 2018.
Meng Sun and Xiyue Zhang gave two talks "Using Coq and RNN to Model and Verify Connectors" and "Modeling and Verification of Probabilistic Connectors" at the colloquium.
FMSES 2018 at Xining, China
The 2018 Workshop on Foundations and Methods for Software in Emerging Systems (FMSES 2018) was held in Xining, China on August 6-26, 2018.
The workshop has three seminar series:
Week1: Software Engineering Meets AI
Week 2: Blockchain
Week 3: Software Engineering for Distributed Systems
Meng Sun gave a talk "Using Coq and RNN to Model and Verify Connectors" at the workshop.
SEKE 2018 at Redwood City, San Francisco Bay, California, USA
The 30th International Conference on Software Engineering and Knowledge Engineering (SEKE 2018) was held at Redwood City, San Francisco Bay, California, USA from July 1 to July 3, 2018.
Three papers from our group were accepted by the conference:
"Modeling and Verification of IEEE 802.11i Security Protocol for Internet of Things" by Yuteng Lu and Meng Sun
"Reo2PVS: Formal Specification and Verification of Component Coneectors" by M.Saqib Nawaz and Meng Sun
"Towards Formal Modeling and Verification of Probabilistic Connectors in Coq" by Xiyue Zhang and Meng Sun
Details of the conference can be found here.
"It's All About Coordination" at Amsterdam, the Netherlands
On May 25 2018, CWI organizes a symposium celebrating the lifelong scientific achievements of Prof. Farhad Arbab on the occasion of his retirement from CWI, "It's All About Coordination". Meng Sun gave an invited speech "Tons of Fun in a Zodiac Cycle" at the event.
A book collecting a number of papers by several of Farhad's close collaborators has been published by Springer, which can be found here.
Generating Arduino C Codes from Mediator
The paper "Generating Arduino C Codes from Mediators" by Li Yi and Sun Meng has been published in "It's all about coordination: Essays to celebrate the lifelong scientific achievements of Farhad Arbab", LNCS 10865, 2018.
Manual encoding is exceedingly time consuming and error prone, and has become a huge obstacle between reliable software models and trustworthy computer programs. To deal with this problem, dozens of code generators are developed to automatically convert different models into executable codes. In this paper we present a new code generator for the component-based modeling language Mediator. It aims to generate platform-dependent (Arduino in this case) programs that can be directly downloaded to the hardware without any manual adaption. We also present a case study where we use Mediator to develop a wheeled-robot controller, generate the corresponding program through our code generator, which has been successfully executed on an Arduino-based robot platform.
Dr. Bohua Zhan Visited Our Group
Dr. Bohua Zhan from TU Munich visited our group on April 26, 2018 and gave a talk "Auto2 prover in Isabelle and its application to program verification". Details of the talk can be found here.
Dr. Gaogao Yan Visited Our Group
Dr. Gaogao Yan from ISCAS visited our group on April 11, 2018 and gave a talk "Synthesizing SystemC Code from Delay Hybrid CSP".
Prof. Yongwang Zhao Visited Our Group
Prof. Yongwang Zhao from BUAA visited our group on March 21, 2018 and gave a talk "Formal Verification of Safety-Critical Operating Systems". Details of the talk can be found here.
2018 Seminar
The group seminar in 2018 will be held every Wednesday, 13:00-15:00.
Details about the seminar schedule can be found here.