Task Model Design and Analysis with Alloy

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2023

Autores

Cunha, A (Autor) Outra; Macedo, N (Autor) FEUP; Kang, E (Autor) Outra

Ata de Conferência Internacional

Título: RIGOROUS STATE-BASED METHODS, ABZ 2023

Páginas: 303-320

9th International Conference on Rigorous State-Based Methods (ABZ)

Nancy, FRANCE, MAY 30-JUN 02, 2023

Indexação

ISI Web of Knowledge - 0 Citações

Scopus

Outras Informações

ID Authenticus: P-00Y-CCP

DOI: 10.1007/978-3-031-33163-3_23

Abstract (EN): 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 18