Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover
Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise, France.
Ericsson AB, Sweden.
Uppsala University, Sweden.
RISE - Research Institutes of Sweden, ICT, SICS.ORCID iD: 0000-0003-3079-8095
2018 (English)In: International Conference on Software Engineering and Formal Methods / [ed] Einar Broch Johnsen and Ina Schaefer, 2018, p. 239-253Conference paper, Published paper (Refereed)
Abstract [en]

An important task of testing a telecommunication protocol consists in analysing logs. The goal of log analysis is to check that the timing and the content of transmitted messages comply with specification. In order to perform such checks, protocols can be described using a constraint modelling language. In this paper we focus on a complex protocol where some messages can be delayed. Simply introducing variables for possible delays for all messages in the constraint model can drastically increase the complexity of the problem. However, some delays can be calculated, but this calculation is difficult to do by hand and to justify. We present an industrial application of the Coq proof assistant to prove a property of a 4G protocol and validate a constraint model. By using interactive theorem proving we derived constraints for message delays of the protocol and found missing constraints in the initial model.

Place, publisher, year, edition, pages
2018. p. 239-253
Series
Lecture Notes in Computer Science ; 10886
Keywords [en]
Testing of telecommunication protocol; Constraint programming; Formal proof; Coq
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:ri:diva-34224DOI: 10.1007/978-3-319-92970-5_15Scopus ID: 2-s2.0-85049015507ISBN: 978-3-319-92969-9 (print)ISBN: 978-3-319-92970-5 (electronic)OAI: oai:DiVA.org:ri-34224DiVA, id: diva2:1233379
Conference
International Conference on Software Engineering and Formal Methods (SEFM 2018), part of STAF 2018
Available from: 2018-07-17 Created: 2018-07-17 Last updated: 2019-01-08Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopushttps://doi.org/10.1007/978-3-319-92970-5_15

Authority records BETA

Carlsson, Mats

Search in DiVA

By author/editor
Carlsson, Mats
By organisation
SICS
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 40 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
v. 2.35.7