| Abstract: In this paper, we apply our timing fault modeling strategy to writing formal specifications for communication protocols. Using the formal language of Specification and Description Language (SDL), we specify the Controller process of rail-road crossing system, a popular benchmark for real-time systems. Our extended finite state machine (EFSM) model has the capability of representing a class of timing faults, which otherwise may not be detected in an IUT. Hit-or-Jump algorithm is applied to the SDL specification based on our EFSM model to generate a test sequence that can detect these timing faults. This application of fault modeling into SDL specification ensures the synchronization among the timing constraints of different processes, and enables generation of portable test sequences since they can be easily represented in other formal notations such as TTCN or MSC. |
| @INPROCEEDINGS{BatthVCU07,
author = {Samrat S. Batth and Elisangela Rodrigues Vieira and Ana Rosa Cavalli and M. Umit Uyar},
title = {Specification of Timed EFSM Fault Models in SDL},
booktitle = {Proceedings of the 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'07)},
year = {2007},
address = {Tallinn, Estonia},
month = {26-29 June},
pages = {50-65}
} |