Simulation of Hybrid Reo Connectors

摘要

The prevalence of complex Cyber-Physical Systems (CPS) as an increasingly ubiquitous technology, necessitates the incorporation of component based and compositional design methods for the development and deployment of such systems. In this paper, we introduce a hybrid coordination framework to specify CPSs with components and use the resulting models to simulate, validate and verify those systems, using UPPAAL statistical model checker (SMC). We use SMC because with a level of uncertainty and unpredictability (e.g., the physical environment with which a CPS interacts), simulation-based verification approaches, where properties are guaranteed with a degree of confidence, produce more meaningful results. To demonstrate the main idea of our paper, we chose Reo as the language for the specification of hybrid components coordination, where both continuous and discrete state transitions can occur inside components. Next, we introduce a transformation that takes the specification of a connector in the language of hybrid Reo, into a network of hybrid timed automata, a commonly used semantic model in SMC. Finally, we report on the implementation of our transformation, and experimentation on two case studies.