SPARK

Master of Science in Computer Science

After 1 year and 8 months of being a Graduate Student at Kansas State University and Research Assistant at SAnToS Lab Research Group I got my Master of Science degree.

Courses I took:

In my first semester as a Graduate Research Assistant at SAnToS Lab I was working on integration Bakar Kiasan with GNAT Programming Studio (using Python and PyGTK).

In Summer 2013 I started my actual research work, which is captured in my Master Thesis: A Model-Driven Development and Verification Approach for Medical Devices. The main problem of my research was to propose translation of AADL/BLESS models to SPARK Ada programming language. I created PCA Pump Prototype for BeagleBoard-xM platform, by translating already existing models (using translations developed by me), and performed verification (static analysis) using SPARK Verification Tools.

This is a video from my defense:

Unfortunately, QuickTime crashed 3 minutes before the end. Fortunately, you can catch up with slides.

I created additional video with PCA Pump Prototype demonstration. Pump is developed in SPARK Ada, and it runs on BeagleBoard-xM platform.

Patient Controlled Analgesia (PCA) pump is a medical device, which allows the patient to self-administer small doses of narcotics (usually Morphine, Dilaudid, Demerol, or Fentanyl). PCA pumps are commonly used after surgery to provide a more effective method of pain control than periodic injections of narcotics. A continuous infusion (called a basal rate) permits the patient to receive a continuous infusion of pain medication. Patient can also request additional boluses, but only in specified intervals. It prevents from overinfusion. In addition to basal and patient bolus, clinician can also request bolus called clinician bolus or square bolus.

My Master Thesis in PDF format can be found here. LaTeX source is available here.

I spent 2 years at Kansas State University (4 months as an Exchange Student, and 20 months as a Graduate Student). I had very good time and I learnt a lot. I really recommend to get Master degree from a different University than you get your Bachelor. Wroclaw University of Technology (where I got my Bachelor) is more practical. Graduates are ready to work at the industry. Kansas State is more theoretical and research oriented. I had an opportunity to experience both and I am very happy with that!


Medical Device Coordination Framework

Patient room - future

As a Research Assistant at SAnToS Lab I am working on Medical Device Coordination Framework. It is a long term research effort. MDCF is an implementation of Integrated Clinical Environment. There is many people involved in it. Not only from my University. There are folks from University of Pennsylvania and some other researchers who cooperate with us. My part of research is focused on code translation. You can call it Model Driven Development. The long-term research goal is to create a AADL/BLESS to SPARK Ada translator for Medical Devices.

Technologies

AADL stands for Architecture Analysis & Design Language. It is modeling language, which allows to describe hardware and software parts of the system. It can be represented in graphical and textual form.

BLESS stands for Behavioral Language for Embedded Systems with Software. It is an extension to AADL language. AADL can be extended by language annexes. BLESS is one of them. It is designed to prove embedded software/system conformance to specification. In other words: to verify the AADL model.

SPARK is a programming language and static verification technology designed specifically for the development of high integrity software. It is subset of Ada programming language. It contains all features of Ada, except:

  • Pointers
  • Exceptions
  • Aliasing between variables
  • All Concurrency features
  • Side effects in expressions and functions

However, it contains toolset for Software Verification, such as:

  • Examiner – analyze code and ensures that it conforms to the SPARK language; also verify program to some extent using Verification Conditions (VC)
  • Simplifier – simplify Verification Conditions generated by Examiner
  • Proof Checker – prove the Verification Conditions

I blogged about SPARK Ada recently.

Research background

The ultimate goal has a big scope. The goal is to deliver a platform, which allows different medical devices to work together. Moreover, there will be monitored and controlled by centralized system.

We use and create a lot of different technologies. From AADL, BLESS, DML to SPARK Ada, Java, through many other. Most of them are still under development. I work mainly with AADL, BLESS and SPARK Ada. The biggest challenge for me is to understand how AADL models should be mapped to SPARK Ada in real-World. Unfortunately, I cannot find some Open Source examples on github. Companies treat it as their intellectual property, and do not share it. More over, the AADL committee still did not decide how some AADL constructs should be mapped to Software. Thus, my role is to propose it (based on existing work).

There is an AADL to Ada code generator: Ocarina. It is written in Ada and it uses Ada features, which are not in SPARK language. However, it is a good point to start. Another resource I am based on is Aerospace Standard – Architecture Analysis & Design Language (AADL) V2 Programming Language Annex Document. It describe data types translation and base for ports communication.

The essence of AADL models is port-based communication. Usually implemented in publish-subscribe mode. It allows to interaction between different components of the system.

Sample medical device

To create code translator for Medical Devices, I needed some example of Medical Device. One member of our research group, Brian Larson created AADL/BLESS models of Patient-controlled analgesia Infusion Pump. This device, is used to infuse a pain killer. The dose can be controlled by patient. He also created Open PCA Pump Requirements. Document, which describe precisely functionalities of PCA Pump. My role is to develop AADL/BLESS to SPARK Ada translation schemes and translate existing PCA Pump models, to assure that translation makes sense.

PCA Pump

Research plan

There are many issues and problems to solve in this project. One of them is SPARK limitation. Besides excluded features mentioned above, SPARK 2014 does not support multitasking (yet). SPARK 2005 support it in some extent (with Ravenscar profile). Thus I use mainly SPARK 2005.

The plan is as follows:

  • Create AADL/BLESS to SPARK Ada translation schema
  • Manually implement working PCA-Pump prototype on BeagleBoard-xM based on Requirement document to find out possible implementation issues
  • Manually translate AADL/BLESS models to SPARK Ada, reusing code created during implementation
  • Create AADL/BLESS to SPARK Ada translator based on manual translated code

How it goes?

I started working on this project around 1 year ago. Most of the time, I spend on studying AADL, SPARK Ada, BLESS and Ravenscar Profile. I thought, I would accomplish much more. However during the process I faced a lot of problems and I had to Shave the Yak. First challenge was to run SPARK Ada code on BeagleBoard-xM device. In cooperation with Ada Core, we got cross-compiler, which works for its processor. It took around 3 months, because cross-compiler was under development. After around half a year of exploring, I came up with AADL ports translation schema (based on AADL annex document). Simultaneously, I was working on PCA Pump implementation (based on its Requirements Document). Most of it is described in SPARK Ada programming for ARM-based device(BeagleBoard-xM). It allowed me to better understand SPARK Ada development environment and create translation schemes for AADL packages threads. SPARK Ada development is much different than Java, C# or Python. After many hours spent on AADL/BLESS models analysis, I created mapping from BLESS to SPARK Ada.

For now, most of the work is done. Especially, translations schema. I have less than 2 months to finish everything. My plan is to refactor existing PCA Pump implementation and create final mock of code translated from AADL/BLESS models. Additionally I want to add implementation to some ‘translated’ part and apply SPARK Verification tools and AUnit tests. Finally, I will need to describe everything in my Master Thesis.

My thoughts so far…

Development for safety-critical systems is totally different, than creating Web or Mobile applications. My research adventure is very fascinating and allow me to discover new things everyday. It gives me different perspective of Software Development, which will be useful in the future. No matter if I would work for company producing Aircrafts or Space Shuttles. It will be valuable also for Web/Mobile Start-up in Silicon Valley or personal Mobile App. Finally I understand where UML and variety of Software Design Processes can be applied. Programming in SPARK Ada requires deep thinking and understanding about how every small part of the program work. There is no high abstraction layer, where calling some library function will do all work. It allows to understand what is underneath and how powerful languages like C#, Java or Python are.

If you are at the University now, I strongly recommend you to join some Research Group. Or at least talk to some of your professors and ask if you can do some Research-oriented project for him. No matter, if you are Graduate or Undergraduate student. If research topic is out of your comfort zone, then it is even better!

outside comfort zone


SPARK Ada programming language

Before I joined SAnToS Lab, I heard about Ada programming language only a few times. I thought it is an ancient language, that nobody is using anymore. I assumed, that only reason why somebody may bother are some legacy applications written 30 years ago. I thought that safety-critical and high-assurance systems are developed in C/C++ or even Assembly language.

I was wrong.

Ada programming language

First version of Ada programming language – Ada 83 – was designed to meet the US Department of Defence Requirements formalized in “Steelman” document. Since that time, Ada evolved. There were Ada 95, Ada 2005 and Ada 2012 (released in December 10, 2012). Ada is activelly used in many Real-World projects, e.g. Aviation (Boeing 777’s Software is written in Ada), Railway Transportation, Commercial Rockets, Satellites and even Banking. One of the main goals of Ada is to ensure software correctness and safety. The picture below, shows what is the goal of Ada: prevent the Developer from introducing bugs into system by rich tooling and language properties.

Ada responsibilities

Ada does not use curly braces. The code listing below shows “Hello, World” in Ada:

with Ada.Text_IO; 
use Ada.Text_IO;

procedure Hello is 
begin   
  Put_Line ("Hello, world!"); 
end Hello;

Basic constructs

The table below, shows C# code, and equivalent Ada code.

C# Ada
x = 5;
x := 5;
x == 5
x = 5
x != 5
x /= 5
// comment
-- comment
int i = 2;
Console.WriteLine(i);
i : Integer := 2;
Put_Line(Integer'Image(i));
if (a > b)  
{
  Console.WriteLine("Condition met");  
}  
else  
{
  Console.WriteLine("Condition not met");
}
if a > b then   
 Put_Line("Condition met");
else   
 Put_Line("Condition not met"); 
end if;
switch(i) 
{
  case 0:     
    Console.WriteLine("zero");     
    break;   
  case 1:
    Console.WriteLine("one");     
    break;
  case 2:     
    Console.WriteLine("two");     
    break;   
  default:     
    Console.WriteLine("none");     
}
case i is   
  when 0 => Put_Line("zero");   
  when 1 => Put_Line("one");   
  when 2 => Put_Line("two");   
  when others => Put_Line("none");
end case;
for (int i=1; i<=10; ++i)  
{
  Console.WriteLine("Iteration: ");   
  Console.WriteLine(i);   
  Console.WriteLine("");  
}
for i in 1 .. 10 loop
  Put_Line("Iteration: ");   
  Put_Line(Integer'Image(i));
  Put_Line("");
end loop;
while(a != b)  
{
  Console.WriteLine("Waiting"); 
}
while a /= b loop   
  Put_Line("Waiting"); 
end loop;
do 
{
  a++;    
} 
while(a!=10);
loop   
  a := a + 1;   
  exit when a = 10; 
end loop;

Packages

The equivalent for C# class – in Ada – is package. It has two files: specification (.ads file) and body (.adb file). It is like header (.h) and implementation (.cpp) files for class definition in C++. Additionally:

  • class variables in C# conforms to ‘global’ variables in Ada package (the name ‘global’ in Ada package means that variable is visible for entire package, not entire application like in C/C++)
  • C# class have methods, which returns value or not (void). In Ada, methods are called subprograms. There are two distinguished types of them: functions (returns something) and procedures (does not return anything).

Here is sample C# class:

class Person  
{
  public int publicVar;

  private int privateVar;

  void MyMethod(int param)
  {
    // do stuff
  }

  public int MultiplyBy(int param) 	
  {
    return param * 2
  }
}

And its equivalent package in Ada:

-- person.ads
package Person is
  publicVar : Integer; 	

  procedure MyMethod(Param : Integer);   
   
  function MultiplyBy(Param : Integer) return Integer; 
end Person;
-- person.adb
package body Person is 	
  privateVar : Integer;

  procedure MyMethod(Param : Integer)
  is
  begin
    -- do stuff
  end;

  function MultiplyBy(Param : Integer)
  is
    Result : Integer;
  begin
    Result := Param * 2;
    return Result;
  end;
end Person;

SPARK Ada

SPARK programming language is based on Ada. Thus, it is usually referred as “SPARK Ada”.

SPARK is a programming language and static verification technology designed specifically for the development of high integrity software. First version was designed over 20 years ago. SPARK excludes some Ada constructs (i.e. pointers, dynamic memory allocation or recursion) to make static analysis feasible. Additionally SPARK contains tool-set for Software Verification:

  • Examiner – analyze code and ensures that it conforms to the SPARK language; also verify program to some extent using Verification Conditions (e.g. array index out of range, type range violation, division by zero, numerical overflow etc.)
  • Simplifier – simplify Verification Conditions generated by Examiner
  • Proof Checker – prove the Verification Conditions

Using SPARK, a developer takes a Z specification and performs a stepwise refinement from the specification to SPARK code. For each refinement step a tool is used to produce verification conditions (VC’s), which are mathematical theorems. If the VC’s can be proved then the refinement step will be known to be valid. However if the VC’s cannot be proved then the refinement step may be erroneous.

First version of SPARK (SPARK 83) was based on Ada 83. The second version (SPARK 95) – on Ada 95. Current version – SPARK 2005 – is based on Ada 2005. It is a subset of Ada 2005 with annotations. The annotation language support flow analysis and formal verification. Annotations are encoded in Ada comments (via the prefix --#). It makes every SPARK 2005 program, valid Ada 2005 program. Code listing below shows example SPARK 2005 package specification.

package Odometer
--# own Trip, Total : Integer;
is
	procedure Zero_Trip;
	--# global out Trip;
	--# derives Trip from ;
	--# post Trip = 0;

	function Read_Trip return Integer;
	--# global in Trip;

	function Read_Total return Integer;
	--# global in Total;

	procedure Inc;
	--# global in out Trip, Total;
	--# derives Trip from Trip & Total from Total;
	--# post Trip = Trip~ + 1 and Total = Total~ + 1;

end Odometer;

It is an interface for simple Odometer. There are 4 subprograms (2 procedures and 2 functions):

  • Zero_Trip procedure – reset Odometer to 0
  • Read_Trip function – returns current distance
  • Read_Total function – returns total distance traveled
  • Inc procedure- increment total and current distance by 1

Annotation global means that subprogram uses some global variable. Postfix in, out or in out means that particular variable is read, write or read and write respectively. Annotation derives says that some variable value depends on other variables. E.g. in procedure Inc variable Trip is dependent on its current value (before procedure call). Annotations pre and post define pre- and postconditions of procedure (only post is present in above example). We can see, that in Zero_Trip procedure postcondition requires that variable Trip is equal to 0. In procedure Inc, postconditions requires that variables Trip and Total are incremented by 1 (‘~‘ is the value of variable before procedure call). Annotation own expose private variables for use in public methods specification.

We can see, that SPARK contracts describe the functionality of particular subprograms. It is like documentation. You can find more about SPARK contracts in Tokeneer Discovery tutorial and SPARK 2005 to SPARK 2014 Mapping Specification.

The most popular IDE for SPARK Ada development is GNAT Programming Studio. There is also Eclipse plugin GNATbench.

The next version, SPARK 2014 (based on Ada 2012) is under development. There is partial tool support (in GNAT Programming Studio), but some language features are still not supported. It is worth to mention, that Ada 2012 contains code contracts. Thus SPARK 2014 is just subset of Ada 2012. There are no additional constructs like annotations in SPARK 2005, because now, contracts are part of the language.

In real-world applications, the embedded critical components are written in SPARK while the non-critical components are written in Ada.

Summary

I am working with SPARK Ada for more than 1 year. My (beginner) thoughts are as follows:

  • I don’t like the syntax. It is not developer friendly. You need to do a lot of repetitions, of the same code (e.g. subprograms declaration/definition). Syntax is very verbose, e.g. code blocks starts with begin and ends with end keywords. It means more writing than in case when you use ‘curly braces’ for that.
  • It is very hard to create valid and working SPARK program. There are many rules and limitations (e.g. no dynamic allocation).
  • Quite steep learning curve. Additionally, it is not easy to find some resources like tutorials, books, videos.
  • SPARK Ada IDE – GNAT Programming Studio – is very specific, and different than the most popular IDEs (e.g. Visual Studio or Eclipse). It is also less powerful, in case of e.g. intellisense, key shortcuts or project manipulations.

From my perspective, SPARK is a temporary subset of Ada, chosen for software verification. Once, verification techniques evolves, more features of Ada are getting included in SPARK. Maybe, in some day, there will be no SPARK, but just Ada, and tools will be able to verify (reason about) all its features.

More about Ada you can find at Ada Programming at Wikibooks, AdaCore University (video tutorials) and at ada2012.org website. Good place to start getting familiar with SPARK is Tokeneer Discovery tutorial (SPARK 2005) and SPARK 2014 tutorial. This lecture gives SPARK overview in nutshell. More about SPARK 2014 can be found in SPARK 2014 website, SPARK 2014 Toolset User’s Guide and SPARK 2014 Reference Manual. To go deeper, there is a book SPARK: THE PROVEN APPROACH TO HIGH INTEGRITY SOFTWARE by John Barnes.


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.