Analysing sanity of requirements for avionics systems

DOI10.1007/S00165-015-0348-9zbMATH Open1335.68131arXiv1510.02669OpenAlexW2266282164MaRDI QIDQ282095FDOQ282095

Authors: J. Barnat, Petr Bauch, Nikola Beneš, Luboš Brim, Jan Beran, Tomáš Kratochvíla 

Publication date: 12 May 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Abstract: In the last decade it became a common practice to formalise software requirements to improve the clarity of users' expectations. In this work we build on the fact that functional requirements can be expressed in temporal logic and we propose new sanity checking techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate approaches to consistency and redundancy checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). We further report on the experience obtained from employing the consistency and redundancy checking in an industrial environment. To complete the sanity checking we also describe a semi-automatic completeness evaluation that can assess the coverage of user requirements and suggest missing properties the user might have wanted to formulate. The usefulness of our completeness evaluation is demonstrated in a case study of an aeroplane control system.

Full work available at URL: https://arxiv.org/abs/1510.02669

Recommendations

• Sanity Checks in Formal Verification
• Lightweight validation of natural language requirements
• Requirements specifications checking of embedded real time software
• High-automation proofs for properties of requirements models
• Verification of software requirements on program systems represented by attribute transition systems

zbMATH Keywords

linear temporal logicrequirement engineeringsanity checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Application models in control theory (93C95)

Cites Work

• Title not available (Why is that?)
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Title not available (Why is that?)
• Title not available (Why is that?)
• Diagnostic Information for Realizability
• Sanity Checks in Formal Verification
• Efficient detection of vacuity in temporal model checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (5)

• Finding boundary elements in ordered sets with application to safety and requirements analysis
• Timed automata relaxation for reachability
• Hashing-based approximate counting of minimal unsatisfiable subsets
• A weakness measure for GR(1) formulae
• Title not available (Why is that?)

Uses Software

• mCRL2
• DiVinE
• NuSMV
• iFEST
• RATSY
• mCRL

This page was built for publication: Analysing sanity of requirements for avionics systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q282095)