Using SPARK-Ada to Model and Verify a MILS Message Router. - Bryan Rossebo; Paul W. Oman; Jim Alves-Foss; Ryan Blue; Paul Jaszkowiak (ISSSE, 2006)