Modeling of Embedded System Using SysML and Its Parallel Verification Using DiVinE Tool

摘要

SysML is a modeling language that can be used for the modeling of embedded systems. It is rich enough to model critical and complex embedded systems. The available modeling tools have made the modeling of such large and complex systems much easier. They provide sufficient support for the specification of functional requirements in the elicitation phase as well as in the design phase by graphical modeling. These systems must be properly validated and verified before their manufacturing and deployment in order to increase their reliability and reduce their maintenance cost. In this paper, we have proposed a methodology for the modeling and verification of embedded systems in parallel and distributed environments. We demonstrate the suitability of the framework by applying it on the case study of embedded security system. The parallel model checking tool DiVinE has been used because the available sequential verification tools either fail or show poor performance. DiVinE supports Linear Temporal Logic (LTL) for defining nonfunctional requirements and DVE language for specifying models. First, the case study is modeled using SysML's state machine diagrams and then semantics are described to translate these state machine diagrams to DVE based model. The translated model is verified against specified LTL properties using DiVinE.