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.
SBMF 2017 at Recife-Pe, Brazil
The 20th Brazilian Symposium on Formal Methods (SBMF 2017) was held in Recife-Pe, Brazil on November 29-December 1, 2017.
The work "Capturing Stochastic and Real-Time Behavior in Reo Connectors" by Yi Li, Xiyue Zhang, Yuanyi Ji and Meng Sun got the Best Paper Award (1st Place) at the symposium.
LEDS 2017 at Haikou, China
The Colloquium on Logic in Engineering Dependable Software (LEDS 2017) was held in Haikou, China on November 25-26, 2017.
Yi Li gave a talk on component based modeling in Mediator at the colloquium.
Dr. Gang Chen Visited Our Group
Dr. Gang Chen from CASIC visited our group on November 8, 2017 and gave a talk "Formalized Engineering Mathematics and the Next Generation of Artificial Intelligence". Details of the talk can be found here.
Prof. Fei He Visited Our Group
Prof. Fei He from Tsinghua University visited our group on November 3, 2017 and gave a talk "PSpec-SQL：Enabling Fine-Grained Control for Distrubuted Data Analytics". Details of the talk can be found here.
MAVeLoS 2017 at Beijing, China
The PKU International Workshop on Modeling, Analysis and Verification of Large-Scale Complex Systems was held in Beijing, China on October 7-8, 2017.
Details of the workshop can be found here.
Prof. Luis Barbosa Visited Our Group
Prof. Luis Barbosa from Minho University visited our group from September 28 to October 8, 2017 and gave a talk "Formal Modeling in Software Design". Details of the talk can be found here.
Capturing Stochastic and Real-time Behavior in Reo Connectors
The paper "Capturing Stochastic and Real-time Behavior in Reo Connectors" by Li Yi, Zhang Xiyue, Ji Yuanyi and Sun Meng has been accepted by SBMF 2017, which will be held in Recife-Pe, Brazil on November 29-December 1, 2017.
Modern distributed systems are often coupled with flexible architectures, composed of heterogenous components, and deployed on different execution nodes. Under such frameworks, connectors (or middlewares) are widely used to organize the separated components and make them functioning. Apparently, reliability of such systems highly depends on the correctness of their connectors. Reo is a channel-based coordination language where complex connectors are constructed from simpler ones through a compositional approach. In this paper, we propose a stochastic and real-time extension of Reo, including a set of new primitive channels and an expressive semantics named Stochastic Timed Automata for Reo (STAr). With the support of STAr, different coordination scenarios in existing Reo extensions can be easily encoded, integrated, and analyzed.
Prof. Zhiping Shi Visited Our Group
Prof. Zhiping Shi from Capital Normal University visited our group on September 20, 2017 and gave a talk "Formalization of Mathematics in Engineering". Details of the talk can be found here.
FOCLASA 2017 at Trento, Italy
The 15th International Workshop on Foundations of Coordination Languages and Self-Adaptative Systems was held in Trento, Italy, in September, 2017.
The details about the conference can be found here.
Dr. Yu Pei Visited Our Group
Dr. Yu Pei from the Hong Kong Polytechnic University visited our group on August 7, 2017 and gave a talk "Contract-based Automated Software Testing". Details of the talk can be found here.
Zhang Xiyue Visited Singapore University of Technology and Design, 2017
A student in our group, Ms. Zhang Xiyue visited Singapore University of Technology and Design in August 2017.
The visit was hosted by Dr. SUN Jun at SUTD.
CAP Workshop at Heidelberg, Germany
The China-Germany bilateral project CAP workshop was held in Heidelberg, Germany, in July, 2017. The PhD students Yi Li and Xiyue Zhang gave two presentations at the workshop.
SEKE 2017 at Pittsburgh, USA
The 29th International Conference on Software Engineering & Knowledge Engineering was held in Pittsburgh, USA, in July, 2017.
The details about the conference can be found here.
Component-Based Modeling in Mediator
The paper "Component-Based Modeling in Mediator" by Li Yi and Sun Meng has been accepted by FACS 2017, which will be held in Braga, Portugal, October 10-13, 2017.
In this paper we propose a new language Mediator to formalize component-based system models. Mediator supports a two-step modeling approach. Automata, encapsulated with an interface of ports, are the basic behavior units. Systems declare components or connectors through automata, and glue them together. With the help of Mediator, components and systems can be modeled separately and precisely. Through various examples, we show that this language can be used in practical scenarios.
Using Coq for Formal Modeling and Verification of Timed Connectors
The paper "Using Coq for Formal Modeling and Verification of Timed Connectors" by Hong Weijiang, Saqib Nawaz, Zhang Xiyue, Li Yi and Sun Meng has been accepted by FOCLASA 2017, which will be held in Trento, Italy, September 5, 2017.
Formal modeling and verification of connectors in component-based software systems are getting more interest with recent advancements and evolution in modern software systems. In this paper, we use the proof assistant Coq for modeling and verification of timed connectors. We first present the definition of timed channels and the composition operators for constructing timed connectors in Coq. Basic timed channels are interpreted as axioms and inference rules are used for the specification of composition operators. Furthermore, timed connectors being built by composing basic timed / untimed channels, are defined as logical predicates which describe the relations between inputs and outputs. Within this framework, timed connector properties can be naturally formalized and proved in Coq.
A Formal Specification and Verification Framework for Timed Security Protocols
The paper "A Formal Specification and Verification Framework for Timed Security Protocols" by Li Li, Sun Jun, Liu Yang, Sun Meng and Dong Jinsong has been accepted by IEEE Transactions on Software Engineering.
Nowadays, protocols often use time to provide better security. For instance, critical credentials are often associated with expiry dates in system designs. However, using time correctly in protocol design is challenging, due to the lack of time related formal specification and verification techniques. Thus, we propose a comprehensive analysis framework to formally specify as well as automatically verify timed security protocols. A parameterized method is introduced in our framework to handle timing parameters whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied π-calculus as a formal language for specifying timed security protocols. It supports modeling of continuous time as well as application of cryptographic functions. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various authentication and secrecy properties. Given a parameterized security protocol, our method either produces a constraint on the timing parameters which guarantees the security property satisfied by the protocol, or reports an attack that works for any parameter value. The correctness of our verification algorithm has been formally proved. We evaluate our framework with multiple timed and untimed security protocols and successfully find a previously unknown timing attack in Kerberos V.
Formal Modeling, Analysis and Verification of Black White Bakery Algorithm
The paper "Formal Modeling, Analysis and Verification of Black White Bakery Algorithm" by M. Saqib Nawaz, M. Ikram Ullah Lali and Sun Meng has been accepted by IHMSC 2017, which will be held in Hangzhou, China, August 26-27, 2017.
In this article, Black White (BW) Bakery algorithm is formally analyzed and verified in SPIN model checker. BW Bakery algorithm is first modeled in PROMELA and the model is then verified in SPIN. Mutual exclusion property for the BW Bakery model is verified with inline assertion and as linear temporal logic (LTL) formulas. BW Bakery algorithm uses bounded integers to put a bound on the required space in Bakery algorithm. We also investigate the complete state space and verification time for BW Bakery, original Bakery and Dekker algorithm in SPIN. Obtained results showed that verification time and generated state space for BW Bakery algorithm was much lower than original Bakery algorithm.
Weijiang, Yuteng and Xiyue have Finished their Thesis Defense Successfully
Three undergraduate students, Weijiang Hong, Yuteng Lu and Xiyue Zhang have successfully defended their bachelor thesis on June 8 and will start their graduate study soon. Congratulations!
Prof. Pierre-Louis Curien Visited Our Group
Prof. Pierre-Louis Curien from University Paris 7 visited our group on June 7, 2017 and gave a talk "A Syntactic Approach to Polynomial Functors and Opertopes". Details of the talk can be found here.
Prof. Min Zhang Visited Our Group
Prof. Min Zhang from ECNU visited our group on June 7, 2017 and gave a talk "Optimizing Backbone Filtering". Details of the talk can be found here.
Dr. Yu Jiang Visited Our Group
Dr. Yu Jiang from THU visited our group on May 31, 2017 and gave a talk "Dependable Model Driven Development of CPS: From Stateflow Simulation to Verified Implementation". Details of the talk can be found here.
Dr. Wen Su Visited Our Group
Dr. Wen Su from SHU visited our group on April 5, 2017 and gave a talk "Formalizing Hybrid Systems with Event-B and the Rodin Platform". Details of the talk can be found here.
A Formal Design Model of Cloud Services
The paper "A Formal Design Model of Cloud Services" by Sun Meng and Fu Guirong has been accepted by SEKE 2017, which will be held in Pittsburgh, USA, July 5-7, 2017.
To support rigorous development of cloud applica- tions, a formal model for understanding and reasoning about cloud services is needed. Unifying Theories of Programming (UTP) provide a formal semantic foundation for various expres- sive programming and specification languages. A key concept in UTP is design: the familiar pre / post-condition pair that describes a contract. In this paper we use UTP to provide a formal model for cloud computing, whereby cloud services are interpreted as designs in UTP. Refinement and equivalence relations between cloud services can be naturally established by implication between predicates. A family of composition operators that can be used to put different cloud services together to construct more complex services and applications are defined based on the design model for cloud services. On the other hand, dynamic reconfiguration of cloud applications can be dealt with in the context of the design model as well, by applying the reconfiguration rules on the design models for the corresponding applications.
Prof. Mingsheng Ying Visited Our Group
Prof. Mingsheng Ying from UTS visited our group on March 22, 2017 and gave a talk "Toward Automatic Verification of Quantum Programs". Details of the talk can be found here.
Prof. Haifeng Wang Visited Our Group
Prof. Haifeng Wang from BJTU visited our group on March 1, 2017 and gave a talk on safety-critical software for automatic train control system. Details of the talk can be found here.
2017 Seminar
The group seminar in 2017 will be held every Wednesday, 13:00-15:00.
Details about the seminar schedule can be found here.