Formal description and validation for an integrity policy supporting multiple levels of criticality

Author

Fantechi, A. ; Gnesi, S. ; Semini, L.

Author_Institution

Dept. of Syst. & Inf., Firenze Univ., Italy

fYear

1999

fDate

8-8 Jan. 1999

Firstpage

129

Lastpage

146

Abstract

Formal methods are increasingly used to validate the design of software and hardware components of safety critical systems. In particular, formal validation is needed for those mechanisms which support the overall dependability of the systems. Inside the GUARDS project, a novel integrity mechanism has been proposed to implement the Multiple Levels of Criticality model within an object-oriented framework. We present the application of model checking techniques to the formal validation of this integrity level mechanism.

Keywords

formal verification; object-oriented methods; process algebra; safety-critical software; GUARDS project; Multiple Levels of Criticality model; formal methods; formal validation; hardware components; integrity policy; model checking; object-oriented framework; process algebra; safety critical systems; software components; software design validation; system dependability; Algebra; Automatic logic units; Carbon capture and storage; Costs; Electrical capacitance tomography; Hardware; Logic functions; Mechanical factors; Software design; Software safety;

fLanguage

English

Publisher

ieee

Conference_Titel

Dependable Computing for Critical Applications 7, 1999

Conference_Location

San Jose, CA, USA

Print_ISBN

0-7695-0284-9

Type

conf

DOI

10.1109/DCFTS.1999.814293

Filename

814293