How to link SysML requirements?
SysML is at the center peace of MBSE. But many questions are raised when it comes to use it really. Most of them are related to requirement. Today, I will focus on how to link derived requirements.
I hear you say: Easy, use the «deriveReqt»!. But I think that using a «deriveReqt» is not the best way to link derived requirements. Let us see why on the house heater example.
The top goal of the heater system is to keep the house warm enough for the house’s temperature to be in the comfortable temperature range of every inhabitants of the house. It could be more formally define with the following OCL+Temporal logic formula:
always(theHouse.inhabitants->forAll(p | p.isIn(theHouse) implies p.conformtableTemperatureRange.contains(theHouse.temperature)))
This goal express exactly what the system should achieve. The system might set the temperature to zero if there is no (present) inhabitant or keep the temperature constant. Now we can derive this goal to a more concrete one. For instance, always(theHouse.temperature = 19°C). The rationale is that you make the hypothesis that 19°C is comfortable for everyone. You would express this in the SysML model with an OCL invariant or a parametric constraint on Person (self.comfortableTemperatureRange.contains(19°C)). The context model is thus as on following diagram.
Heater system BDD
For traceability reason, you would like to link the high level requirement, the low-level one and the invariant. But you cannot use the «deriveReqt» as it can only link requirements. Hopefully «Refine» can link with other model elements! Moreover in the formal method background, refinement has been well studied. Of course, it comes with several definitions (forward/backward-refinement, logical implication, bisimulation, …) but at least you can pick one.
Refinement of requirements for a heater system
Additionally a tool (to be written) can now formally check the refinement. I know SysML is not formal but ideas from fUML (aka Executable UML) can be applied for that. This is exactly what people from the KAOS/GORE method express and push forward. On the previous example the logical implication can indeed be automatically verified, because the conjunction of the invariant and the low-level formula implies the high-level one.
There are additional advantages, such as expressing alternative derived requirements, that I will demonstrate on future post. In conclusion, you can of course use the «deriveReqt» but then your tool shall enforce the presence of a rationale, or use the «Refine» when the rationale is already in the model and formally provable.
Edit: I forgot to mention Containment link! Containment link is related to model organisation and has no meaning (semantic) per se. Or you consider the extension set as in the property based requirement… but in that case you won’t be able to form a semi-lattice! More in future post.
Further reading:
- Requirements Engineering, from System Goals to UML Models to Software specifications, Axel van Lamsweerde
- Toward a property based requirements theory: System requirements structured as a semilattice, Patrice Micouin, Systems Engineering, Volume 11, Issue 3, pages 235–245, Autumn (Fall) 2008
- KAOS on wikipedia
- Program refinement on wikipedia
- Temporal Extensions of OCL Revisited, Michael Soden and Hajo Eichler, ECMDA-FA ’09: Proceedings of the 5th European Conference on Model Driven Architecture – Foundations and Applications
- B Method
- TLA+
