MSE/MSSF Practicum Ideas
A comparitive analysis of specification languages
for design, development and verification
One way to develop secure and reliable code is to use a formal language.
However there are many demands placed on the language the developer
chooses in order to be sure that the application that is subsequently
developed in secure and reliable. Firstly the langauge must be expressive
and easy to use in order to allow the developer to specify the application.
Next the language must be ammenable to verifiaction techniques in order
to prove that the design has the required properties. Finally the language
ahould also be ammenable to program generation, either manually or automatically
(extremely difficult). This practicum will choose a set of formal languages
and through a series a small case studies, preform a comparitive analysis
of these langauges in terms of ease of specification, ease of verification
and ease of program generation.
Specifying Quality of Service
Taken
One important set of properties that an application has are its quality
of service (QoS) properties. An application will not be acceptable if
its performance does not meet the minimum requirements of the user.
This practicum will look at QoS properties and how they can be specified.
In particular it will investigate how the specification of QoS properties
can be integrated into existing formal and semi-formal specification
notations.
Autonomic Simulation Tool
Autonomic Systems have
been proposed as a possible solution to the increasing complexity of
modern computing system. In particular the "Self-*" properties
enable these systems to automatically configure components, automatically
discover and correct faults, automatically monitor and control resources
to ensure the optimal functioning with respect to the defined requirements
and proactively identify and protect from arbitrary attacks. These systems
are typically defined as a collection of interacting agents. When designing
a system, identifying all the emergent behaviours from these interactions
is problematical. The goal of this project is to build a simulator for
a class of autonomic systems to test if a system design has the required
behaviours and does not introduce additional malign behaviours.
If you are interested in these ideas or related projects please contact
Dr. David Sinclair.
|