Formalize and Validate Requirements - MATLAB & Simulink
Video Player is loading.
Current Time 0:00
Duration 23:33
Loaded: 0.70%
Stream Type LIVE
Remaining Time 23:33
 
1x
  • descriptions off, selected
  • en (Main), selected
    Video length is 23:33

    Formalize and Validate Requirements

    Overview

    Incomplete and inconsistent requirements cause errors in the design phase that become exponentially more expensive to fix over time. Engineers can save time and money by formalizing requirements to validate them earlier. Formal requirements are expressed mathematically as unambiguous specifications that you execute through simulation to validate that they are complete, correct, and consistent.

    In this session, you will learn about the different styles of formal requirements, how to model complete and consistent formal requirements, and how to go from stakeholder needs to formal requirements using use case diagrams and simulation.

    Highlights

    • Express requirements that are consistent and complete
    • Go from stakeholder needs to formal requirements using use case diagrams
    • Simulate requirements to validate required model behavior

    About the Presenters

    Pat Canny is a Product Manager on the Simulink Verification and Validation team. He has a background in helicopter flight control systems and jet engine embedded control systems. He has previously worked at Sikorsky Aircraft, GE Aviation, and Avitas Systems.

    Stephan van Beek has been working for more than 15 years as a technical specialist in Systems Engineering and Embedded Systems at MathWorks in Eindhoven. He works closely with customers across Europe that want to build a bridge between Model-Based Systems Engineering (MBSE) and Model-Based Design (MBD).

    Recorded: 21 Sep 2022

    Hi, everyone, and welcome to this webinar. My name is Pat Canny. I'm a product manager in the Model Verification and Validation team here at MathWorks. I'm joined here today by my colleague Stephan van Beek, an Application Engineer based in the Netherlands.

    We're here today to talk to you about how to formalize and validate requirements, define consistent and complete requirements starting with stakeholder needs. But, first, let's start off with a simple example.

    These are three requirements that we wrote for an electric vehicle charging system. These are safety requirements. The first requirement has to do with locking the charger in place if the electric vehicle supply equipment is compatible.

    The second requirement stipulates when to unlock the cord during normal shutdown procedures. And the third requirement dictates when to unlock the cord during an emergency shutdown. Now, you don't have to be an expert in electric vehicle charging systems, I certainly am not, to see a requirements error here. Or at least, can you spot the error?

    Well, assuming you just pause the video to take a, look one thing to ask is what happens during an emergency shutdown? Z So, as it turns out, the first requirement and the third requirement are in conflict during that scenario. So one easy fix is to define the scope more fully of the first requirement to be not in an emergency shutdown.

    So that's great. We just resolved the requirements conflict. Are we all done? Well, not really. This is not a complete set of requirements. It's not the whole story. What happens when the voltage is above 60 volts?

    What about when the charge session stop signal isn't received? Or what happens if it's not charging anyway? So this is a simple example just to motivate you to show a case where you have conflicting requirements which are inconsistent, and an incomplete set of requirements.

    So what are you going to learn today? First, why should you model formal requirements? What are the different styles of formal requirements models? When would you choose one style over another? And Stephan's going to go through a use case of how to develop formal requirements for stakeholder needs using use case diagrams and simulation.

    So why should you model formal requirements? Well, they're mathematically rigorous. They're executable through simulation. They're easier to author and maintain than pseudocode text requirements. I'll get into more details on what pseudocode text requirements look like in a few minutes.

    They're also easier to analyze as the requirement set grows, and they're reusable for downstream verification activities, such as automatic requirements-based test generation. So let's go through some different modeling styles using MathWorks products.

    You can use Simulink blocks, a Stateflow state chart, MATLAB code written in a MATLAB function block, temporal assessments from Simulink Test, or a requirements table from Requirements Toolbox. Now, this is a newer feature and I'm going to go through a quick demonstration later.

    But which style should you choose? Those are five different styles that I just showed you in the previous slide. Well, it depends on a few factors. What is the appropriate verification method? Which style are you comfortable with? What type of requirement is being modeled? And how would you ensure the requirements are complete and consistent?

    Again, I gave a simple example at the beginning of three requirements with issues right away. So, first off, what is the appropriate verification method? This often depends on the type of requirement. Many requirements are relatively easy to verify through simulation, such as mode logic, or anything that uses an if this, then that sort of structure.

    So a temporal assessment is I'm showing here on the slide, or a Simulink assertion, may maybe the appropriate modeling style for these types of requirements. Some requirements, often safety requirements, are difficult if not impossible to fully verify using simulation.

    This is where static analysis techniques can help. You can use tools like Simulink Design Verifier to define functions in a Simulink model or a Stateflow chart to model these requirements and prove that they can't be violated, such as the example here.

    Next, is what style are you comfortable with? Some users are more comfortable writing MATLAB code. This may also be preferred if you have a complex expression which might be more difficult to visualize in a Simulink model.

    This is an example of a formal proof statement defined in a MATLAB function block. Other users are more comfortable using Simulink or Stateflow to model their requirements. This example uses blocks from the Simulink Design Verifier library in combination with an assertion block in Simulink. You can model the same requirement using different styles. Sometimes it comes down to preference.

    Next is what type of requirement is being modeled. Many requirements are simple and logic driven, sort of if this, then that structure, such as fault detection, signal selection, sometimes called voting, or mode logic. These are often simple requirements that represent the vast majority, in some cases, over a given requirement set.

    There are some common challenges with validating these types of requirements. An individual requirement is often easy to manually validate. But a set of many requirements is not so easy to manually validate. Completeness and consistency are often the top challenges, such as the example I gave at the beginning.

    Completeness is when all required functionality is defined. And consistency is when requirements do not conflict. So how do engineers ensure consistency and completeness today with these types of requirements? Many organizations create intermediate-level text-based requirements.

    These requirements often look like pseudocode such as this example. The system shall enable drive mode 1 when switch 1 is pressed. Notice something a bit peculiar about this requirement? Well, it calls out these variable names, drive mode 1 and switch 1, which are basically just symbols.

    So a team will develop tools to parse these types of requirements to check for issues and compliance with either internal requirements standards and styles, or standards in the industry such as Inkosi. This process and these tools are often expensive to create and maintain.

    The moral of the story is, text is not always the answer. You should model these types of requirements. Let's switch over to MATLAB to see how you would model logic-driven requirements in a requirements table.

    Each row of the table defines a requirement. A requirement includes a summary, which is a text-based description of the requirement; a precondition, which is an expression, which defines the conditions where the requirement is valid. This expression is written using MATLAB code-- an optional duration, which describes the time in seconds during which the precondition must be satisfied; a postcondition, which is an expression which defines the conditions that must be achieved when the precondition is met.

    You can also express a variable's range using standard syntax, such as parentheses and brackets. You can analyze the table for consistency and completeness using Simulink Design Verifier. The results are shown in a report and are highlighted on the table.

    You can also define assumptions, which are accounted for during consistency and completeness analysis. I'm now going to turn things over to Stephan to go through a use case on how to define formal requirements starting with stakeholder needs.

    Thank you for your introduction to the requirements table. So let's see how we can now use this very nice new feature for the design of a system and software architecture for production machine and its cooling system.

    And while we actually have to stakeholder requirements, the machine needs to have a certain production throughput. And the machine also needs to operate within a certain temperature range. Now, I think we can all agree that these are nowhere near good design requirements. They're ambiguous. They're not complete. So they will need some further refinement together with the stakeholder.

    And, again, I would say there are many ways of doing this. But in this particular case, I've chosen to actually use case diagram to drive this conversation with the stakeholder. And where use case diagram, you can actually create it by means of interconnect block diagrams, state charts, sequence diagrams.

    But I'd like to extend this a bit more. I'd like to add also a notion of simulation to it as well as formal methods. So let's go to MATLAB and see how this would look like in System Composer, which I've used to actually create this interconnect block diagram.

    Now, this is a very descriptive model. It shows the actors, the environments, the operations engineer. I have my inputs, my temperature inputs. I have the actual behaviors, and as well as the actions that need to happen as part of this use case diagram.

    I've also provided a bit more detail context to the cooling action when cooling needs to be off, on, or when a machine needs to be turned off if cooling is not effective enough. But, as I mentioned, this is a very descriptive model. So it already helps, but I'd like to do a bit more with it.

    And, as I already mentioned, I'd like to add a notion of simulation to it. So for that, I've attached a test harness to it. And this test harness basically gives me the controls to drive the simulation, machine temperature, ambient temperature. It has the actual behavior of the state chart.

    And I've also added some visuals to indicate which action is active at the given moment and what the current temperature is. So let's run the simulation and see what happens. Now, in this case, we start in the cooling-off stage. You see the nice animation in the state chart.

    And when I control-- when I increase the machine temperature-- the machine is overheating. You see that cooling kicks in. And as a result of cooling, temperature drops, cooling is turned off again. And if after a while the temperature increases again, but at this time it doesn't go down, then at some point the expectation is that the machine needs to be turned off because then apparently something serious is happening.

    Now, this is a very visual way of representing the whole setup of my cooling system that I could quite nicely use in a conversation with the actual stakeholder. So this already gives me some very good insights in my actual design requirements, which I have captured in the form of requirements table.

    Now, you see in this lower-right corner. I have a component called ReqTable. In fact, it's in reference to subsystem which references another model that contains my requirements table. And the inputs of my requirements table are my temperature, as well as the output states of my state chart.

    So let's look into the requirements table itself. So here you see that the precondition, that's mostly driven by the temperature, the current state of my system, as well as the postcondition which describes the output conditions, the outputs expected outputs for each requirement. And each requirement is described by each line in this table.

    Now here the question is, are these requirements complete, and are a consistent, question mark? So you might type in the chat your answer if you believe that they are consistent, or if they are inconsistent or not complete, and what the inconsistency or the incompleteness says.

    But I'd like to take an easier way of doing this by simply running this table analysis. And this will take actually a form of view on the model on the requirements table to assess the completeness and the correctness of my requirements.

    Do I have any requirements conflicts, or are any specific scenarios that I have captured in the form of this requirements table. Notice, this may take a little while. So as a first step, it validates the compatibility of the table, which it is obviously.

    And in this stage, it determined that there are six objectives to be satisfied. And three of them can be satisfied. And three of them are falsified. Now, looking at the results of the analysis here, then I show that there are three incomplete instances. But they all revolve around the temperatures being exactly 40 degrees Celsius.

    Now, you see here that I have greater than. I have smaller than. So I actually forgot the equal sign and one of these requirements. And, to be honest, this is not very-- this is not uncommon mistake to make. So let me go back to the model. And I said this is in reference to a subsystem.

    So let me reference a version of this requirements table, but that already includes the fix. And if you look at it now, then you see that we included the equal sign to my requirements. So where the temperature is greater or equal to 40 degrees Celsius, cooling should be turned on. So that's got to be the requirement.

    And now when we run the analysis, then again we go through the same process still six objectives to be satisfied. And it can all be satisfied in this case, which is great. So now we also have the formal proof that my requirements are complete, that they are consistent.

    And what I actually already did before is that I can now actually validate these requirements while I'm running my simulations, which again, it's great. But then the second question is when I do this, validating these requirements through simulation, is this the proof that the requirements table and the model are-- they are 100% equal?

    Again, we don't know. I mean, this, of course, depends on my simulation inputs. So here I might take a fist step towards using full analysis to also formally prove that requirements and model, that they basically perfectly match.

    So, again, here we have our requirements table. And as a tool, the tool that I'm going to use now is called Simulink Design Verifier. And with the Simulink Design Verifier, I can perform property proving. And this requirements table in itself also very much could serve as a property that I need to prove that-- it's equal or that the model is equal to the property which is described in this requirements table.

    So, again, the method that I'm going to use here, it's called property proving. So let me just kick it off. And, again, we go through the same steps. So the first step is to validate if the model is compatible for proving with Simulink Design Verifier, which it is.

    And so four objectives to be proven, one is already satisfied. One is falsified. So, again, from the four objectives, three are satisfied, one falsified. Now, to get some further details on this, for that I would have to look into the detailed analysis report. So let's open it up.

    And here I basically get more details on the analysis done on the model. So here you see the objectives that are satisfied, that are considered valid. And there was also one objective falsified. And when we falsify an objective, we also provide a counterexample to replicate the issue through simulation.

    So if I just click on this link, it will take me to the counterexample. And here you see that it's very much steps that will bring the system into a cooling on state. But after exactly 30 seconds, temperature drops to minus 128 degrees. Which according to our requirements means it should go back to a cooling off state. But apparently that is not happening.

    And then the question is, why is that happening? And for to answer that question, we need to go back to the model. So let's do that. So we go back to the state chart. And when I drill into this state chart, what I see here is that there are two conditions that are apparently true after exactly 30 seconds. It's a condition after 30 seconds as well as temperature below 40.

    But in this particular case we have an execution order specified that the after 30 seconds has an higher priority over t minus 40 degrees. So either we may want to change that execution order priority, or we may want to extend the condition after 30 seconds with one additional one that says that if, in addition to that temperature is still equal or greater than 40 degrees, just to avoid the conflict, the condition conflict basically.

    So with that said, after making that change to the model, we can then prove that model and requirements table are the perfect match again. And, again, we have formal evidence to actually back that statement up as well.

    So let's go back to the presentation. So what we have done so far is we have used a System Composer to build a descriptive model for a use case diagram. We also extended the model with simulation, with a test harness to be able to simulate it to be a bit more expressive in the behavior, in our understanding of the requirements.

    We then formally proved that there were incompleteness, that there were incompleteness issues, which we fixed. And then after that we formally proved that there was a mismatch between the requirements table in the model. We could fix that issue quite easily as well.

    And then we are actually having a requirements table, which is basically our input for our design process. So knowing, having all of this, we could also quite easily create the links between the stakeholder, the various requirements, the various models like architecture models, design models, verification components.

    And after establish that kind of traceability, we could also then quite easily create this traceability diagram. And which is quite convenient if you need to further-- if the stakeholder needs to understand who are the design teams to talk to if stakeholder requirement changes.

    Or if a certain design requirement cannot be implemented, cannot be met, who is a stakeholder to talk to when that happens? And, again, these are quite useful diagrams to facilitate those type of conversations.

    What we did is we actually used a use-case diagram to come up with our design requirements for functional requirements, system architecture, as well as hardware requirements, which can then be used to create our functional architecture, logical architecture, physical architecture, as well as our design components in Simulink, and which can then be used for code generation and C or C++ code, for instance.

    So, overall, I would say the value that we provide is that-- so it's basically, we provide a way to maintain requirements as a single source of truth throughout the production development process by using simulatable models to actually transform stakeholder requirements needs, and to design requirements, to establish traceability, to manage system complexity through views and traceable architecture. We didn't actually show that, but again, it's part of System Composer as well.

    You can then also connect system architecture with software architectural components. Again, we didn't show that but it's part of the tool-- as well as the ability to explore design spaces through trade off studies. Again, we didn't show it, but it's part of what System Composer can already provide to you. So having said that, back to you, Pat, for concluding this webinar, thank you.

    Thanks, Stephan. So what did you hopefully learn today? First, why should you model requirements? What are the different styles of requirements models? Remember the five different styles I showed you? There's a lot you can choose from.

    So when would you choose one style over another? It depends on a few different factors such as the verification method and your own personal preference. And how do you develop formal requirements from stakeholder needs? Refer back to Stephan's use case for guidance.

    Thank you for joining us today and feel free to visit MathWorks.com for more information on how to formalize requirements, thanks.