The Importance of Formal Verification in User Interactions: A Case Study in Aircraft Management

Model Checking, a powerful method of formal verification, has been employed in this article to ensure that systems conform to specific properties. The focus was on aircraft management, with a particular interest in the crucial process of checking in customers for a flight. The main objective was to ensure the reliability and accuracy of this essential step in air travel. To achieve this goal, I chose NuSMV as my verification tool, but the process began with system modeling and requirements specification. A detailed model was created, describing the various stages of customer check-in.User interactions and specific rules were precisely specified.The NuSMV tool was applied to a single specification initially, enabling an initial assessment of system conformity. The results were analyzed, and this specification was used as a starting point for future perspectives. The approach is to explore how NuSMV could provide counter-examples for incorrect specifications, paving the way for continuous improvements in the design of the customer check-in process for flights.