Use of SPARK in a resource constrained embedded system. - Chad Loseby; Peter Chapin; Carl Brandon (SIGAda, 2009)