Publication
Real-time MTL with durations as SMT with applications to schedulability analysis
dc.contributor.author | Matos, Andre de | |
dc.contributor.author | Leucker, Martin | |
dc.contributor.author | Pereira, David | |
dc.contributor.author | Pinto, Jorge Sousa | |
dc.date.accessioned | 2021-09-24T13:58:05Z | |
dc.date.embargo | 2031-12 | |
dc.date.issued | 2020 | |
dc.description.abstract | This 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.sponsorship | This 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.version | info:eu-repo/semantics/publishedVersion | pt_PT |
dc.identifier.doi | 10.1109/TASE49443.2020.00016 | pt_PT |
dc.identifier.uri | http://hdl.handle.net/10400.22/18539 | |
dc.language.iso | eng | pt_PT |
dc.publisher | IEEE | pt_PT |
dc.relation | Research Centre in Real-Time and Embedded Computing Systems | |
dc.relation.publisherversion | https://ieeexplore.ieee.org/document/9405311 | pt_PT |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | pt_PT |
dc.subject | Metric temporal logic | pt_PT |
dc.subject | Schedulability analysis | pt_PT |
dc.subject | Constraint programming | pt_PT |
dc.subject | Satisfiability modulo theories | pt_PT |
dc.title | Real-time MTL with durations as SMT with applications to schedulability analysis | pt_PT |
dc.type | conference object | |
dspace.entity.type | Publication | |
oaire.awardTitle | Research Centre in Real-Time and Embedded Computing Systems | |
oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/157676/PT | |
oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UID%2FCEC%2F04234%2F2013/PT | |
oaire.citation.conferencePlace | Hangzhou, China | pt_PT |
oaire.citation.endPage | 56 | pt_PT |
oaire.citation.startPage | 49 | pt_PT |
oaire.citation.title | 2020 International Symposium on Theoretical Aspects of Software Engineering (TASE) | pt_PT |
oaire.fundingStream | 6817 - DCRRNI ID | |
oaire.fundingStream | 6817 - DCRRNI ID | |
project.funder.identifier | http://doi.org/10.13039/501100001871 | |
project.funder.identifier | http://doi.org/10.13039/501100001871 | |
project.funder.name | Fundação para a Ciência e a Tecnologia | |
project.funder.name | Fundação para a Ciência e a Tecnologia | |
rcaap.rights | embargoedAccess | pt_PT |
rcaap.type | conferenceObject | pt_PT |
relation.isProjectOfPublication | 8c7c9c17-5755-4336-b394-738550c57d62 | |
relation.isProjectOfPublication | 278bd9d6-8d0a-4e53-8ca5-53afe4cd7ea2 | |
relation.isProjectOfPublication.latestForDiscovery | 8c7c9c17-5755-4336-b394-738550c57d62 |
Files
Original bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- COM_CISTER_TASE_2020.pdf
- Size:
- 629.09 KB
- Format:
- Adobe Portable Document Format