Title :
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
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;
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
DOI :
10.1109/SCAM.2012.25
