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

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.