Research Assistant Job - Project Sireum
Since January 2013 I am Master student at Kansas State University. I am also Research Assistant at SAnToS lab.
Bakar toolset
Since the beginning I am working on project Sireum. It is focused on toolset for analyzing Spark/Ada programs: Bakar. Spark is subset of Ada programming language extended by code contracts. More info here. Bakar contains two main tools: Alir (information flow analysis tool) and Kiasan (verification tool for code contracts).
The Kiasan tool is based on symbolic execution. Simply saying: it checks all possible code paths and discover possible issues (like variable overflow, side effects etc.). More info about Spark contracts can be found in Tokeneer Discovery Tutorial. Comprehensive description of Kiasan in contained in this paper.
Kiasan plugin for GPS
My first task was to integrate Kiasan tool (Java app) with GPS (GNAT Programming Studio).
I have never working on IDE plugins before. It was something totally new for me. That's why I was excited.
Plugins for GPS are written in PyGTK (Python graphic library). First I needed to learn Python and PyGTK. Then I followed GPS documentation (especially chapters 16 and 18).
The sample flow of running Kiasan plugin is as follows:
- right click on method (which you want to analyze) and choose 'Run Kiasan'
- handle this event and get method name and package name (will be needed to run Kiasan)
- run external Java program (Kiasan.jar) from Python code (it has command line interface, so I just needed to execute subprocess.call method), which generates JSON report
- parse JSON report and display it in the PyGTK window attached to the GPS
- add code highlighting, dependent on chosen method or case (in report window by double-click)
GPS along with Kiasan plugin is available in Sireum distribution, which can be downloaded from http://www.sireum.org/download.
In the demo below I am showing how to install Sireum distribution and GPS with Kiasan plugin on Windows.
By the way: Sireum Project is Open Source on github!
Do I like GRA job? Yes. It is very nice experience. I am able to work on Mac. I didn't have this opportunity before (I wouldn't buy it soon probably). I was able to learn Python (and PyGTK). I learn Design by Contract. I learn how to create plugin for IDE (GNAT Programming Studio). We have continues integration server - Jenkins: I learn how to manage it. I explore the World of 'High Assurance Software' and Ada programming language, which is most common in such environment. It is totally different than working as software developer in some company.
Recently I started working on second SAnToS' project: Medical Device Coordination Framework. Another interesting thing. But I will tell you about it in another post.
Interesting fact: Ada programming language was named after Ada Lovelace (1815–1852), who is credited as being the first computer programmer.