Analysing Sanity of Requirements for Avionics Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00089171" target="_blank" >RIV/00216224:14330/16:00089171 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s00165-015-0348-9" target="_blank" >http://dx.doi.org/10.1007/s00165-015-0348-9</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s00165-015-0348-9" target="_blank" >10.1007/s00165-015-0348-9</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Analysing Sanity of Requirements for Avionics Systems

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Analysing Sanity of Requirements for Avionics Systems

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/7H13001" target="_blank" >7H13001: Critical System Engineering Acceleration</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Formal Aspects of Computing

ISSN

0934-5043

e-ISSN

—

Svazek periodika

28

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

19

Strana od-do

45-63

Kód UT WoS článku

000372262000003

EID výsledku v databázi Scopus

—