| Título: | On the Model Checking of the SpaceWire Link Interface |
| Autores: |
Hua, Wei; Capital Normal University Li, Xiaojuan; Capital Normal University Guan, Yong; Capital Normal University Shi, Zhiping; Capital Normal University Zhang, Jie; Beijing University of Chemical Technology Dong, Lingling; Beijing University of Chemical Technology |
| Fecha: | 2013-02-01 |
| Publicador: | TELKOMNIKA: Indonesian journal of electrical engineering |
| Fuente: |
 |
| Tipo: |
info:eu-repo/semantics/article info:eu-repo/semantics/publishedVersion |
| Tema: | No aplica |
| Descripción: | In this paper we display a practical approach adopted for the formal verification of SpaceWire using model checking to solve state explosion. SpaceWire is a high-speed, full-duplex serial bus standard which is applied in aerospace, so its functions have a very high accuracy requirements. In order to prove the design of the SpaceWire was faithfully implements the SpaceWire protocol’s specification , we present our experience on the model checking of SpaceWire link interface using the Cadence SMV tool. We applied environment state machine to overcome state explosion and successfully verified a number of relevant properties about transmitter and controller of the SpaceWire in reasonable CPU time. |
| Idioma: | Inglés |