Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89468| Título: | Task model design and analysis with alloy |
| Autor(es): | Cunha, Alcino Macedo, Nuno Kang, Eunsuk |
| Palavras-chave: | Air traffic control Alloy Arrival manager HAMSTERS Interactive system analysis Task models |
| Data: | 2023 |
| Editora: | Springer, Cham |
| Revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Citação: | 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 |
| Resumo(s): | 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. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/89468 |
| ISBN: | 978-3-031-33162-6 |
| e-ISBN: | 978-3-031-33163-3 |
| DOI: | 10.1007/978-3-031-33163-3_23 |
| ISSN: | 0302-9743 |
| Versão da editora: | https://link.springer.com/chapter/10.1007/978-3-031-33163-3_23 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
