Calvino, Alessandro TempiaApvrille, Ludovic2021-07-172021-07-172021-07-172021-01-0110.5220/0010256302160223https://infoscience.epfl.ch/handle/20.500.14299/179970WOS:000662840600020Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a new model-checker that can be applied (almost) directly to the SysML model. The paper first explains how this model-checker works. Then, we explain how it can efficiently check CTL-like properties. Finally, the paper discusses the performance of this model-checker integrated in the TTool framework.Computer Science, Software EngineeringComputer Science, Theory & MethodsComputer Sciencesysmlmodel-checkingformal verificationembedded systemstext::conference output::conference proceedings::conference paper