White Paper

Validating Requirements with Simulation and Formal Methods


Two of the most important tasks in systems engineering are arguably understanding stakeholder needs and translating them into system requirements. This white paper discusses the early application of modeling to perform these tasks, demonstrating modeling techniques of increasing sophistication and value that range from purely descriptive models to formal proofs. The increased quality of system requirements alone justifies investment in these techniques, but the resulting models can also be used in later stages of the project to represent the needs of stakeholders more effectively. We show how requirement models can be utilized to achieve consistent and complete system requirements. Figure 1 shows the process followed in this paper to achieve these benefits.

Workflow diagram depicting the staged transformation of stakeholder needs to systems requirements on to detailed requirements by systems, software, and test engineers while producing artifacts such as architecture models, design models, code files, and test harnesses.

Figure 1. Process of refining stakeholder needs into system requirements leading to detailed requirements.

For this case study, requirements will be derived for a machine cooling system based on the stakeholder needs described below:

Provide a system that maintains the operating temperature of a machine, avoiding damage to the machine due to overheating.

  • [constraint] Cooling system needs to maintain operating temperature below 40 ˚C.
  • [constraint] Cooling needs to be effective within a predetermined time.
  • [assumption] Environmental temperature greater than -10 ˚C and smaller than 80 ˚C.
Illustration of an engineer standing beside a cooling system.

These stakeholder needs are ambiguous and could easily be misinterpreted, which could result in incomplete and/or incorrect system requirements, and eventually lead to a design that fails to meet the stakeholder’s expectations. To avoid this, validating stakeholder needs is necessary.

There are modeling techniques that can help validate our understanding of stakeholder needs and converge on a set of system requirements. These methods include the use of:

  1. Descriptive models
  2. Simulation models
  3. Formal models

We will describe each of these methods in the following sections and end with a discussion on the use of a digital thread to establish traceability between stakeholder needs and various levels of derived requirements.


  1. Using Descriptive Models

A first step in exploring stakeholder needs is to describe the different scenarios that the cooling system needs to fulfill. For example, what needs to happen if the temperature is too high, or when cooling does not appear to be effective?

Descriptive requirements models are a step forward compared to the traditional natural language requirements as they provide a structured, graphical representation of the requirement, which improves collaboration between the teams involved. A good example of such a representation would be a sequence diagram.

What Are Descriptive Models?

A descriptive model is a graphical specification of a system that describes what the system is or does in a human-readable way.

Figure 2 describes the following scenario: If the temperature (T) is too high (T>=40), cooling is needed; if cooling is effective (T<40), cooling should be turned off; but if cooling is not effective (delay>=30), the machine needs to be turned off.

A sequence diagram describing three different operational scenarios of a cooling system.

Figure 2. The sequence diagram describing our scenario.


  1. Using Simulation Models

Sequence diagrams provide graphical descriptions of how the modeled components of the cooling system work together in different scenarios. However, these descriptive requirements models are still firmly in the engineering domain, whereas simulatable (or executable) requirement models can yield observations and insights in the system domain, allowing stakeholders to get a direct understanding of the requirements in their domain-specific context. A good example of an executable formalism that can produce these outputs is a state chart (see Figure 3).

What Are Simulation Models?

A simulation model is a specification of a system meant for machine interpretation where the outputs of the interpretation are left for human interpretation to draw conclusions.

A simulatable state chart with plots showing outputs generated by the simulation.

Figure 3. A simulatable architecture component (state machine) and its outputs.

This is important because simulation provides an unambiguous interpretation of each scenario described in the earlier sequence diagrams. It also provides a means to communicate this interpretation back to the stakeholder, explore different scenarios, and understand what their specific needs are, so that we can describe that information in the system requirements.

Now that we have a model that simulates the behaviors specified in the sequence diagrams, we can observe and discuss the outputs generated by the state machine with the stakeholders. Additionally, we can validate whether the state machine behavior is consistent with the scenarios described in the sequence diagram. In Figure 4, the green checkmarks in the sequence diagram indicate that the right events have occurred in the right order during the simulation. This confirms that the functional model behavior is correct. These results can also be used for validation with the stakeholder.

Sequence diagram showing validation of expected behavior through simulation results with green check marks indicating “passed” criteria.

Figure 4. Validation through simulation.


  1. Using Formal Models

Although simulation techniques provide good coverage of system behaviors, simulation is typically targeted at key scenarios to support collaborative work. Formal requirements models, on the other hand, contain formalisms that enable a more systematic assessment of the model’s quality.

One such formalism is a Requirements Table that can be used to formally prove the consistency and completeness of a set of requirements. Consistent requirements do not conflict while complete requirements have no missing functionality. The precondition columns (A) in Figure 5 describe the system inputs (temperature values) and when a requirement is valid or “active.” The postcondition columns (B) describe the expected behavior when the specified requirement is active.

What Are Formal Models?

A formal model is a specification of a system meant for machine interpretation where the outputs of the interpretation are further processed to present definitive conclusions for human consumption.

Requirements Table explaining the requirements using a formal notation, with the precondition column describing the inputs and postcondition column describing the expected outputs.

Figure 5. Formal model to describe the requirements.

For example, requirement #1 states that when T is below 40 ˚C (T<40), the cooling system should be turned off (Turn_off_cooling == true).

An analysis using the formal methods capabilities of Simulink Design Verifier™ can now determine whether the requirements are consistent and complete. In Figure 6, the scenario where the temperature is exactly 40 ˚C has not been included and therefore this requirement set is incomplete.

Results of a formal analysis of a Requirements Table flagging an incompleteness issue with T=40 degrees being a missing precondition.

Figure 6. Formal analysis has identified an incompleteness issue (T=40 is missing).


Further Considerations and Uses of Requirement Models

Testing of Design Models

Formal requirement models provide a good starting point for downstream teams, both because the quality of the requirements is higher and because elements of the requirements model can be reused during design, automatic test generation, and verification. Requirement models can be used as part of unit tests to ensure that functional models are developed to meet requirements. These unit tests can be executed both interactively and as part of a CI/CD framework. Figure 7 shows that requirements 1 and 2.2 pass the test and that the other requirements have not been exercised.

A diagram showing a test harness reusing a Requirements Table for verification purposes.

Figure 7. Using the formal requirements as a test to validate design models.

Digital Thread and Beyond

Many artifacts are created and/or generated throughout the different stages of the product development lifecycle. These digital artifacts include requirements, architecture, design models, code files, and verification and validation files. It is critical to establish a traceable link between these artifacts to understand how requirements impact other requirements, models, or verification and validation activities. This link serves as the digital thread.

For example, requirements traceability diagrams can be generated automatically from the requirements and architecture models, helping provide insight into how these requirements, models, and verification artifacts are graphically linked to each other.

Figure 8 shows the digital thread where a stakeholder need is met by another stakeholder. In reality, several stakeholders will be spread across the organization covering different functional areas at various levels of abstraction. This is where a digital thread becomes indispensable. Furthermore, a digital thread facilitates the use of automated, agile, and iterative processes and infrastructure (DevOps). For example, Figure 8 shows how the verification status of a test is automatically fed back to the responsible engineer.

Traceability diagram showing the relationship between stakeholder needs, artifacts such as models and test cases, with verification status linked back to the requirements.

Figure 8. Traceability diagram showing the digital thread for the cooling system.

As organizations embark on their digital transformation journeys, the concepts of digital threads, digital twins, and DevOps play complementary roles in establishing a foundation for digital engineering. These concepts work in concert to create an infrastructure that supports the transition from traditional to digital-centric engineering practices.



In this paper, we have described a process wherein, based on stakeholder needs, we converged on (simulatable/executable) system requirements using simulation and formal methods. To do this, we used requirement models that could simulate (state machines), evaluate (sequence diagrams), and be formally analyzed (Requirements Table).

The use of requirement models enables automation for verification and validation activities, resulting in complete, consistent, and validated system requirements. It also improves collaboration between different teams, as they provide more information than purely descriptive or text-based requirements can.

By Alan Moore, Becky Petteys, and Stephan van Beek