Repository logo
 
Publication

Real-time MTL with durations as SMT with applications to schedulability analysis

2020Conference object Embargoed access
Simple item page
dc.contributor.authorMatos, Andre de
dc.contributor.authorLeucker, Martin
dc.contributor.authorPereira, David
dc.contributor.authorPinto, Jorge Sousa
dc.date.accessioned2021-09-24T13:58:05Z
dc.date.embargo2031-12
dc.date.issued2020
dc.description.abstractThis paper introduces a synthesis procedure for the satisfiability problem of RMTL- ∫ formulas as SAT solving modulo theories. RMTL- ∫ is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL- ∫ with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL- ∫ formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach.pt_PT
dc.description.sponsorshipThis work was partially supported by BMVI project IHATEC / SecurePort; by National Funds through FCT/M-CTES (Portuguese Foundation for Science and Technology), within the CISTER Research Unit (UID/CEC/04234) and the INESC TEC (UIDB/50014/2020); also by the Norte Portugal Regional Operational Programme (NORTE 2020) under the Portugal 2020 Partnership Agreement, through the European Regional Development Fund (ERDF) and also by national funds through the FCT, within project NORTE-01–0145-FEDER-028550 (REASSURE).pt_PT
dc.description.versioninfo:eu-repo/semantics/publishedVersionpt_PT
dc.identifier.doi10.1109/TASE49443.2020.00016pt_PT
dc.identifier.urihttp://hdl.handle.net/10400.22/18539
dc.language.isoengpt_PT
dc.publisherIEEEpt_PT
dc.relationResearch Centre in Real-Time and Embedded Computing Systems
dc.relation.publisherversionhttps://ieeexplore.ieee.org/document/9405311pt_PT
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/pt_PT
dc.subjectMetric temporal logicpt_PT
dc.subjectSchedulability analysispt_PT
dc.subjectConstraint programmingpt_PT
dc.subjectSatisfiability modulo theoriespt_PT
dc.titleReal-time MTL with durations as SMT with applications to schedulability analysispt_PT
dc.typeconference object
dspace.entity.typePublication
oaire.awardTitleResearch Centre in Real-Time and Embedded Computing Systems
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/157676/PT
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UID%2FCEC%2F04234%2F2013/PT
oaire.citation.conferencePlaceHangzhou, Chinapt_PT
oaire.citation.endPage56pt_PT
oaire.citation.startPage49pt_PT
oaire.citation.title2020 International Symposium on Theoretical Aspects of Software Engineering (TASE)pt_PT
oaire.fundingStream6817 - DCRRNI ID
oaire.fundingStream6817 - DCRRNI ID
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.nameFundação para a Ciência e a Tecnologia
project.funder.nameFundação para a Ciência e a Tecnologia
rcaap.rightsembargoedAccesspt_PT
rcaap.typeconferenceObjectpt_PT
relation.isProjectOfPublication8c7c9c17-5755-4336-b394-738550c57d62
relation.isProjectOfPublication278bd9d6-8d0a-4e53-8ca5-53afe4cd7ea2
relation.isProjectOfPublication.latestForDiscovery8c7c9c17-5755-4336-b394-738550c57d62

Files

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
COM_CISTER_TASE_2020.pdf
Size:
629.09 KB
Format:
Adobe Portable Document Format
Download

Collections

ISEP – CISTER – Comunicações em eventos científicos