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 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

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.

Quick look at Java Spring MVC framework

Java software market is still bigger than .NET. Many times, when I heard that some friend on mine is working as Java Web Developer, he is using Spring MVC framework. Finally I decided to look at this (most popular?) Java Web Framework.

I started with tutorials: Introduction to Spring MVC and Spring with JPA and Hibernate.

First surprise for me was a lot of xml based configuration, which needs to be written by developer. E.g. we need to configure which class is controller by declaring its path in xml file (servlet-config.xml). For some other elements we need to provide long uris as packages’ names. So easy to misspell. This is ‘configuration over convention’, instead of ‘convention over configuration’ as it is in Ruby on Rails or ASP.NET MVC.

As an example, look at this piece of xml, which is needed to handle JSON and XML requests (all written by hand):

<bean class="org.springframework.web.servlet.view.ContentNegotiatingViewResolver">
		<property name="order" value="1" />
		<property name="contentNegotiationManager">
			<bean class="org.springframework.web.accept.ContentNegotiationManager">
					<bean class="org.springframework.web.accept.PathExtensionContentNegotiationStrategy">
								<entry key="json" value="application/json" />
								<entry key="xml" value="application/xml" />
		<property name="defaultViews">
				<bean class="org.springframework.web.servlet.view.json.MappingJacksonJsonView" />
				<bean class="org.springframework.web.servlet.view.xml.MarshallingView">
						<bean class="org.springframework.oxm.xstream.XStreamMarshaller">
							<property name="autodetectAnnotations" value="true" />

Going back to controller: besides its configuration in XML file, we need to add annotation @Controller on its class and @RequestMapping on methods (no default routing). Additionally we always need to return the name of view (instead of some default value). Here is a sample controller with one action:

public class HelloWorldController {

    public String helloWorld(Model model) {
        model.addAttribute("message", "Hello World!");
        return "helloWorld";

Above code will return the view helloWorld.jsp (according to convention, located in webapp/WEB-INF/jsp/ directory):

<!DOCTYPE html>
        Message: ${message}

The result should looks like that:

Spring MVC Hello World

Connecting application with database is not easier. Adding dependencies and writing code to make Hibernate working with the app took 1h(!) in Pluralsight tutorial (Spring with JPA and Hibernate). It is over 50 lines of xml. Additionally as we know – it is very easy to make a mistake during writing xml. In ASP.NET MVC it can be done automatically (eventually we can change data source by specifying connection string). I didn’t find easier way to do that (in Spring). Of course we can use copy/paste method and just set some properties, but…where is code generation for that?

After all, I would like to notice how big step was made by other MVC Web Frameworks like Rails, Django or ASP.NET MVC. Lot of stuff, which has to be written by hand in Spring, is already implemented under framework layer (in Rails, Django and ASP.NET MVC). However Spring MVC was also big step ahead, when it was created in 2002. In this video people are explaining that (e.g. because of Spring they do not need to rewrite lots of boilerplate code anymore).

I wonder whether next version of Spring MVC will have more ‘conventions’ and default configurations. It will make the framework more developer friendly and easier to maintain.

If you want to start with Spring MVC i recommend you to start with tutorials: Introduction to Spring MVC and Spring with JPA and Hibernate. You can also find this website useful, as well as Spring Framework Reference Documentation. I didn’t read any book, but I found those two most often recommended: Spring Recipes and Spring in Action.

The Ten-Day MBA

The Ten-Day MBA cover

Chad Fowler, in his book “The Passionate Programmer” recommended a book The Ten-Day MBA. The reason, why he recommend it, is the fact that successful programmer should know the basics of marketing. E.g. to be aware how much his work is worth.

The Ten-Day MBA is an overview of fundamental basics of economy, business, finance, leadership and even real estate. In my opinion, this book is not only for programmers. It is for everyone! You can find there difference between monetarists and Keynesian economy, the product life cycle (from factory to customer), the difference between corporation and private business, time estimation of projects, business strategies etc.

I strongly recommend this book. I was studying at University of Economics 3 years (Bachelor degree). This book contains all most important concepts I learned there.

You can find it on amazon.

Ninja Rails Developer

Warning: this configuration was tested only on MacOS X.

To create default project in Rails we just need to run command:

rails new my_app

However it creates project without many useful gems. I found nice Gem-set and some configuration hacks in Michael Hartl’s tutorial.

Instead of standard test framework (TestUnit) he use RSpec (which is more popular among Rails developers). To generate project without standard test, run command:

rails new my_app --skip-test-unit

Then use his Gemfile (this link is kept up to date). Copy it a paste into my_app/Gemfile. I recommend to uncomment everything (to use all Gems from the file).

Once Gemfile is modified, you need to install gems:

bundle install

Then you can run RSpec test:

bundle exec rspec

You may need to point the tests’ directory:

bundle exec rspec rspec/

It would be nice to run them with just ‘rspec’ command. To do that we need to run following commands (if we used RVM to install Rails):

rvm get head && rvm reload

cd ~/projects/my_app

bundle install --without production --binstubs=./bundler_stubs

After those steps you should be able to run RSpec with:


You should get a warning, that to maintain this possibility you need to add following line to ~/.bash_profile if it exists, otherwise add it to ~/.bash_login:

source ~/.profile

Michael Hartl’s Gem file contains ‘guard’. It allows us to run RSpec test each time, when we change some file (after save).

To initialize guard (if all above steps are performed, otherwise you need to add ‘bundle exec ‘ at the beginning):

guard init

It creates Guardfile in main project directory, which specify when tests should be run (which files should be monitored). To run guard:


The last improvement is use the test server Spork. It allows to run tests faster. Without Spork, RSpec needs to reload entire Rails environment before run the tests (in each run). Spork loads the environment once, and then maintains a pool of processes for running future tests. Unfortunately it works only on POSIX systems (which means: doesn’t work on Windows).

To setup spork run:

spork --bootstrap

Then change spec/spec_helper.rb file to something like that:

require 'rubygems'
require 'spork'

Spork.prefork do
  ENV["RAILS_ENV"] ||= 'test'
  require File.expand_path("../../config/environment", __FILE__)
  require 'rspec/rails'
  require 'rspec/autorun'

  Dir[Rails.root.join("spec/support/**/*.rb")].each {|f| require f}
  RSpec.configure do |config|
    config.mock_with :rspec
    config.fixture_path = "#{::Rails.root}/spec/fixtures"
    config.use_transactional_fixtures = true
    config.infer_base_class_for_anonymous_controllers = false

Spork.each_run do
  # This code will be run each time you run your specs.

You also need to configure RSpec to automatically use Spork. To do that, modify .rspec file:


To run Spork:


You can test difference between running tests with and without spork.

time rspec

In my case it was 4.821s without Spork, and 0.784 with Spork.

The disadvantage of Spork is that after e.g. changes in database we need to restart it.

The screencast showing advanced setup by Michael Hartl is available for free here. If you use SublimeText (as I do), you can follow this screencast to adjust it for Rails development. After that you will be able even to run tests from SublimeText!

Sign in with facebook (OAuth): how to and threats

Many websites provide possibility to authorize with OAuth protocol (e.g. using facebook account).

How to

In ASP.NET application it is very easy to implement. Check this 3 minutes long screencast by Scott Hanselman.

In Rails it is a little bit more complex, but also not big deal. There is nice Rails cast #360 about it (12 minutes).


However it is good to know what data we are providing when we click ‘Login with facebook’. I implemented facebook auth with omniauth-facebook library (according to above rails cast). I was surprised when I look at the source code.

This is auth data available for developer, when we sign in with facebook:

  :provider => 'facebook',
  :uid => '1234567',
  :info => {
    :nickname => 'jbloggs',
    :email => '[email protected]',
    :name => 'Joe Bloggs',
    :first_name => 'Joe',
    :last_name => 'Bloggs',
    :image => '',
    :urls => { :Facebook => '' },
    :location => 'Palo Alto, California',
    :verified => true
  :credentials => {
    :token => 'ABCDEF...', # OAuth 2.0 access_token, which you may wish to store
    :expires_at => 1321747205, # when the access token expires (it always will)
    :expires => true # this will always be true
  :extra => {
    :raw_info => {
      :id => '1234567',
      :name => 'Joe Bloggs',
      :first_name => 'Joe',
      :last_name => 'Bloggs',
      :link => '',
      :username => 'jbloggs',
      :location => { :id => '123456789', :name => 'Palo Alto, California' },
      :gender => 'male',
      :email => '[email protected]',
      :timezone => -8,
      :locale => 'en_US',
      :verified => true,
      :updated_time => '2011-11-11T06:21:03+0000'

We provide our email(!), timezone and even location! Actually I was not aware of that. I thought facebook provides just basic info like name and photo.

We should think twice before we sign in to some website with OAuth. Especially due to providing our email address. Malicious websites can use it for sending spam.