Ph. D. Project
Title:
Executable Model-Based System Requirements Engineering (eMBRE) for early System requirements Validation and Design Verification (V&V)
Dates:
2022/11/07 - 2025/11/06
Student:
Supervisor(s):
Other supervisor(s):
Pr. Eric BONJOUR (eric.bonjour@univ-lorraine.fr)
Description:
Designers need models and methods to perform early and collaborative Verification and Validation
(V&V) respectively of system requirements and architectures (Chapurlat and Bonjour 2014), to detect
specification and design errors and to avoid late and costly modifications, during the ground & flight
test phase or even worse when the system is in operation. This approach ensures that system
requirements at all layers and system design phases are trustworthy. The system requirement
validation process aims to ensure the right system was built. The design verification process aims to ensure the system was built right. SE processes include requirements engineering based on the traceability of system requirements through the different system layers (Micaëlli et al. 2013). A textbased description is an ambiguous way for capturing and communicating system requirements, it leads system development teams to exchange incomplete, incoherent and incorrect descriptions of system requirements whereas executable model-based system requirements engineering (eMBRE) coupled with executable Concept of Operations open the opportunity to system requirements V&V: formally with proof-checking or factually with simulations reviewed with stakeholders. Executable" means that the model enables to support either proof-checking for formal system requirements validation or simulation for factual validation.
Systems Requirements Engineering (RE) is the result of iterative and recursive activities of definition, analysis and management (ISO/IEC/IEEE 15288: 2015). This process receives as input a list of needs and constraints from stakeholders, (i.e., customers, users, certification authorities), and transforms this list into technical (system) requirements that the system must satisfy in order to meet the needs.
Requirements analysis is the activity that aims to verify the qualities of a requirement or a set of requirements, to negotiate changes, and to define the integration, verification and validation plans of the system. Requirements management is the activity of maintaining requirements along the life cycle
of the system. In a complex system (system decomposed into subsystems and components at different layers), the requirements of subsystems are defined (or refined) through the system architecture.
These transformations are potential sources of errors, therefore verification and validation activities (requirements analysis) should be led after each step. Today, most requirements are described in textual form, which does not allow for early detection of possible specification or design errors.
Moreover, there are different types of requirements (e.g., functional, performance, safety). ISO29148 or ARP 4754A standards define different qualities for a requirement or a set of requirements (e.g., consistency, completeness...). Different formal verification techniques exist but their application on complex systems seems difficult (scaling). In the field of Systems Engineering, different approaches and tools have been developed in the last decade (Masmoudi et al. 2022), e.g., SysML Standard (omgsysml.org), Property Model Methodology (PMM) proposed by Micouin (Micouin 2008) (Micouin 2014), Stimulus software developed by Argosim and integrated in Dassault System's 3D Experience.
The incoming version v2.0 of SysML will pay special attention on Property-Based Requirements (PBR).
With PMM, Micouin proposed to model PBR using a set theory to describe the external relations of the system with its environment. These cause-effect assertions may be verified formally and factually. With Stimulus, the system engineer can model requirements with temporal logics expressions, being presented in a textual, natural language-like format. These properties can be completed with statecharts. The whole set can then be checked for consistency through simulated runs, or used as a basis for tests generation (Azzouzi et al, 2019).
In ISO 15288 and ARP 4754A standards, capturing complete, coherent and correct requirements is a key process. Our objective is to propose and experiment models and methods to support a collaborative and trustworthy eMBRE approach focused on the objectives of systems engineering
(capture requirements with executable and therefore validable requirement models; design executable and therefore verifiable solution models), that shall be consistent with other SE processes,
applicable for the development of key enabling systems (manufacturing, support & services), and able to prevent specification and design errors and foster collaborative approaches either on the overall SoI problem or on solution spaces. In this context, this PhD thesis aims to answer four main research questions:
- What are the needs for requirements modeling and V&V as well as their priorities.
- What are the appropriate formalisms according to the modeling and V&V needs?
- How to prove the qualities of requirements expressed by different languages and models?
-What are the requirements which is useful (in terms of benefit/cost/risk) to be further formalized?
(V&V) respectively of system requirements and architectures (Chapurlat and Bonjour 2014), to detect
specification and design errors and to avoid late and costly modifications, during the ground & flight
test phase or even worse when the system is in operation. This approach ensures that system
requirements at all layers and system design phases are trustworthy. The system requirement
validation process aims to ensure the right system was built. The design verification process aims to ensure the system was built right. SE processes include requirements engineering based on the traceability of system requirements through the different system layers (Micaëlli et al. 2013). A textbased description is an ambiguous way for capturing and communicating system requirements, it leads system development teams to exchange incomplete, incoherent and incorrect descriptions of system requirements whereas executable model-based system requirements engineering (eMBRE) coupled with executable Concept of Operations open the opportunity to system requirements V&V: formally with proof-checking or factually with simulations reviewed with stakeholders. Executable" means that the model enables to support either proof-checking for formal system requirements validation or simulation for factual validation.
Systems Requirements Engineering (RE) is the result of iterative and recursive activities of definition, analysis and management (ISO/IEC/IEEE 15288: 2015). This process receives as input a list of needs and constraints from stakeholders, (i.e., customers, users, certification authorities), and transforms this list into technical (system) requirements that the system must satisfy in order to meet the needs.
Requirements analysis is the activity that aims to verify the qualities of a requirement or a set of requirements, to negotiate changes, and to define the integration, verification and validation plans of the system. Requirements management is the activity of maintaining requirements along the life cycle
of the system. In a complex system (system decomposed into subsystems and components at different layers), the requirements of subsystems are defined (or refined) through the system architecture.
These transformations are potential sources of errors, therefore verification and validation activities (requirements analysis) should be led after each step. Today, most requirements are described in textual form, which does not allow for early detection of possible specification or design errors.
Moreover, there are different types of requirements (e.g., functional, performance, safety). ISO29148 or ARP 4754A standards define different qualities for a requirement or a set of requirements (e.g., consistency, completeness...). Different formal verification techniques exist but their application on complex systems seems difficult (scaling). In the field of Systems Engineering, different approaches and tools have been developed in the last decade (Masmoudi et al. 2022), e.g., SysML Standard (omgsysml.org), Property Model Methodology (PMM) proposed by Micouin (Micouin 2008) (Micouin 2014), Stimulus software developed by Argosim and integrated in Dassault System's 3D Experience.
The incoming version v2.0 of SysML will pay special attention on Property-Based Requirements (PBR).
With PMM, Micouin proposed to model PBR using a set theory to describe the external relations of the system with its environment. These cause-effect assertions may be verified formally and factually. With Stimulus, the system engineer can model requirements with temporal logics expressions, being presented in a textual, natural language-like format. These properties can be completed with statecharts. The whole set can then be checked for consistency through simulated runs, or used as a basis for tests generation (Azzouzi et al, 2019).
In ISO 15288 and ARP 4754A standards, capturing complete, coherent and correct requirements is a key process. Our objective is to propose and experiment models and methods to support a collaborative and trustworthy eMBRE approach focused on the objectives of systems engineering
(capture requirements with executable and therefore validable requirement models; design executable and therefore verifiable solution models), that shall be consistent with other SE processes,
applicable for the development of key enabling systems (manufacturing, support & services), and able to prevent specification and design errors and foster collaborative approaches either on the overall SoI problem or on solution spaces. In this context, this PhD thesis aims to answer four main research questions:
- What are the needs for requirements modeling and V&V as well as their priorities.
- What are the appropriate formalisms according to the modeling and V&V needs?
- How to prove the qualities of requirements expressed by different languages and models?
-What are the requirements which is useful (in terms of benefit/cost/risk) to be further formalized?
Department(s):
| Modeling and Control of Industrial Systems |
