UPSL-SE: A model verification framework for Systems Engineering

Systems Engineering (SE) is an approach for designing complex systems. It is now standardized, applied succesfully and recognized in industry. It is intrinsically a model based approach i.e. it promotes a set of modeling languages, reference models, methods, techniques, and processes allowing to guide and organize the designers work. Particularly, verification process is one of the main standardized processes. It helps the engineering team to detect errors or mistakes, to check solutions, to assume traceability of proof to the different stakeholders, and finally to help to argue and to assume the quality and relevance of the proposed solutions. The engineering team involved in a SE project is provided with various verification techniques and tools e.g. simulation, test, expertise, data analysis, traceabilty matrix, etc. However, the formal techniques used in other domains e.g. in software, automation or in mechanical engineering, remain not really considered to be an advantage in SE for many reasons which are first presented and analyzed in this paper. Second, it presents and illustrates the different components of a formal verification framework called UPSL-SE (Unified Properties Specification Language for Systems Engineering). This framework is based on a set of concepts, proposes verification techniques and is implemented in a platform allowing to complete the current verification toolbox.