Modeling of real-time embedded systems using SysML and its verification using UPPAAL and DiVinE

SysML is a graphical modeling language that is more suitable for modeling of real-time and embedded systems. The application modeled in SysML must be verified in earlier phases of software development life cycle to increase the reliability and reduce the modeling and verification cost. The available tools for verification are sequential and parallel types. The sequential verification tools either fail or unable to show the significant performance to verify a large scale embedded real-time system. The limitations of sequential verification tools have increased the importance of parallel verification tools. While, DiVinE is parallel verification tool that doesn´t support the timed verification of model. By keeping in view the limitations of both types of model checkers and their compatibility, we have proposed a methodology to use both types of model checkers for verification of real-time system that are graphically modeled using SysML. We demonstrate the suitability of the framework by applying it on a case study of embedded real-time system. The case study is modeled using state machine diagram of SysML and verified against specified timed properties using UPPAAL while the untimed properties are verified using DiVinE.