Integrating the SysML and ACME in a Model Driven Engineering Approach to Verify the Web Service Composition

Systems engineering, and especially the modelling of the Web service composition, needs proper means for verification to detect critical issues as soon as possible. The objective of our work is to identify a verifiable subset of SysML (System Modelling Language) that is usable by system engineers, while still amenable to automatic transformation towards formal verification tools. As we are interested in proving properties expressed using invariants, we consider the ACME/ARMANI language for this purpose. Our approach consists in an alignment of SysML concepts with an identified subset of the ACME language, using similarities between both languages. We define a SysML models and a transformation towards the ACME/ARMANI language for verification of the consistency of Web services composition. The obtained MDE(Model Driven Engineering) process is applied to a simplified concrete case study of travel system online: a SysML model is designed with properties, then automatically transformed into ACME/ARMANI, and finally imported into AcmeStudio tool for automated proof of the properties.