Integrating Simulink Models into the Model Checker Cosmos

Autor: Béatrice Bérard, Benoît Barbot, Serge Haddad, Yann Duplouy
Přispěvatelé: Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), Modélisation et Vérification (MoVe), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), IRT SystemX, Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), IRT SystemX (IRT SystemX), Duplouy, Yann
Jazyk: angličtina
Rok vydání: 2018
Předmět:
Zdroj: Application and Theory of Petri Nets and Concurrency-Petri Nets 2018
39th International Conference on Applications and Theory of Petri Nets and Concurrency
39th International Conference on Applications and Theory of Petri Nets and Concurrency, Jun 2018, Bratislava, Slovakia. pp.363-373, ⟨10.1007/978-3-319-91268-4_19⟩
Application and Theory of Petri Nets and Concurrency ISBN: 9783319912677
Petri Nets
Popis: We present an implementation for Simulink model executions in the statistical model-checker Cosmos.We take profit of this implementation for an hybrid modeling combining Petri nets and Simulink models.
Nous présentons une implémentation pour l'exécution de modèles Simulink dans le model-checker Cosmos.Cette implémentation est ensuite utilisée pour la simulation de modèles hybrides, combinant des réseaux de Petri et des modèles Simulink.
Databáze: OpenAIRE