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.

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.

Sending email from Rails application

It took me a while to configure sending email from Rails application. I went through many different tutorials, blogs, StackOverflow posts etc. Step, by step I found working configuration.

To send emails I use ActionMailer. First you need to generate mailer:

rails generate mailer UserMailer

It will create UserMailer class in app/mailers directory. In this class we need to define our method for sending emails:

class UserMailer < ActionMailer::Base
  default from: "[email protected]"

  def send_email(user_email, content)
  	@user_email = user_email
  	@content = content
  	mail(to: "[email protected]", subject: "Email from")

Then in the directory app/views/user_mailer we need to create template for our email: send_email.html.erb (this name must match the name of action created in UserMailer class):

<!DOCTYPE html>
    <meta content='text/html; charset=UTF-8' http-equiv='Content-Type' />
      From: <%= @user_email %>
      <%= @content %>

(*) If you do not want to send html you can create plain text and name file send_email.text.erb.

Now, the hardest part. Configuration of smtp. You need to add it to config/environments/development.rb (or test.rb or production.rb). I found this configuration working for gmail:

# set delivery method to :smtp, :sendmail or :test
  config.action_mailer.delivery_method = :smtp
  config.action_mailer.perform_deliveries = true

  # these options are only needed if you choose smtp delivery
  config.action_mailer.smtp_settings = {
    :address        => '',
    :port           => 587,
    :domain         => '',
    :authentication => :login,
    :user_name      => '[email protected]',
    :password       => 'your_password',
    :enable_starttls_auto => true

The last thing is call ActionMailer from our app:

UserMailer.send_email(params[:from], params[:content]).deliver

Form for sending email can looks like that:

<%= form_tag '/send_email', method: 'post' do %>
	<div class="field">
		Email<br />
    <%= email_field_tag :from %>

	<div class="field">
		Content<br />
    <%= text_area_tag :content, nil, rows: 10, cols: 25 %>

  <div class="actions">
    <%= submit_tag "Send", class: "btn btn-large btn-primary" %>
<% end %>

For that you need to configure action in controller and match route e.g.:

match '/send_email', to: 'your_controller#your_action'

Method send_mail (from UserMailer class) can have as much parameters as you need. It can be also 0. In above example, the params are just rendered in the email template (send_email.html.erb file).