Cyber physical systems (CPS) typically employ real-time multitasking systems as their control software. This paper proposes an approach to formally analyzing such control software using statistical model checking of UPPAAL. The main contribution of this study is a model in timed automata which modularly describes the major components of a multitasking system. The model supports the analysis of timing-related functional properties as well as schedulability analysis, and can easily be adapted and extended for verifying different properties of various multitasking systems. A case study on an early version of the Chinese Lunar Rover control software shows that the proposed method is able to track down undesired behavior in real-world industrial CPS.
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.