Past Final Year Projects

2009/2010

Title: Compensations in an Imperative Programming Language Supervisor: Adrian Francalanza and Gordon Pace Student: Lydia Vella Description: Apart from the standard programming constructs such as selection and looping, more elaborate constructs, such as exception handling, are used to provide more succinct ways of defining particular programming logic. The notion of compensations of programs and automated undoing of certain program chunks upon failure has been shown to be particularly useful in various domains. For example, consider programming a web portal for shopping: { (search <> ok); (deductStock <> restock); (credit <> refund); (packItem <> unpack) } <> notifyOperator. The <> operator is used here to enable the programmer to identify the action to be taken to undo a particular program fragment. In the example given above, if the action credit fails, the action restock will be executed to counteract deductStock. If, however, the individual instructions work fine, the individual compensations are replaced by the single notifyOperator() action. There are other more low level examples such as using compensations to implement backtracking in search problems. The aim of this project is to enrich an imperative programming language with the compensation construct, implementing a compiler for the language. Title: Dynamic Automata in LARVA Supervisor: Gordon Pace and Christian Colombo Student: John Paul Cassar Description: DATEs [1,2] are a real-time automata used to specify properties for the runtime verification of Java programs in the tool LARVA. This code can then be used during the execution of a Java system, ensuring its adherence to the represented properties. DATEs support various features, including clocks, channels and variables. Currently, LARVA takes a property written as a DATE, and generates a complete automaton. An alternative approach would be to give the description of DATEs as a function which given the current system configuration and a system event, creates the new state, thus generating the automaton on-the-fly depending on the path taken during the system execution, thus reducing memory requirements and enabling runtime-verification using infinite-state DATEs. The aim of this project is to rewrite LARVA to handle dynamic automaton generation, and explore its use on a sizable case study. References: C. Colombo. Practical runtime monitoring with impact guarantees of Java programs with real-time constraints. Master's thesis, University of Malta, 2008. C. Colombo, G. J. Pace, and G. Schneider. Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties. In FMICS'08, Italy, 2008. To appear in LNCS. 2008/2009 Title: Real-Time Logics and Slowdown Invariance for Runtime Monitoring Supervisor: Gordon Pace and Christian Colombo Student: Ingram Bondin Description: In many cases, it is desirable to check whether a program satisfies some constraint on its behaviour, known as a property. Sometimes, these constraints involve the element of time. For example, the software controlling a car spraying arm might be required to move away from the assembly line within 3 seconds of completing its task lest it crash into an oncoming car. Properties are expressed in various logics. Amongst the logics used to express time related properties is the formalism known as Timed Regular Expressions (TRE) [1]. Properties, once expressed, can be automatically compiled into monitors which can be added to the system's code in order to check whether a system is obeying the constraints or not. Unfortunately, in time critical systems, adding this monitoring code can slow down the system, which can mean that although the system does obey the property, the system plus the monitor does not obey it. This can mean that the monitor would report false results about the system. Similarly, a system might satisfy a property precisely because adding a monitor sufficiently slows it down to allow satisfaction to occour. Once the monitor is removed, a bug can therefore be introduced. How can one reason about when these problems will occour? In prior work, Colombo has already developed a theory of slowdown [2] which has been applied to reason about properties expressed in the logic known as duration calculus, which can be used to check which fragment of the logic is safe and which is not. For example, a system satisfying the property 'wait more than three seconds to activate', is not affected by slowing down the system, because at worst, it will simply start to take more to activate. The objective of this work is to use Colombo's theory to mathematically prove which fragment of the logic known as TRE does not suffer from the problems relating to the slowing down or speeding up of a system due to the addition or removal of monitors. Once this has been done, it is possible to determine which properties are safe with respect to these problems and which are not, giving extra guarantees to any software engineer which might need to use TRE to monitor real time applications. References: E. Asarin, P. Caspi, and O. Maler. A kleene theorem for timed automata. In LICS '97: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, page 160, Washington, DC, USA, 1997. IEEE Computer Society. C. Colombo, G. Pace, and G. Schneider. Safe runtime verification of real-time properties. 2008. Submitted for publication. Title: Statistics and Runtime Verification Supervisor: Gordon Pace and Christian Colombo Student: Andrew Gauci Description: Sometimes it is useful to answer questions such as: "What is the average number of packet retransmissions" in a communication protocol, or "How often does process P1 enter the critical section while process P2 waits" [3]. Such statistics gathered at runtime can be used to check properties which should be satisfied with a particular probability. For example the Eagle logic [1] is a tool which supports statistical properties. Another approach is to use statistics for optimization. Furthermore, verification of a property can be done on a sample of objects rather than all the objects [2]. In this proposed project you will be expected to extend the LARVA logic to be able represent such properties and consider possible optimizations through the use of statistics. References: H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtime verification. In VMCAI, pages 44{57, 2004. K. Bhargavan, C. A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and M. Viswanathan. Verisim: Formal analysis of network simulations. IEEE Trans. Software Eng., 28(2):129-145, 2002. B. Finkbeiner, S. Sankaranarayanan, and H. B. Sipma. Collecting statistics over runtime executions. Form. Methods Syst. Des., 27(3):253-274, 2005. Title: Counter-Example Visualisation for Runtime Verification Supervisor: Gordon Pace and Christian Colombo Student: Matthew Cachia Description: Once a bug is discovered using runtime verification, replaying the bug for debugging purposes may be augmented with the visualisation of the property that was violated, to enable relating the behaviour of the system with the expected property. Since LARVA properties are defined in terms of automata, the concurrent visualisation of the properties with the debug trace can be very effective. The aim of this project is to explore the use of counter example visualisation techniques within LARVA. Since it is planned that LARVA will support additional logics (which compile down to underlying automata), a framework to enable visualisation of other logics would also be required. 2007/2008 Title: Embedding Prolog in Haskell Supervisor: Gordon Pace Student: George Bonanno Description: Prolog is a well known declarative programming language in which one is allowed to specify terms and rules on these terms. The language then makes use of resolution to resolve these terms into concrete values (or otherwise refute the solution). The aim of this project is to build a subset of the Prolog syntax as an embedded language within Haskell (a functional language). You are then expected to implement the resolution solver for an input program written in this Prolog-like syntax. The main emphasis would be the investigation of optimisation techniques that can be expressed in Haskell when applying resolution. Alternatively you may also investigate alternate techniques to reach a particular clause proof. Title: Model Checking User-Interfaces Supervisor: Gordon Pace and Sandro Spina Student: Abigail Cauchi Description: Complex user interfaces, where certain actions may remove (or disable) certain controls and others re-enable them, are prone to bugs which are easily fixed but not so easily discovered. On the other hand, if we take a program and strip away all irrelevant and non-user-interface code, the resulting program is usually reasonably small and can be model checked for correctness. A similar technique has been used to model check programs for memory leaks. In this FYP, we will explore the possibility of applying this verification on a real-life programming language, and identify other aspects of user-interfaces which can be model checked in a similar manner. Title: An Embedded Domain Specific Language to Model, Transform and Quality Assure Business Processes in Business-Driven Development Supervisor: Gordon Pace Student: Luana Micallef Description: Business process models are usually produced by business analysts to graphical and textual communicate the current business processes to a software engineer in the IT department. As soon as business processes are updated to meet the new demands in the competitive market, the prior implementation of these processes has to be revised and possibly redesigned and re-implemented, adding up on the costs and the time required to update the system. Thus, for the implementation to remain consistent and evolve at the same pace as its business process model, the business-driven development methodology should be adopted. IT solutions that directly satisfy the business requirements, should ideally be developed and implemented in a Service-Oriented Architecture. In this project, we are proposing an embedded domain specific language to model, transform and quality assure business processes. With this language, the user would be able to declaratively define the business process models. Programmers will be able to pre-define a number of model transformations, which can then be used by the end-user (usually the business analyst) for automated transitions. Advanced users would be allowed to define their own model transformations and add them to the current provided list. Data-flow and control-flow errors in the business process model and the transformed models would be detected automatically. A model checking tool, such as CADP, shall be used to check the quality and properties of a modelled system. This domain specific language with provide the right abstraction for any user to define business process models and increase the user productivity by helping the user to produce correct and refined models, to keep up with the increasing demands in the competitive market. Title: Constrained Access to Code Libraries through Library Interfaces Supervisor: Gordon Pace and Sandro Spina Student: Clinton Mifsud Description: A problem when designing a code library is that one would usually want to constrain the way the user of the library accesses the functions provided in the library. Temporal constraints on library access can be very difficult to hard code, whether it's in terms of order of execution (eg this method should be called before this other one), or, even worse, if they are in terms of actual time (eg this function cannot be invoked more than once every 30 minutes unless this other one is invoked in the meantime). The aim of this project is to develop a framework to enable the programmer to give an interface to a code library (or possibly, class), which will be automatically translated into code causing runtime errors if these contraints are not satisfied. 2006/2007 Title: Tangonome: A tango music classifier Supervisor: Gordon Pace Student: Josef Attard Description: Nowadays the amount of digital music over the internet and inside homes is increasing rapidly. Moreover most people are highly selective about music and this gave rise to the demand for automatic genre classification systems. This explains why in the last ten years, several methods for automatic music classification have been tried out. In this project we primarily aim to show to which extent it possible to adapt such methods in order to classify specific subgenres of tango music. In a way this makes our taxonomy simpler to envision, but at the same time more sophisticated, given the high similarity within the subgenres. Tango music can be sub classified into a number of categories, primarily normal tangos, tango Vals, and milongas. Furthermore tango music evolved throughout the decades with clear cut distinctions between one era and another. In this project we present Tangonome which adds meta-data to tango music excerpts accordingly. We also attempt mood classification using a number of features, for which three different classifiers, more specifically KNN (K-Nearest Neighbor), SVM (Support Vector Machine) and GMM (Gaussian Mixture Model) are applied. Title: Model Checking Games Supervisor: Gordon Pace and Sandro Spina Student: Andrew Calleja Description: Games have been an area of study for computer science and artificial intelligence ever since the first computers were created. They not only provide us with a means of challenging our mental prowess alone and against other players but have also been successfully used as case studies for how computers may be taught to emulate human thought and intelligence. By studying games, and proving properties about them, computer scientists have been able to develop theories and techniques which have been subsequently used for other types of systems. Another, highly studied field of computer science is system verification. System verification goes beyond the normal validation techniques which prove only that a system is fit for its job. Verification makes sure that the system at hand satisfies its requirements fully by making sure that there are no hidden faults which validation techniques such as testing and simulation may not detect. To do so verification techniques make a thorough and complete search of the system and ensure that is bullet-proof as far as its requirements demand and can hence handle any situation it is required to without breaking down. These two fields of study have been sometimes combined together so as to prove a number of interesting, and sometimes surprising, properties about games. Since verification is a complete way to check a system, analysing games using its techniques proves properties about the latter which cannot be contested since they follow a rigorous proof-based approach. In our study we are interested in analysing how an automatic and relatively recently developed verification technique called Model Checking fares when attempting to verify properties about games as has been done before with other more established verification techniques. Our study will first focus on model checking itself: its steps, the structures utilised such as Kripke structures and binary decision diagrams, the logics involved such as CTL and mu-calculus temporal logics and the algorithms employed for automatic verification. The next part of the study will then focus on how the theory of model checking may be put to use for games themselves. Finally, we will consider two simple but important case studies: Tictactoe and Connect Four and use these to show how model checking can prove properties about these games by verifying them by means of two model checkers: SMV and Mucke. In parallel to this we will see which of the two mentioned temporal logics is more suitable for describing game properties and also obtain an indication of model checking's ability to scale up for games with large board sizes. Title: Embedding Origami Constructs Supervisor: Gordon Pace and Joseph Cordina Student: Gaetano Caruana Description: Origami is the art of paper folding where users build complicated constructions by performing a sequence of folds, resulting in aesthetic beauty. At first Origami, did not allow cuts in papers and only one paper could be used to build a model. But as time went by, Origami constraints were relaxed resulting into slightly different arts. Origami can be described using the seven axioms provided in the literature. In this dissertation we build a Domain Specific Embedded Language for Origami in Haskell, called OriDSEL, based on these seven axioms. OriDSEL gives a concise way on how to describe Origami models. A model description is described by a combination of basic axioms, and in turn this description can be reused as a basic component. This description can be evaluated into text, HTML, constraints description or a basic animation. OriDSEL also allows for modularity when building a model. Information about the particular modules is kept so as to allow for different evaluations at various levels of abstraction according to the users. knowledge of Origami. Title: ??? Supervisor: Gordon Pace and Joseph Cordina Student: Stephen Fenech Description: xxx Title: Embedding Geometric Constructions Supervisor: Gordon Pace and Joseph Cordina Student: Maria Grima Description: Domain-specific languages are used in specialised areas where only a specific set of commands, types and operations are required, pertaining to the domain in question. When these languages are hosted by another established language, they are referred to as domain-specific embedded languages. By making use of the tools available for the hosting language, the development effort for an embedded language is greatly simplified and the focus can be set on the domain functionality required. This project proposes a domain-specific embedded language for geometric constructions, with Haskell as the host language. We show how users can easily describe construction models through operations which are based on Euclidean axioms and through other pre-defined constructions which serve as building blocks. These construction models can then be represented in tutorial formats that can be textual, diagrammatic or animated. The language also provides functionality for testing properties and proving conjectures on defined constructions. Title: Imperative Mode-Automata Supervisor: Gordon Pace and Joseph Cordina Student: Ruth Schembri Description: Different forms of abstraction mechanisms and language constructs are designed in programming languages, to model, in natural manner, some form of application problem, so that problems within the target area of the language may be solved as easily as possible by application programmers. This thesis presents a programming language extension to be applied over imperative programming languages, in order to structure programs to reflect the organization and behavior of multimodal systems through the combined use of imperative languages and an overlying abstraction model to represent modes. The natural structure of multinational system behavior is observed to resemble that of a finite state machine, involving a number of states, or modes, each responsible for executing a particular task or operation of the system, and a number of transitions between these modes, activated immediately upon their labeling condition being satisfied. The language designed in this thesis, bases its structure upon that of a finite state machine, in order to reflect the multimodal behavior of the systems as accurately as possible. In addition to this basic structure, a number of complimenting constructs are supported by the language, each of which has been carefully analysed with respect to its impact upon the overall simplicity of the language. A syntax is designed for the language to aid in the natural expression of the multimodal behaviour, and the semantics for the language are defined formally using operational semantics notation. A demonstration compiler for the language is built to illustrate the development of multimodal systems using the designed language, Imperative Mode-Automata. Finally, through the use of a case study for the language, we demonstrate how this language improves the overall readability, maintainability and reusability of the multimodal systems developed in an imperative programming language using Imperative Mode-Automata. 2005/2006 Title: Using a Domain Specific Language for Computer Game Playing Supervisor: Gordon Pace Student: William Borg Barthet Description: Domain-Specific Languages (DSLs) are programming languages that allow users to create artefacts relating to some specialized area. Such domain engineers benefit greatly by using DSL, as they provided with a set of tools catered specifically for that problem area. Also they need only familiarize themselves with the syntax of the DSL and can make use of it without being expert programmers. Combinator libraries enhance the flexibility of such DSLs by allowing users to specify unforeseen constructs from more basic ones. Embedding the DSL into a suitable host language reduces the development time and effort required to create the DSL. Such languages are known as Domain-Specific Embedded Languages (DSELs). In order to make artefacts created using the DSEL run more efficiently, they can be complied into an optimized rendition in another language. This project attempts to evaluate the applicability of complied combinator library-based domain specific embedded languages to computer game playing. Particularly for specifying many different games within a class in a way that is easy for humans to describe and also easy for machines to read and use. This language infrastructure is then used by a number of applications to highlight the utility of having a machine .readable complied game description that can be specified by a domain engineer. These applications will be able to generate a game player and playing interface that would allow the game to be tested. The player can also be optimized by finding an appropriate weight set that works well for that particular game. Also, the game.s complexity can be automatically analyzed. A number of the many potential uses for the compiled game description are discussed. Title: Implementing a Compiler/Interpreter for pi-Calculus Supervisor: Adrian Francalanza Student: Christian Tabone Description: We consider pi-Calculus as the foundation of our study, by analyzing the syntax and semantics that this notion offers. We then describe a simple typing convention that will be used to type-check pi-Calculus programs. This is followed by the description of an intermediate representation of the pi-Calculus, and we suggest how several machine implementations can use this representation to stimulate pi-Calculus programs. A parser and compiler are constructed. These will translate pi-Calculus program into this intermediate representation. Subsequently, we concentrate on David N. Turner's Abstract Machine, to develop a Stand-Alone Virtual Machine capable of interpreting pi-Calculus, and simulating a correct execution on the semantic meaning of the given program. We tackle a number of optimizations that are incorporated with the architecture of the Stand-Alone machine, to produce a more efficient simulation. We present the architecture for an interactive virtual machine to allow a user to communicate with the program during execution, and we give an illustration on the differences between a Stand-Alone virtual machine and an Interactive virtual machine. We then verify the correctness of the virtual machines` implementations, by presenting a number of examples. We conclude by examining the capability of the interactive virtual machine, in creating an abstract layer between the implementation details of pi-Calculus programs and the user. We illustrate how a typical user is unable to distinguish between two pi-Calculus programs that offer the same functionalities, but have a different internal implementation. 2004/2005 Title: Abductive Runtime Verification of Lustre Programs Supervisor: Gordon Pace and Mike Rosner Student: Nikolai Sultana Description: Fully automating the process of verifying a system is fraught with complexity, in spite of significant progress in this area, and does not necessarily lead to understanding the nature of perceived faults. We present an approach to automate diagnosing a system by subjecting the system to passive monitoring, part of a technique called runtime verification. Being a partial technique, we justify its use by its potential to glean information about faults once they arise in monitored programs. Abductive runtime verification can derive additional benefit from this context by inferring possible causes of deviation from the expected program behavior. Our approach enables observed faults to be mapped to elements in the program.s code from which they arose. Moreover, the fault.s symptoms are elaborated into an explanation and possible causes are suggested by a diagnostic engine. These benefit from knowledge about the structure and state of the running program to generate program slices for individual symptoms. Finally, a representation of these slices is produced in a graph language for visualization. These artifacts are intended to provide the user with select information to assist them in focusing on the relevant parts of a program following an observed failure. In the course of the project we have explored ideas from Artificial Intelligence and Formal Methods and incorporated techniques from both fields to implement an abductive runtime verification tool for programs written in Lustre, a synchronous programming language. Title: Gesture Oriented, Combinator-Based Calligraphy Supervisor: Gordon Pace Student: Liana Sammut Description: xxx 2003/2004 Title: Ordering Functions for Game Playing Supervisor: Gordon Pace Student: David Captur Description: xxx Title: SharpHDL: A Hardware Description Languege Embedded in C Sharp Supervisor: Gordon Pace Student: Christine Vella Description: SharpHDL is a language for designing, specifying and verifying hardware. It is embedded in the object-oriented programming language C# and therefore hardware definitions are treated as first-class objects in the host language. Thus, in developing our hardware objects, we are able to use object-oriented features like polymorphism and inheritance, as well as the various tools developed for C#. Being a structural hardware description language, it provides means to describe circuits by specifying the components and their interconnections. It also supports higher-order circuits, which are referred to as Generic Circuits. These are circuit descriptions which take other circuits as their input. The language also allows definition of circuit specification by describing observers expressing safety properties. Observers are circuits that take the inputs and outputs of a circuit under observation and output a single wire stating whether the combination of inputs and outputs satisfy the given specifications. In addition, circuit descriptions can be translated to verification tools, thus enabling a designer to verify circuit specifications. Presently, SharpHDL supports translation to SMV, which is standard model checker. The language can generate other types of description formats, including translations to other hardware description languages. Using these features, SharpHDL was used to design and verify the equivalence of two circuit implementations of Fast Fourier Transform (FFT) algorithms-the radix-2 FFT and the radix-2 FFT. FFTs are efficient algorithms to compute the Discrete Fourier Transform which is widely used in digital signal processing and other related fields. We also discuss the embedding of a simple language over SharpHDL that caters for modular verification and refinement. Modular verification allows a verification problem to be decomposed into smaller manageable sub-problems and each sub-problem is verified individually. Refinement allows the verification of an implementation against an abstract specification defining its legal behavior. We analyze how the characteristics of SharpHDL give more user-control over the verification process, thus highlighting the various contributions given by the embedded approach.