Model Transformation for Requirements Verification in Embedded Systems

In embedded systems, use cases have become increasingly popular as a means of requirements specification and drive all the development activities,particularly in validation ones. However, they are usually written in informal text form describing the interactions between the environment and the system. This prevents using formal methods in requirements verification. Though, they are becoming a practical means to ensure the correctness of system models, formal methods still are not commonplace in embedded systems especially in the requirements validation. In this study presenst an approach to model transformation for requirements verification in embedded systems. It firstly consists of transforming the use case structured-text style into an UML activity diagram, which may be reused in the subsequent development steps and secondly we transform this diagram into Pres, a formal notation capable of capturing relevant features of embedded systems. In addition to the offered formal verification framework, we argue that our approach enables enriching the use case model and producing more precise and complete requirements.