Formal modeling and analyzing high-confidence software of cyber-physical systems.

From the perspective of multi-agent systems, a high-confidence software formal model (HCSFM) of cyber-physical systems (CPS) based on two complementary formalisms, namely Petri nets and π-calculus, is proposed. Petri nets are employed to visualize the architecture and model the behaviors of CPS software, and the structural analysis techniques allow the qualitative analysis of properties that may be proved directly on the structure of Petri nets. π-calculus is used to describe CPS software evolution, including agent joining, exiting, updating, and architecture reconfiguration. The evolving strategy of agents and the consistency of CPS software can also be analyzed using π-calculus. HCSFM will improve the dependability of CPS software. HCSFM is applied to unmanned ground vehicles CPS, which shows that it can effectively describe and analyze the high-confidence software of cyber-physical systems. [ABSTRACT FROM AUTHOR]