Towards a formal semantics of the TESL specification language

Hai Nguyen Van 1, 2, 3 Thibaut Balabonski 1, 2, 3 Frédéric Boulanger 4, 1, 3, 5 Safouan Taha 1, 5, 3 Benoît Valiron 1, 5, 3 Burkhart Wolff 1, 2, 6, 3 Lina Ye 1, 5, 3
1 LRI - Laboratoire de Recherche en Informatique
2 UP11 - Université Paris-Sud - Paris 11
3 Université Paris-Saclay
4 MODHEL - LRI - Modélisation hétérogène (LRI)
LRI - Laboratoire de Recherche en Informatique
5 CentraleSupélec
6 CNRS - Centre National de la Recherche Scientifique
Abstract : Most relevant industrial modeling problems depict hetero-geneity issues when combining different paradigms. Designing such systems with discrete and continuous parts necessarily raises formal verification problems. We focus on a synchronous heterogeneous specification language, called TESL. In particular, it allows the expression of interrelations of clocks and — unlike other existing languages — is able to express time-triggered behaviors above event-triggered ones. We are interested in formalizing such a language to derive a verification framework, including model-checking, and testing. The long-term purpose of this work is to develop in the Isabelle/HOL proof assistant, a formal semantics for such a language. In the current paper, we present and compare three complementary semantic approaches for our problem.
Keywords : Formal Methods Theorem Prover Heterogeneity Synchronicity Time Model Logic
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download
https://hal-centralesupelec.archives-ouvertes.fr/hal-01239669
Contributor : Frédéric Boulanger <>
Submitted on : Thursday, December 10, 2015 - 10:58:23 AM
Last modification on : Thursday, February 7, 2019 - 2:59:34 PM
Long-term archiving on : Saturday, April 29, 2017 - 8:53:20 AM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01239669, version 1

Collections

UMR8623 | LRI-MODHEL | TDS-MACS | UNIV-PARIS-SACLAY | INRIA | CENTRALESUPELEC | LRI-VALS

Citation

Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Safouan Taha, Benoît Valiron, et al.. Towards a formal semantics of the TESL specification language. 3rd International Workshop on the Globalization Of Modeling Languages (GEMOC 2015), Benoit Combemale; Julien Deantoni; Jeff Gray, Sep 2015, Ottawa, Canada. pp.14-19. ⟨hal-01239669⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

684

Files downloads

104

Contact

CCSD