Proving dynamic properties in an aerospace application

Author

Nadjm-Tehrani, Simin ; Strömberg, Jan-Erik

Author_Institution

Dept. of Comput. & Inf. Sci., Linkoping Univ., Sweden

fYear

1995

fDate

5-7 Dec 1995

Firstpage

2

Lastpage

10

Abstract

We give an exposition to an ongoing research effort in cooperation with aerospace industries in Sweden. We report on an application of formal verification techniques on a landing gear system. This system consists of actuating hydromechanic and electromechanic hardware, and of controlling software components. We emphasize the need for modelling techniques and languages covering the whole spectrum from informal engineering documents, to hybrid mathematical models. In this modelling process we give as much weight to the physical environment as to the controlling software. We show the application of two verification methods for proving safety and timeliness properties of the closed loop system; first, using the proof system of extended duration calculus, and second by symbolic model checking

Keywords

aerospace computing; aircraft control; calculus; closed loop systems; formal verification; real-time systems; state feedback; actuating electromechanic hardware; actuating hydromechanic hardware; aerospace application; closed loop system; dynamic properties proving; extended duration calculus; formal verification techniques; hybrid mathematical models; informal engineering documents; landing gear system; modelling techniques; proof system; safety; symbolic model checking; timeliness properties; Aerodynamics; Aerospace industry; Application software; Closed loop systems; Control systems; Formal verification; Gears; Hardware; Mathematical model; Safety;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Systems Symposium, 1995. Proceedings., 16th IEEE

Conference_Location

Pisa

ISSN

1052-8725

Print_ISBN

0-8186-7337-0

Type

conf

DOI

10.1109/REAL.1995.495190

Filename

495190