<p>Model-Based Software Engineering (MBSE) is a development approach aiming to build correct-by-construction systems, provided the use of clear, unambiguous and complete models to describe them along the design process. The approach is supported by several engineering tools, such as the TASTE toolset. TASTE is a pragmatic and mature open-source toolset supported by European Space Agency that enables and provides automation for most of the phases of software system development: (i) heterogeneous system design through several modeling and programming languages, (ii) code generation, build and deployment of the binary application(s), and (iii) validation through static analysis and simulation. One topic left open in TASTE is the formal verification of a system design with respect to specified properties. In this paper we address this shortcoming by introducing model-checking in the TASTE environment. Our approach is based on the IF toolset, that provides the needed model-checking capabilities in an intuitive manner for TASTE engineers. This is mainly due to the similarity between the two formalisms—TASTE and IF, and the complete integration of the model-checker in the IDE (while hiding the implementation details). Our contribution enables a model-checking view in TASTE with specification of properties, execution of the IF model-checker given a user-set configuration, and exploration of the results (e.g., diagnosis) directly by engineers. We describe our implementation and the results obtained by applying our tool on a simple running example and an industrial case study.</p>