Thank you very much @LaurentDelaigue for the kind words!
It was an honour and a pleasure to be hosted by you and welcomed by such a warm audience 
Here below are some questions that went unanswered during the presentation itself 
Have you differentiated in your Physical Level between HW & SW domains? And if so, did you transfer this param. to TASTE?
I feel like this question can be interpreted at two levels of depth.
I’ll elaborate on both, but the short answers are: yes in full for components, and kinda (but not really in the same way) for functions.
About our modelling of Components at the Capella Physical Level, we used Behaviour and Node PCs extensively in accordance with the ARCADIA method.
This is one of the most fundamental pillars of mapping to TASTE (not only for us, but for the N7Space pioneers too): Behaviour and Node PCs are used to represent SW and HW components respectively, and the allocation of the former to the latter is used to represent the deployment of SW Functions to HW Devices. All further mappings listed in the tables below are basically built on this core symmetry!
About our modelling of Functions at the Capella Physical Level, we did mostly focus on using them to represent steps for components to perform in the SW domain, as it allowed us to make the most out of the mapping to TASTE and was therefore the main focus of our work.
However, the beauty of the ARCADIA method is in its malleability, and nothing prevents Physical Functions from also representing steps for HW components to perform – and, in turn, Behaviour PCs from also representing more complex HW behaviours. In fact, we did adopt this approach to model an off-the-shelf camera for our prototype sounding balloon mission.
Similarly, this can be extended to HW components to make: depending on the scope of your modelling, Functions could represent functional groups of electronic components in a circuit (e.g. “amplify signal”), or “building blocks” of a DSP network implemented on an FPGA (e.g. “delay signal”). TASTE does currently support VHDL blocks, so the latter option is particularly interesting for further bridging.
If solely using Capella for MBSE of a space subsystem, do you think it would also give good results until the phase before assembly and testing?
This is a very interesting question!
My (certainly limited) understanding of MBSE is that it shines particularly in integration settings, so I’d say yes if the model includes interfaces to other subsystems or to the general system as fixed boundaries for the subsystem under modelling – on the other hand, I don’t think it would need much more to be useful. You can always follow the ARCADIA method to design and analyse your subsystem, and use Obeo’s M2Doc add-on to generate specification documents for assembly and testing. If the other subsystems or the entire system are already modelled in Capella, the System-Subsystem Transition add-on could also be helpful to manage complexity.
Of course, the bridge method would only really be applicable to software-heavy subsystems, but TASTE can similarly be useful too as long as boundary interfaces are considered. In fact, for our sounding balloon mission, the Payload Data Handling subsystem was developed outside of TASTE, and even needed multiple hardware nodes (a Raspberry Pi Pico acting as an I2C bridge to the NVIDIA Jetson Nano running the ML processing pipeline); still, the understanding and specifications of the subsystem boundary interfaces developed in Capella were really helpful in making it work reliably.
Could you tell more about the formal verification you did? Can you present any example?
Unfortunately, we haven’t done any formal verification just yet as we needed something to verify first, so I’ll tell about the formal verification we’d like to do instead.
The most immediate and interesting development would be to formalise the “unit” behavioural verification step and extend it beyond the component level to subsystems and even the entire system. Currently, this activity is only performed relatively informally at the component level. This is because TASTE’s OpenGEODE editor only generates state chart diagrams from individual blocks of SDL code.
However, a simple analysis of the Capella [MSM] should enable the generation of some basic Linear Temporal Logic rules to formally verify that the FSM implementation matches its specification, such as the presence or absence of transitions between certain states. Additionally, following our recommendations to design [MSM]s at all levels of abstraction and specifying each state of a component as a combination of the states of its children, the same process can be repeated for subsystems and even the entire system. TASTE enables this enforcement by supporting model-checking with full visibility of all components.
Both these ideas are only considering verification, as answering the question “Have we built the system right?” – but validation is another very interesting option, to answer the question Have we built the right system? This would have to look a little different, as formal validity rules are typically more complex and specific to a particular system, and as it’s better to analyse for validity earlier than the implementation stage to avoid having to go back to square one. Some research has already been done in this area, but an add-on extending Capella to support this capability would surely be very nice.
Did you generate the code out of the model?
Although “generation” is still manual in our work, we did find a rigorous and straightforward way of deriving a good deal of code from our model.
For the architectural aspects (data types and structures, software components and interfaces, deployment of software to hardware), we developed mappings between Capella diagrams and TASTE views to bridge one tool to the other. I’ve tried my best to explain this in the webinar, in the interactive poster, and in the full paper. Again, this was done manually at this stage, but very similar entity and relationship mappings were used in the automated plugin developed by N7Space, so it shouldn’t be too complex to reproduce with our semantics.
For the behavioural aspects (software component logic implementations), at this stage we recommended that Functions “should represent reasonably atomic implementation steps: decisions, interface calls, I/O operations, etc.”; these steps can then be elaborated when actually implementing the code in TASTE. It’s a little harder to extend formality beyond this point, especially considering that TASTE systems support implementing different components in very different languages – you might have logic in Simulink semantics for one block and in VHDL semantics for another; even without these “extras”, SDL blocks are way too convenient to be disregarded just for the sake of homogeneity, and without a HAL block written in C you’re effectively locking your system out of interacting with the outside world.
However, some advancements are possible by considering the formality of [MSM] Finite State Machines representing SDL components. Following our recommendations to allocate incoming Physical FEs as Transition Triggers, and to allocate boundary-crossing FEs to CEs, a rigorous link can be made from the state transition to its triggering interface signal, and translated into TASTE; similarly, outgoing Physical FEs listed as Transition Effects can be rigorously bridged to TASTE interface calls.
This becomes more problematic when trying to represent logic such as decisions, iterations, etc. The fork, join, and choice blocks available in [MSM] could do a pretty good job, but at that point “modelling” in Capella would effectively become trying to use Capella for programming, and I feel like drawing the line at a miserable user experience. In my opinion, the right balance would be generating code skeletons with pre-populated states, transition triggers, interface calls, and comments on each transition outlining the steps specified in Capella to let the user do the humanly near trivial but programmatically very challenging job of turning those into actual code.
In accordance with the spirit of open-source software, we make both our model and our codebase public. The forum’s new user rules prevent me from spamming too many links, so check out the webinar’s description for more info
