Professor Zhi Jin's team and 111 Intelligence base experts, Professor Carlo Ghezzi's team collaborate on the topic of the Cyber-Physical Space Systems for several year. Recently, one of their outcomes won the ACM SIGSOFT Distinguished Paper Award at ASE2020.
The awarded paper is: Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations. The co-authors are Christos Tsigkanos, Nianyu Li, Zhi Jin, Zhenjiang Hu, Carlo Ghezzi
Abstract: Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets – design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder’s viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive systems whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.
Collaboration referring to the Cyber-Physical Space Systems has several other outcomes, including:
l Nianyu Li, Christos Tsigkanos, Zhi Jin, Zhenjiang Hu, Carlo Ghezzi: Early validation of cyber-physical space systems via multi-concerns integration. J. Syst. Softw. 170: 110742 (2020)
l Nianyu Li, Christos Tsigkanos, Zhi Jin, Schahram Dustdar, Zhenjiang Hu, Carlo Ghezzi: POET: Privacy on the Edge with Bidirectional Data Transformations. PerCom 2019: 1-10
l Christos Tsigkanos, Nianyu Li, Zhi Jin, Zhenjiang Hu, Carlo Ghezzi: On early statistical requirements validation of cyber-physical space systems. SEsCPS@ICSE 2018: 13-18
