Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89468Registo completo
| Campo DC | Valor | Idioma |
|---|---|---|
| dc.contributor.author | Cunha, Alcino | por |
| dc.contributor.author | Macedo, Nuno | por |
| dc.contributor.author | Kang, Eunsuk | por |
| dc.date.accessioned | 2024-03-12T22:07:13Z | - |
| dc.date.available | 2024-03-12T22:07:13Z | - |
| dc.date.issued | 2023 | - |
| dc.identifier.citation | Cunha, A., Macedo, N., Kang, E. (2023). Task Model Design and Analysis with Alloy. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds) Rigorous State-Based Methods. ABZ 2023. Lecture Notes in Computer Science, vol 14010. Springer, Cham. https://doi.org/10.1007/978-3-031-33163-3_23 | por |
| dc.identifier.isbn | 978-3-031-33162-6 | - |
| dc.identifier.issn | 0302-9743 | - |
| dc.identifier.uri | https://hdl.handle.net/1822/89468 | - |
| dc.description.abstract | This paper describes a methodology for task model design and analysis using the Alloy Analyzer, a formal, declarative modeling tool. Our methodology leverages (1) a formalization of the HAMSTERS task modeling notation in Alloy and (2) a method for encoding a concrete task model and compose it with a model of the interactive system. The Analyzer then automatically verifies the overall model against desired properties, revealing counter-examples (if any) in terms of interaction scenarios between the operator and the system. In addition, we demonstrate how Alloy can be used to encode various types of operator errors (e.g., inserting or omitting an action) into the base HAMSTERS model and generate erroneous interaction scenarios. Our methodology is applied to a task model describing the interaction of a traffic air controller with a semi-autonomous Arrival MANager (AMAN) planning tool. | por |
| dc.description.sponsorship | The work of the first two authors is financed by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project LA/P/0063/2020. The last author was supported in part by the National Science Foundation award CCF-2144860. | por |
| dc.language.iso | eng | por |
| dc.publisher | Springer, Cham | por |
| dc.rights | openAccess | por |
| dc.subject | Air traffic control | por |
| dc.subject | Alloy | por |
| dc.subject | Arrival manager | por |
| dc.subject | HAMSTERS | por |
| dc.subject | Interactive system analysis | por |
| dc.subject | Task models | por |
| dc.title | Task model design and analysis with alloy | por |
| dc.type | conferencePaper | por |
| dc.peerreviewed | yes | por |
| dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-031-33163-3_23 | por |
| oaire.citationStartPage | 303 | por |
| oaire.citationEndPage | 320 | por |
| oaire.citationVolume | 14010 LNCS | por |
| dc.date.updated | 2024-02-10T08:00:11Z | - |
| dc.identifier.doi | 10.1007/978-3-031-33163-3_23 | por |
| dc.identifier.eisbn | 978-3-031-33163-3 | - |
| dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
| dc.subject.fos | Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática | por |
| sdum.export.identifier | 13227 | - |
| sdum.journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | por |
| oaire.version | AM | por |
| Aparece nas coleções: | ||
