Integration of formal analysis into a model-based software development process

Michael Whalen, Darren Cofer, Steven Miller, Bruce H. Krogh, Walter Storm

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

36 Scopus citations

Abstract

The next generation of military aerospace systems will include advanced control systems whose size and complexity will challenge current verification and validation approaches. The recent adoption by the aerospace industry of model-based development tools such as Simulink® and SCADE SuiteTM is removing barriers to the use of formal methods for the verification of critical avionics software. Formal methods use mathematics to prove that software design models meet their requirements, and so can greatly increase confidence in the safety and correctness of software. Recent advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This paper describes how formal analysis tools can be inserted into a model-based development process to decrease costs and increase quality of critical avionics software.

Original languageEnglish (US)
Title of host publicationFormal Methods for Industrial Critical Systems - 12th International Workshop, FMICS 2007, Revised Selected Papers
Pages68-84
Number of pages17
DOIs
StatePublished - Jun 9 2008
Event12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007 - Berlin, Germany
Duration: Jul 1 2007Jul 2 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4916 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007
CountryGermany
CityBerlin
Period7/1/077/2/07

Keywords

  • Flight control
  • Model checking
  • Model-based development
  • Software verification

Fingerprint Dive into the research topics of 'Integration of formal analysis into a model-based software development process'. Together they form a unique fingerprint.

Cite this