-
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.
|
|