Task Model Design and Analysis with Alloy

• Type: Article in International Conference Proceedings Book
• Date: 2023

Authors

Cunha, A (Author) Other; Macedo, N (Author) FEUP; Kang, E (Author) Other

Conference proceedings International

Title: RIGOROUS STATE-BASED METHODS, ABZ 2023

Pages: 303-320

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

Nancy, FRANCE, MAY 30-JUN 02, 2023

Indexing

ISI Web of Knowledge - 0 Citations

Scopus

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 18