<div class="description">
<p>Security modeling is the foundation to formal verification which is a core  requirement for high assurance systems. This thesis explores how security models can be  built in a simple and expressive manner using the Metaslang specification language in  Specware. The models are subsequently translated, via the Specware to Isabelle Interface,  to be proven for correctness in Isabelle which is a generic, interactive theorem proving  environment. It is found that the translation between Specware and Isabelle is almost  seamless and there is much potential in the use of Isabelle/HOL to discharge proof  obligations that arise in developing Specware specifications, although the actual proving  requires substantial knowledge and experience in logical calculus.
</p>
<br>Subjects:</div>
<div class="fn value">
<dl><dd>Ng, Eng Siong.</dd>
<dd>Koh, Chuan Lian</dd></dl></div>
Internet Archive identifier