Medical Device Coordination Framework
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.
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!
