English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Model-Based Systems Engineering (MBSE) is a development approach aiming tobuild correct-by-construction systems, provided the use of clear, unambiguousand complete models to describe them along the design process. The approach issupported by several engineering tools that automate the development steps, forexample the production of code, documentation, test cases and more. TASTE [1]is pragmatic MBSE toolset supported by ESA that encapsulates severaltechnologies to design a system (data modelling, architecture modelling,behaviour modelling/implementation), to automatically generate the binaryapplication(s), and to validate it. One topic left open in TASTE is the formalverification of a system design with respect to specified properties. In thispaper we describe our approach based on the IF model-checker [4] to enable theformal verification of properties on TASTE designs. The approach is currentlyunder development in the ESA MoC4Space project.

Formal verification of space systems designed with TASTE