Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A simple and flexible timing constraint logic
School of Innovation, Design and Engineering, Mälardalen University, Västerås.
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
2012 (Engelska)Ingår i: Leveraging applications of formal methods, verification and validation: technologies for mastering change : 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012 : proceedings / Part II / [ed] Tiziana Margaria ; Bernhard Steffen, Heidelberg: Encyclopedia of Global Archaeology/Springer Verlag, 2012, Vol. 2, s. 80-95Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

Formats for describing timing behaviors range from fixed menus of standard patterns, to fully open-ended behavioral definitions; of which some may be supported by formal semantic underpinnings, while others are better characterized as primarily informal notations. Timing descriptions that allow flexible extension within a fully formalized framework constitute a particularly interesting area in this respect. We present a small logic for expressing timing constraints in such an open-ended fashion, sprung out of our work with timing constraint semantics in the TIMMO-2-USE project [15]. The result is a non-modal, first-order logic over reals and sets of reals, which references the constrained objects solely in terms of event occurrences. Both finite and infinite behaviors may be expressed, and a core feature of the logic is the ability to restrict any constraint to just the finite ranges when a certain system mode is active. Full syntactic and semantic definitions of our formula language are given, and as an indicator of its expressiveness, we show how to express all constraint forms currently defined by TIMMO-2-USE and AUTOSAR. A separate section deals with the support for mode-dependencies that have been proposed for both frameworks, and we demonstrate by an example how our generic mode-restriction mechanism formalizes the details of such an extension.

Ort, förlag, år, upplaga, sidor
Heidelberg: Encyclopedia of Global Archaeology/Springer Verlag, 2012. Vol. 2, s. 80-95
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7610
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Kommunikations- och beräkningssystem
Identifikatorer
URN: urn:nbn:se:ltu:diva-39955DOI: 10.1007/978-3-642-34032-1_12Scopus ID: 2-s2.0-84868273940Lokalt ID: ee69017c-f222-4e51-adfe-837fda4b5a6bISBN: 9783642340321 (tryckt)OAI: oai:DiVA.org:ltu-39955DiVA, id: diva2:1013475
Konferens
International Symposium on Leveraging Applications of Formal Methods, Verification and Validation : 15/10/2012 - 18/10/2012
Anmärkning
Validerad; 2012; 20121113 (andbra)Tillgänglig från: 2016-10-03 Skapad: 2016-10-03 Senast uppdaterad: 2018-07-10Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Nordlander, Johan

Sök vidare i DiVA

Av författaren/redaktören
Nordlander, Johan
Av organisationen
Datavetenskap
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 134 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf