Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/68525
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Brunel, Julien | por |
dc.contributor.author | Chemouil, David | por |
dc.contributor.author | Cunha, Alcino | por |
dc.contributor.author | Macedo, Nuno | por |
dc.date.accessioned | 2020-12-11T19:36:43Z | - |
dc.date.available | 2020-12-11T19:36:43Z | - |
dc.date.issued | 2019 | - |
dc.identifier.issn | 2075-2180 | - |
dc.identifier.uri | https://hdl.handle.net/1822/68525 | - |
dc.description.abstract | Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next. Traditionally this simulation mode cannot take into consideration additional temporal logic constraints, such as arbitrary fairness restrictions, substantially reducing its usability for debugging the modelled system behaviour. Similarly, when a specification is false, even if all its counter-examples combined also form a set of behaviours, most model checkers only present one of them to the user, providing little or no mechanism to explore alternatives. In this paper, we present a simple on-the-fly verification technique to allow the user to explore the behaviours that satisfy an arbitrary temporal logic specification, with an interactive process akin to simulation. This technique enables a unified interface for simulating the modelled system and exploring its counter-examples. The technique is formalised in the framework of state/event linear temporal logic and a proof of concept was implemented in an event-based variant of the Electrum framework. | por |
dc.description.sponsorship | This work is financed by the ERDF - European Regional Development Fund - through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 - and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01- 0145-FEDER-016826, and the French Research Agency project FORMEDICIS ANR-16-CE25-0007. The third author was also supported by the FCT sabbatical grant with reference SFRH/BSAB/143106/2018. | por |
dc.language.iso | eng | por |
dc.publisher | Open Publishing Association | por |
dc.relation | SFRH/BSAB/143106/2018 | por |
dc.rights | openAccess | por |
dc.title | Simulation under arbitrary temporal logic constraints | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
oaire.citationStartPage | 63 | por |
oaire.citationEndPage | 69 | por |
oaire.citationVolume | 310 | por |
dc.date.updated | 2020-12-11T15:31:35Z | - |
dc.identifier.doi | 10.4204/EPTCS.310.7 | por |
dc.subject.fos | Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática | por |
sdum.export.identifier | 7593 | - |
sdum.journal | Electronic Proceedings in Theoretical Computer Science, EPTCS | por |
oaire.version | VoR | por |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
fide19.pdf | 569,33 kB | Adobe PDF | Ver/Abrir |