ePrints

Formal verification of a space system's user interface with the IVY workbench

Lookup NU author(s): Professor Michael HarrisonORCiD

Downloads

• Accepted version [.pdf]

Licence

This is the authors' accepted manuscript of an article that has been published in its final definitive form by IEEE, 2016.

For re-use rights please refer to the publisher's terms and conditions.

Abstract

This paper describes the application of the IVY workbench to the formal analysis of a user interface for a safety-critical aerospace system. The operation manual of the system was used as a requirement document, and this made it possible to build a reference model of the user interface, focusing on navigation between displays, the information provided by each display, and how they are interrelated. Usability-related property specification patterns were then used to derive relevant properties for verification. This paper discusses both the modeling strategy and the analytical results found using the IVY workbench. The purpose of the reference model is to provide a standard against which future versions of the interface may be assessed.

Publication metadata

Author(s): Campos JC, Sousa M, Alves MCB, Harrison MD

Publication type: Article

Publication status: Published

Journal: IEEE Transactions on Human-Machine Systems

Year: 2016

Volume: 46

Issue: 2

Pages: 303-316

Print publication date: 01/04/2016

Online publication date: 27/04/2015

Acceptance date: 09/03/2015

Date deposited: 12/11/2015

ISSN (print): 2168-2291

ISSN (electronic): 2168-2305

Publisher: IEEE

URL: http://dx.doi.org/10.1109/THMS.2015.2421511

DOI: 10.1109/THMS.2015.2421511

Altmetrics

Share