This example demonstrates the modeling and verification of the following aircraft requirement:
Requirement:
APU (Auxiliar Power Unit) start sequence shall start after three successive start failures of one of the engines.
This is an informal requirement. It is interpreted in the following formal way:
Formalized requirement:
APU (Auxiliar Power Unit) start sequence shall start after three succesive start failures of one of the engines.Inputs and parameter of the MaxRising() block are:nRisingMax : Maximum number of check rising edges. APUSeqStarted.y: Output of the boolean step. True if the APU backup sequence is started. EngineStart.y : Output of the boolean pulse. True if the engine is started.nRisingMax = 3 condition = APUSeqStarted.y check = EngineStart.y
This requirement can be modelled with the ChecksInSlidingWindow.MaxRising block.
Test setup of this example:
results in
simulation result |