 |
Conference papers
Towards a formal semantics of the TESL specification language
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.
Cited literature [9 references]
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, July 8, 2021 - 3:50:00 AM
Long-term archiving on: : Saturday, April 29, 2017 - 8:53:20 AM
Contributor : Frédéric Boulanger <>
Submitted on : Thursday, December 10, 2015 - 10:58:23 AM
Last modification on : Thursday, July 8, 2021 - 3:50:00 AM
Long-term archiving on: : Saturday, April 29, 2017 - 8:53:20 AM
File
article.pdf
Files produced by the author(s)