Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK

Author

Thiagarajan, Hariharan ; Hatcliff, John ; Belt, Jason ; Robby

Author_Institution

Dept. of Comput. & Inf. Sci., Kansas State Univ., Manhattan, KS, USA

fYear

2012

fDate

23-24 Sept. 2012

Firstpage

132

Lastpage

137

Abstract

This tool paper describes the design and implementation of an interactive environment for discovering and browsing information flow in SPARK programs. SPARK is a subset of Ada that has been used in a number of industrial contexts for implementing certified safety and security critical systems. SPARK requires explicit specification of information flow properties in the form of procedure contracts. To write such contracts, developers need to understand the data and control dependencies in the program. Our tool Bakar Alir, implemented as an Eclipse Plug-in, utilizes classic slicing and chopping techniques to assist developers in writing information flow contracts.

Keywords

contracts; formal specification; information retrieval; program slicing; safety-critical software; software tools; Ada; Bakar Alir; Eclipse Plug-in; SPARK program; certified safety; data dependency; formal specification; information flow browsing; information flow contracts; interactive environment; program chopping; program control dependency; program slicing; security critical system; Abstracts; Contracts; Input variables; Security; Software; Sparks; IDE support; chopping; slicing; spark;

fLanguage

English

Publisher

ieee

Conference_Titel

Source Code Analysis and Manipulation (SCAM), 2012 IEEE 12th International Working Conference on

Conference_Location

Trento

Print_ISBN

978-1-4673-2398-7

Type

conf

DOI

10.1109/SCAM.2012.25

Filename

6392111