An approach for modeling and analyzing the communication protocols in a telemedicine system

Telemedicine systems are a type of safety critical systems that require high quality in system design and implementation. The quality of the communication protocols between a user and a service provider in a telemedicine system is especially important to the success of a telemedicine system. Therefore, a rigorous modeling and analysis approach to ensure the quality of the communication protocols in a telemedicine system is necessary. However, most of the rigorous modeling and analysis approaches were developed based on formal methods, which are not practical for large systems. In addition, many of existing approaches are only useful in a particular development phase such as design or implementation but not the whole life cycle of system development. In this paper, we introduce an integrated modeling and analysis approach that enhances the quality of software testing though injecting the rigorousness of formal methods into it to ensure the correctness of a system at each development phase. The idea of the approach and its effectiveness are illustrated by case study of the communication protocols in a telemedicine system. The communication protocol is first modeled using a high-level Petri nets, and then the model is analyzed with model checking, simulation, reachability analysis, and testing. According to a selected test adequacy criterion, the adequate tests are automatically generated for the model, and then they are converted into the tests to test the system implementation.