By the same authors

A Candid Industrial Evaluation of Formal Software Verification using Model Checking

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationICSE Companion 2014
DatePublished - 2014
Pages175-184
Number of pages10
PublisherACM
Original languageEnglish
ISBN (Print)978-1-4503-2768-8

Abstract

Model checking is a powerful formal analytical approach to verifying software and hardware systems. However, general industrial adoption is far from widespread. Some difficulties include the inaccessibility of techniques and tools and the need for further empirical evaluation in industrial contexts. This study considers the use of Simulink Design Verifier, a model checker that forms part of a modelling system already widely used in the safety-critical industry. Model checking is applied to a number of real-world problem reports, associated with aero-engine monitoring functions, to determine whether it can provide a practical route into effective verification, particularly for nonspecialists. The study also considers the extent to which model checking can satisfy the requirements of the extensive DO-178C guidance on formal methods. The study shows that the benefits of model checking can be realised in an industrial setting without specialist skills, particularly when it is targeted at parts of the software that are error-prone, difficult to verify conventionally or critical. Importantly, it shows that model checking can find errors earlier in the design cycle than testing, which potentially saves money, due to reduced scrap and rework.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations