Paper Info
Title
Design and Optimization of Multiclocked Embedded Systems Using Formal Techniques
Abstract
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.
Year
DOI
Venue
2015
10.1109/TIE.2014.2316234
IEEE Transactions on Industrial Electronics
Keywords
Field
DocType
automata theory,optimisation,multiclocked embedded systems,distributed systems,timed automata,asynchronous communications,train-control embedded system,standard iec 61 375,control-oriented behavior,iec standards,program debugging,system-on-chip,data-oriented behavior,bugs,multiprocessor architecture,control oriented behaviors,formal techniques,embedded systems,interclock domain,synchronous dataflow,real-world subway communication control system,multiclock train control system,synchronous dataflow module,multiclock,formal specification,synchronization,control systems,automata,asynchronous communication
Asynchronous communication,Synchronization,Computer science,Automaton,Real-time Control System,Correctness,Dataflow,Timed automaton,Control system,Distributed computing,Embedded system
Journal
Volume
Issue
ISSN
62
2
0278-0046
Citations 
PageRank 
References 
26
1.08
16
Authors
7
Name
Order
Citations
PageRank
Yu Jiang1973.31
Hehua Zhang210912.65
Zonghui Li3486.47
Yangdong Deng442944.78
Xiaoyu Song547151.61
Ming Gu655474.82
Jia-guang Sun71807134.30