Design and Optimization of Multiclocked Embedded Systems Using Formal Techniques

Today's system-on-chip and distributed systems are commonly equipped with multiple clocks. The key challenge in designing such systems is that two situations have to be captured and evaluated in a single framework. The first is the heterogeneous control-oriented and data-oriented behaviors within one clock domain, and the second is the asynchronous communications between two clock domains. In this paper, we propose to use timed automata and synchronous dataflow to model the dynamic behaviors of the multiclock train-control system, and a multiprocessor architecture for the implementation from our model to the real system. Data-oriented behaviors are captured by synchronous dataflow, control-oriented behaviors are captured by timed automata, and asynchronous communications of the interclock domain can be modeled as an interface timed automaton or a synchronous dataflow module. The behaviors of synchronous dataflow are interpreted by some equivalent timed automata to maintain the semantic consistency of the mixed model. Then, various functional properties that are important to guarantee the correctness of the system can be simulated and verified within the framework. We apply the framework to the design of a control system described in the standard IEC 61 375 and several bugs are detected. The bugs in the standard have been fixed, and the new version has been implemented and used in the real-world subway communication control system.