https://www.mdu.se/

mdu.sePublications
Planned maintenance
A system upgrade is planned for 10/12-2024, at 12:00-13:00. During this time DiVA will be unavailable.
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Verifying Event-Based Timing Constraints by Translation into Presburger Formulae
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0001-5297-6548
2017 (English)In: Lecture Notes in Computer Science, vol. 10471, Springer Verlag , 2017, p. 19-33Conference paper, Published paper (Refereed)
Abstract [en]

Abstract modeling of timing properties is often based on events. An event can be seen as a sequence of times. Timing constraints can then be expressed as constraints on events: an example is the TADL2 language that has been developed in the automotive domain. Event-based constraints can express timing properties of implementations as well as timing requirements. An important step in timing verification is then to show that any events that comply with the properties of the implementation, i.e., that describe the timings of its possible behaviours, also satisfy the requirements. Real-time software is often organised as a set of periodically repeating tasks, especially in domains with time-critical systems like automotive and avionics. This implementation naturally yields periodic events, where each event occurrence belongs to a periodically repeating time window. An interesting question is then: if some events are periodic in this fashion, will they then fulfil a timing constraint that describes a timing requirement? We show, for a number of TADL2 timing constraints, how to translate this implication into an equivalent Presburger formula. Since Presburger logic is decidable, this yields an automated method to decide whether the periodic implementation satisfies the timing requirements or not. Initial experiments with a Presburger solver indicate that the method is practical.

Place, publisher, year, edition, pages
Springer Verlag , 2017. p. 19-33
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10471 LNCS
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:mdh:diva-36563DOI: 10.1007/978-3-319-67113-0_2ISI: 000851022200002Scopus ID: 2-s2.0-85029541817ISBN: 9783319671123 (print)OAI: oai:DiVA.org:mdh-36563DiVA, id: diva2:1145260
Conference
22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, 18 September 2017 through 20 September 2017
Available from: 2017-09-28 Created: 2017-09-28 Last updated: 2022-11-18Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Lisper, Björn

Search in DiVA

By author/editor
Lisper, Björn
By organisation
Embedded Systems
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • 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