Name
Abstract | ||
|---|---|---|
SpaceWire provides a full-duplex, point-to-point, serial data communication network for on-board applications. This paper presents a Timed Automata approach to modeling, analyzing, and verifying the SpaceWire link interface design. A network of Timed Automata is established to formalize the link interface, including Controller, Transmitter, Receiver, and Channel. Uppaal, a Timed Automata based model checker for real-time system, is adopted for symbolic verification of SpaceWire. The SpaceWire specification requirements are formulated in computational tree logic (CTL). In this way, we have the high-level models of both link ends interacted and verified resorting to Uppaal. It is demonstrated that link initialization can be made successfully within the time scheduled by the requirements of SpaceWire. Furthermore, the paper presents the time properties of the model and makes an analysis of time limitation in the situation that disconnection error occurs. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/COMPSACW.2013.56 | COMPSAC Workshops |
Keywords | Field | DocType |
time property,automata theory,computational tree logic,full-duplex point-to-point serial data communication network,timed automata approach,spacewire specification requirement,link interface,data communication,timed automata,on-board communications,high-level model,model checking,transmitter,receiver,real-time system,ctl,telecommunication computing,space communication links,graphical user interfaces,model checker,spacewire link interface design,symbolic verification,uppaal,formal logic,controller,uppaal gui,high-level models,time limitation,disconnection error,spacewire,link initialization,formal verification,real time system,synchronization,automata,transmitters | Serial communication,Computation tree logic,Automata theory,Model checking,Computer science,Automaton,Real-time computing,Initialization,SpaceWire,Formal verification | Conference |
Citations | PageRank | References |
0 | 0.34 | 2 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ping Luo | 1 | 0 | 0.68 |
| Rui Wang | 2 | 0 | 2.03 |
| Xiaojuan Li | 3 | 14 | 4.14 |
| Yong Guan | 4 | 787 | 82.67 |
| Hongxing Wei | 5 | 101 | 22.41 |
| Jie Zhang | 6 | 36 | 6.46 |