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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Modeling and Analysis of Component Connectors in Coq
The paper "Modeling and Analysis of Component Connectors in Coq" by Li Yi and Sun Meng has been published in Proceedings of FACS2013, LNCS 8348, pages 273-290, Springer, 2014.
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 analysis of Reo connectors via Coq, a proof assistant based on high-order logic and λ-calculus. Basic notions in Reo, like nodes and channels, are defined by inductive types. By tracing the data streams, we can simulate the behavior and output of a given Reo connector. Besides, with prerequisite axioms given, we can automatically prove connectors’ properties using the Coq proof assistant.