Download complete thesis as PDF

be easily understandable by someone that is familiar with functional programming.
However, for a beginner it requires a substantial amount of effort to understand and use
them. We have documented our understanding of Monads in this thesis in hopes of
smoothing the learning curve for Monads.
It was found that the translation between Specware and Isabelle is almost
seamless and that there is much potential in the use of Isabelle/HOL to discharge proof
obligations that arise in developing Specware specifications. The actual proving using
Isabelle requires substantial knowledge and experience in logical calculus, which put
closed results outside the scope of this thesis.
In conclusion, through our work in this thesis we found that Specware, together
with Isabelle, has great potential for specifying and verifying a security model. They will
be great tools for experienced user in the theorem proving field. We hope that the
illustrated use of Sets and Monads in our LPSK example will also be useful to future
users of Specware.
B.
FUTURE WORKS
1.
Proving of the Model Using Isabelle
Isabelle is an interactive theorem prover with lots of capabilities that had yet to be
explored in this thesis. Further studies may be performed to understand the various
approaches in theorem proving using Isabelle and the pros and cons of each approach.
With the understanding of each theorem proving approach, a complete proof for the
LPSK model could be explored.
2.
Segregation of the Model into an Abstract Canonical Model and a
Refined Model
No conscious effort has been put in when specifying the LPSK model to first
create an abstract model which is subsequently refined. Work could be done to segregate
a reusable canonical abstract model from the current specification. Refinements to the
88