BepiColombo SIXS/MIXS OBSW Requirements Modeling Sample Clauses

BepiColombo SIXS/MIXS OBSW Requirements Modeling. Here we concentrate on the Event-B project BepiColombo_Models_v5.0 [RD9] that is the final version of the model of BepiColombo SIXS/MIXS OBSW requirements. The general modeling strategy was reached after several attempts at different approaches. Finding the right approach clearly required experience with Event-B which SSF did not have at the beginning of the Deploy project. The chosen modeling strategy has the following main features: • Refinement steps should be small. Every step should focus only on a few issues. • Complicated behavioral refinement is difficult to use. Superposition and data refinement offer tools for decomposing the problem into steps in most cases. • The refinements should proceed from a basic producer-consumer system towards a model of the TM/TC handling including mode management. The machines in BepiColombo_Models_v5.0 are as follows where every machine except the first one refines the previous machine: • obsw_M000 is devoted to TC/TM (telecommand/telemetry) traffic: reception and processing of TCs and production and sending of TMs is modeled on an abstract level. obsw_M000 has a hardware input buffer for TCs, a hardware output buffer for TMs, a memory pool for TCs and another memory pool for TMs. In obsw_M000, TCs arrive in a hardware input buffer from which they are moved to the TC pool in which they stay at least as long as needed. Respectively, TMs are created in the TM pool from which they are either moved to the hardware output buffer or deleted as obsolete. The fact that some TMs are reports on TCs is modeled, too, as well as the needed special operation that atomically resets the hardware output buffer. • obsw_M001 is devoted to processing of TCs and TMs. In obsw_M001, processing of a TC includes an acceptability check and, in the case of an accepted TC, an execution of the TC. Respectively, processing of a TC includes creation of the TC, a decision on whether to move the TM to the hardware output buffer and, in the case of a positive decision, moving the TM to the buffer. Creation of a TM includes assigning a priority level to the TM and insertion of the TM in a FIFO (first-in-first-out) queue that is dedicated to that priority level. A TM is allowed to be moved to the hardware output buffer only when the TM pool has no higher- priority TM. A TM that is a report on a TC can be either a report on the check of the TC or on the execution of the TC. In obsw_M001, TCs are processed in the order they arrive in the hardware input b...