Past M.Sc. Dissertations
  • Title: PolyLARVA - Towards a language agnostic runtime verification framework
    Supervisor: Adrian Francalanza, Gordon Pace, Christian Colombo
    Student: Ruth Mizzi
    Submitted: 2012
    Download: PDF

    Abstract: A software system's development is commonly driven by a set of requirements which specify the behavior expected from the system throughout its execution. Ensuring that the specified behavior is maintained by a system at all times is a daunting task, which is aggravated further by the complexity of the systems involved. The drive towards modular systems, where components can be integrated seamlessly to provide the desired functionality, means that many systems are now no longer one monolithic application. Most non-trivial systems are created out of a combination of many technologies and languages which are integrated together. The challenge is that of being able to verify the behavior of each one of the components making up the system when these are running together as one integrated solution, regardless of the fact that they have been implemented using different technologies. Although the popularity of runtime monitoring has increased in recent years, many approaches are centered around particular technologies or programming languages. Any monitoring architecture is usually composed of two components: the property specification and verification component and the instrumentation component. By separating these two parts and allowing them to be replaced by pluggable components, a monitoring framework can become much more versatile in the properties which can be verified and universal in the technologies supported. The project proposed will investigate the possibility of producing a language agnostic runtime verification framework. The aim is to develop a proof of concept tool that can be used to verify, at runtime, systems which are an amalgamation of a number of programs written in different languages and running on different platforms.

  • Title: A Discrete Theory of Slowdown for Synchronous Systems
    Supervisor: Gordon Pace
    Student: Ingram Bondin
    Submitted: 2011
    Download: PDF

    Abstract: One often needs to verify that a system satisfies some particular property. These properties sometimes impose real-time constraints on the system. These constraints depend not only on the operation of the software, but also on the platform on which the software is running. If the platform is changed, the system as a whole will change its timing characteristics, which may mean that a previously verified property will be broken. However, not all real-time properties experience this phenomenon; some of them are robust to system retiming.

    When a system is retimed, it either slows down, or it speeds up. In other work, Colombo, Pace and Schneider have devised a theory of slowdown and speedup, which defines precisely what it means for a property written in Duration Calculus to be robust with respect to system slowdown and speedup [1]. However, this is a dense time theory; a system is regarded as being able to continuously examine its environment and instantaneously respond to it. In practice, especially in the scenario of reactive systems, systems sample their environment at periodic intervals, and use the sampled values to compute their output.

    Synchronous languages, such as Lustre and Signal provide a framework for simplifying the development of such systems. These languages allow the separation of functional and non functional aspects of the system for verification purposes. When developing the system, the programmer assumes a discrete notion of time; At each instant, the system takes its inputs and provides its output. The programmer specifies how the transformation from input to output happens at each instant, whilst ignoring any real-time constraints. At this point, the system can be verified for functional correctness. If this verification yields positive results, one can check whether the system satisfies its real-time constraints. In Lustre, the real-time duration of a cycle is bounded and known at compile time; one only needs to check whether a program cycle can always be completed before the next sample arrives.

    In this project, we attempt to define a theory of slowdown and speedup which operates on the discrete time model and which can thus be applied to programs written in the synchronous paradigm. Building on other relevant work, we are interested in considering appropriate ways of modeling the slowing down of the inputs to a discrete sampled system, and to define what it means for a synchronous system to be well behaved under such a discrete slowdown of its inputs. Once a meaningful definition has been arrived at, we shall also want to consider static and dynamic means of deciding cheaply whether a synchronous program expressed in some particular language is well behaved under slowdown or not.

    References:
    [1] Safe Runtime Verification of Real-Time Properties, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in FORMATS 2009, Budapest, Hungary.

  • Title: Runtime Verification of Distributed Systems Using Migrating Monitors
    Supervisor: Gordon Pace
    Student: Andrew Gauci
    Submitted: 2011
    Download: PDF

    Abstract: As systems become more complex, monolithic architectures are becoming less common, and distributed and component-based systems are becoming more mainstream. Furthermore, with the rise of internet and service-oriented architectures, a monolithic view of certain systems is not only undesirable, but also impossible. At the same time, the increased size of the systems, additional complexity due to their inherent distribution, as well as elevated risks related to security and data exposure, hamper system dependability, making techniques such as runtime verification more attractive.

    Although various approaches have been proposed for the runtime monitoring of distributed systems, many still take a global view of the architecture, typically installing a central monitor which overhears system information and acts accordingly. Although this approach works well for monolithic systems, it typically increases communication overhead, while exposing information on global channels. Moreover, this approach admits elevated security risks by offering a central attack point, in the form of the monitor, through which sensitive information can be tapped. This project investigates the use of migrating monitors, an approach which localises monitoring whereby monitoring code migrates across locations according to where its concerns lie. The aim of this approach is the development of a distributed monitoring framework which preserves information locality, while supporting the verification of systems admitting dynamic configurations (systems whose configurations evolve during execution) as well as supporting properties learnt at runtime.

  • Title: Combing Runtime Verification and Testing Techniques
    Supervisor: Gordon Pace
    Student: Kevin Falzon
    Submitted: 2011
    Download: PDF

    Abstract: The importance of software correctness is becoming increasingly emphasised as the complexity of modern-day system continues to soar. Yet testing alone is insufficient for thoroughly verifying the correctness of these systems. Other verification techniques, notably runtime verification, address certain issues whilst introducing problems of their own. The project aims to investigate the integration of testing and runtime verification, researching the benefits of exchanging information acquired through each technique so as to guide the verification process. The proposed approach involves using properties defined for runtime verification in order to derive test cases which can then be executed independently, providing feedback to the runtime monitor and tuning verification. The various methods by which tuning will be performed will be investigated, possibly resulting in the incorporation of a statistical framework.

  • Title: Embedded Languages for Game Scripting
    Supervisor: Gordon Pace
    Student: Andrew Calleja
    Submitted: 2010

    Abstract: Scripting of artificial intelligence in games is often quite done in a domain-specific language, replicating much of standard programming language features. In this manner, programs which control the AI are fixed sequences of instructions following a set of steps while attempting to mimic human behaviour. We are looking into an alternative approach of using the techniques from the embedded language community to build an embedded domain-specific language for AI scripting for certain games. In this manner, AI scripts become data objects in the programming host language, enabling parametrised strategies, and manipulation of the strategies directly through programs in the host programming language.

    This will enable the creation of adaptive two-stage scripts: (i) fixed strategies in the AI language; and (ii) programs in the host language enabling the modification and adaptation of the scripts in the domain specific language to react to the state of the game. Embedded language techniques give us precisely the power required to create such a scripting language for adaptive AI.

  • Title: Runtime Verification of Refined System Properties
    Supervisor: Gordon Pace
    Student: Ruth Schembri
    Submitted: 2010

    Abstract: Software development lifecycles need to be flexible enough to cater for changes in specifications, whilst also aiming for the fastest possible delivery of software products. Meanwhile, software systems are constantly attempting to offer increasingly more functionality and incorporated fault-tolerance.
    Runtime verification and refinement are two techniques which can be used to verify the correctness of systems. It is possible to monitor the execution of a system to ensure that this conforms to a given specification using runtime verification. Meanwhile, refinement characterises the changes in a specification over successive levels in the development lifecycle, by which it evolves into a concrete design or implementation.
    This project aims to exploit both these techniques in order to create a verification mechanism by which a system can be monitored after release, with the ability to detect system malfunction with respect to specifications from any level of abstraction, and to detect inconsistencies in the specifications. evolution over the development cycle, by identifying execution traces for which a refinement relation between two levels does not hold.

  • Title: Conflict Analysis of Deontic Contracts
    Supervisor: Gordon Pace and Gerardo Schneider
    Student: Stephen Fenech
    Submitted: 2009
    Download: PDF

    Abstract: Industry is currently pushing towards Service-Oriented Architectures, where code execution is not limited to the organisational borders but may be extended beyond. Typically, these sources are not accessible making it impossible to fully trust their execution. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. Composition of different services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this work we start by applying the contract language CL to the CoCoME case study in order to compare with other methods of specification. CL takes a deontic approach to specifying contracts formally. We then present a trace semantics of CL suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into other applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk.

  • Title: Practical Runtime Monitoring with Impact Guarantees of Java Programs with Real-Time Constraints
    Supervisor: Gordon Pace
    Student: Christian Colombo
    Submitted: 2008
    Download: PDF

    Abstract: With the ever growing need of robust and reliable software, formal methods are increasingly being employed. A recurrent problem is the intractability of exhaustively verifying software. Due to its scalability to real-life systems, testing has been used extensively to verify software. However, testing usually lacks coverage. Runtime verification is a compromise whereby the current execution trace is verified during runtime. Thus, it scales well without loss of coverage.

    In this thesis we examine closely the work in runtime verification and identify potential improvements with regards to the specification of properties and guarantees which are given. For the first issue of specification we make use of a real-life case study to better understand the day-to-day properties which system architects would need to formalise. DATE is the logic which results from these experiments and experiences. It is shown to be highly expressive and versatile for real-life scenarios. This is further confirmed by the second case study carried out and presented in this work. Our logic requires a complete architecture to be usable with Java programs. This architecture, called Larva, is developed using Java and AspectJ with the aim of being able to automatically create and instrument monitoring code from a Larva script.

    A central aspect of this thesis is the work on real-time properties. Such properties are very sensitive to overheads, because overheads slow down the system and use up resources. For this purpose, we present a theory based on the prominent real-time logic, duration calculus, to be able to give guarantees on the effects of slowing down/speeding up the target system due to the monitoring overhead. Another form of guarantee which we can give on real-time properties is the upperbound of memory overhead used during runtime verification. This is achieved by starting from the subset of duration calculus, QDDC, and translating it into Lustre.

    To relate Larva to other tools in the field we use a benchmark to compare expressivity and resource consumption of Larva to other prominent tools. Furthermore, a subset of duration calculus (counterexample traces), QDDC, and Lustre have been shown to be translatable into Larva. This has two main purposes: first that this allows users familiar with other logics to utilise Larva, and second that the guarantees enjoyed by these logics, will also benefit Larva.

  • Title: Runtime Monitoring of Duration Calculus Assertions for Real-Time Applications
    Supervisor: Gordon Pace
    Student: Karlston D'Emanuele
    Submitted: 2007
    Download: PDF

    Abstract: An open question which is commonly asked in software development is whether the implemented artefact follows the requirements specified. From the early days of computing, a number of projects, ideas and techniques have been proposed to prove software correctness. One of these techniques is validation, which verifies the system during execution.

    Duration Calculus is a powerful logic notation that evaluates property satisfaction by applying the Reimann integral over property values within an interval. Therefore, Duration Calculus not only determines whether a property is being satisfied but also the duration of the property satisfiability. Duration Calculus notation considers time as a real valued variable, which together with the evaluation of calculi formulae becomes undecidable. In this dissertation, we restrict the notation to a subset that is decidable, discrete-time and deterministic. The decidability property is important in order to evaluate the system correctness at runtime. On the other hand, the restriction to discrete-time together with the determinism of the notation reduce the side-effects of the inserting observers in the actual system thus guaranteeing the correctness of the verified program.

    After restricting Duration Calculus notation to the suitable subset of operators, we propose a framework for defining monitors and integrating them with the system code. Our framework allows monitors to be defined using the mathematical notation, which through a pre-compiler is converted to its Lustre semantics and stored inside Abstract Syntax Trees. The synchronous data-flow programming language Lustre is used for the notation semantics because the resource requirements for the monitors can be predetermined. To keep the benefits obtained by using Lustre, the monitoring platform is also defined in Lustre. The final step before executing the system is to integrate the monitors inside the code. The weaving of monitors with the system is performed through the concept of annotated assertions, which are converted into function calls to the Lustre based evaluation engine to determine the properties satisfiability.

    We conclude our research by showing the concept of Interval Temporal Logic validation as an aspect, within the Aspect-Oriented Programming (AOP) framework. This concept can be used to facilitate the design of more robust and flexible validation engine simply by defining notation semantics.

  • Title: An Embedded Language for the Definition and Refinement of Synchronous Circuits
    Supervisor: Gordon Pace
    Student: Christine Vella
    Submitted: 2006
    Download: PDF

    Abstract: 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 a 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-22 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 behaviour. 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.