The group has a long history of funded projects. We describe some of the recent work below.
2020 - 2024: Effective and efficient operation, management and monitoring of large-scale networks (Parisis co-PI)
funded by Moogsoft
This project is in collaboration with Prof Berthouze and will fund PhD studentships in the broader research areas of large-scale network management, monitoring and operation. These include the design of machine learning and data science approaches for identifying and preventing network and service outages, and the development of machine-learned network protocols.
2019 - 2021: Reinforcement learning in next generation data transport mechanisms (Parisis PI)
funded by Amazon
This project is about the development of computer-generated, machine-learned congestion and flow control algorithms for next-generation computer network systems. The focus is on Reinforcement Learning using Actor-Critic approaches with deep neural networks. Amazon funded this project through the provision of AWS services, including CPU and GPU resources.
2019 - 2021: Efficient and scalable computation of metrics for logical and physical IT infrastructure networks (Parisis co-PI)
funded by InnovateUK KTP and Moogsoft
This project was in collaboration with Prof Berthouze and aims at the design and implementation of distributed algorithms for computing graph metrics and context-specific approximations for large scale computer networks.
Research Development Fund - Design and implementation of a simulation framework for experimenting with data transport mechanisms in simulated data centre network topologies (Parisis PI)
Data centres are the home of cloud computing, consisting of large warehouses filled with racks of commodity servers, interconnected by multiple, high bandwidth networking links providing very high aggregate bandwidth. The Transport Control Protocol (TCP) is the protocol that reliably connects computing endpoints together, but by design it will only allow connections to follow a single path. Extensions to the design of TCP and alternative protocols to exploit the high aggregate bandwidth from the high-density connectivity within data centres are emerging from current research but comparisons between proposals are difficult to make because of the lack of a common simulation framework. We propose to build extensions to the most commonly used network simulator, ns-3, to make creating realistic data centre topologies viable, and to allow comparisons between different data transport protocol variants. This work builds on our existing work in extending the ns-3 simulator to support multi-path TCP, aiming at supporting a viable platform for research on network protocols for improving data centres.
2012 - 2013: Digital Stadium (Wakeman PI)
funded by EPSRC
The Digital Stadium project was a collaborative research project funded by the EPSRC (EP/K012762/1) between the University of Sussex, Brighton and Hove Albion Football Club, and Corridor Design, looking at how modern smartphone apps can be used to build new ways of communicating within stadiums. It now continues as a collaboration the university, TribeHive Ltd and BHAFC.
Major sports events are ideal opportunities to exploit pervasive computing technologies to increase the quality of experience. As the penetration of smartphones continues, they can become the hub of the customer’s experience, linked to their ticket, their seat, their favourite food offerings, their modes of transport, and most importantly, to the sporting event on show. But there are many challenges to connecting everything inside the stadium. The numbers and density of people and likely interaction patterns make it difficult to provide adequate bandwidth with larger range networks, which when combined with the concrete and steel construction of the stadium make network provision a serious technical challenge.
This project is investigating pocket switched networking technologies to provide an infra-structure upon which useful services can be deployed.
2008 - 2012: Crowfoot: From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs (Reus PI)
funded by EPSRC
Pointers are an important feature of programming languages used to define dynamically growing and recursive data structures. Many languages provide pointers not just to data but also functions or procedures, i.e. to executable code. Thus, code pointers offer high flexibility of code reconfiguration at runtime. Yet, their treatment in specification and verification has been poor due to their complexity. In order to write correct software in state-of-the-art languages it is paramount to have logics that permit reasoning about programs including function pointers. It is important that reasoning about heaps is local and modular which means that verification can be simply done w.r.t. the part of the heap affected by code, and independently of other code modules linked at a later stage, respectively. Separation Logic has presented us with a handle to tackle the complexity of pointers. It permits local reasoning on the heap, liberating the verifier from specifying and proving that most of the heap does not change when a procedure or command is executed. The central objective of this project is to establish program (Hoare-) logics for languages with explicit and implicit code pointers making the benefits of Separation Logic amenable to them.
2011: Relative Completeness for Logics of Functional Programs (Reus PI)
funded by EPSRC
Program logics play an important role in Computer Science to complement testing. A program logic allows one to prove that a program satisfies a given specification. Seminal work has been done in the early seventies by Hoare on axiomatic semantics for stateful programs. Since then many calculi have been developed for all kinds of programming languages and meanwhile mechanizations of these logics in numerous verification tools exist. Two properties of a program logic are of particular interest: Soundness states that any property one can prove of a program in the calculus is actually valid. Completeness states the converse, namely that any valid property can also be derived. In an ideal world, a formal calculus for a program logic would be both, sound and complete, thus faithfully and completely reflecting the semantics of programs and correctness assertions, also called specifications. However, due to Goedel's Incompleteness Theorem it is hopeless to look for (absolutely) complete program logics since for any formal system S there always exists a correctness assertion which is true but cannot be proved in S.In spite of this, one might ask whether the axioms of some program logic are sufficient to derive all true correctness assertions relative to some complete theory of data as e.g. all true sentences of first order arithmetic. This was first investigated for simple imperative languages where specifications are so-called Hoare triples, of the form {P}C{Q} where C is a program, P the pre-condition, and Q the post-condition. Such a triple states that if C is run in a state fulfilling P and terminates, the resulting new state will meet assertion Q. The Hoare-calculus then provides a set of rules and axioms how one can derive such triples, ie. proofs that programs meet a certain specification given by pre- and post-conditions. The property of relative completeness for such a logic was established by Cook in his seminal paper for a simple variant of Hoare logic. He showed that all correct partial correctness assertions of the form {P}C{Q} can be derived using the rules of Hoare's logic provided we are allowed to use all true sentences of first order arithmetic as axioms. The reason for this is that the language of first order arithmetic is strong enough to express for all programs P its input/output relation by a formula of first order arithmetic.Program logics, however, are also of interest for functional programs. Popular functional programming languages are ML, Caml, or Haskell. Pure functional languages do not use state but recursively defined data structures and higher-order functions on them. To the best of our knowledge the question whether relative completeness holds for logics of functional programming languages has not been investigated systematically and thoroughly. Therefore, this project will investigate logics such as D. Scott's LCF (or extensions of it). Experience tells us that verification of most purely functional programs can be expressed within LCF. But it is also easy to find assertions which can neither be proved nor disproved within LCF, like the specification of 'parallel or'. The reason simply is that the former holds in the Scott model but its negation holds in the fully abstract model. It is important to note that these two models are not different w.r.t. the data type NAT of natural numbers (and also the data type NAT->NAT of unary functions on NAT) but they do differ at higher types. Accordingly, it does not make sense to ask whether LCF is relatively complete w.r.t. to a full axiomatization of its first order part since the latter -- unlike for a basic imperative language -- does not fully determine the (higher type part of the) model.Thus, the right question, the one we will tackle in this project, is whether 'natural' models for PCF can have nice complete axiomatisations.
2008 - 2012 Shyness (Wakeman co-I)
funded by EPSRC
An EPSRC funded research project on the WINES programme, undertaken by the departments of Informatics and Sociology at the University of Sussex. Grant reference number EP/F064330/1.
Pervasive computing gives rise to new forms of interaction which make users feel shy: concerned about how they are perceived when performing in social interaction, and about what data are being collected about them in the process. This project focuses on exploring an awareness of the situations which give rise to these feelings; how presentation and feedback through the available technology can be mediated to manage these issues; and how users can manage the connection between situation and mediation. The project is formed from three parallel threads of study using classrooms, social and situated groups, and public artworks as their focus. In each case the study will be inter-disciplinary, combining the approaches and skills of three groups at Sussex: sociologists, interaction (HCI/CSCW/social software) and software systems.
Summary of Outcomes
The project planned to look at a number of contexts of use: classrooms, social and situated group communications, and public interactive art installations. As the project developed the latter two became the focus and several studies were run in each of these areas, which together reflect the objectives of the project. In the educational context a study was run in programming classes, where a variety of backgrounds can lead to potential embarrassment as competences evolve. We deployed an application for signaling emotional state, building on the “subtle stones” work and a paper discussing the outcomes is currently under review. In the social and situated group communications context we studied the use of wearables, commentary web sites, paired tasks, use of the Twitter and MySpace? social networks and farmers’ markets. Simulated communications technology was also used. In the art galleries context studies were undertaken at Chameleon, an interactive art exhibition at Fabrica, a small contemporary art gallery in Brighton; the Decode: Digital Design Sensations exhibition at the much larger and more traditional Victoria and Albert museum in London; and Like shadows: A celebration of shyness, at the Phoenix art gallery, as part of the White night festival 2011. The latter event was organised in collaboration with the project, and included art work designed to explore the feelings and triggers – acting as both a platform for a sociology study, a deployment for a discussion system we developed which studied controls for the mediation of identity in public spaces and also as a public engagement exercise with an estimated 4500 visitors. Returning to our objectives, we have succeeded in making publishable advances in each, with some research and publication preparation and review ongoing at this time.
Understand performance anxiety and shyness arising from … pervasive computing. Our findings highlighted a common theme in the experience of shyness: the fear about ‘not knowing the rules’ of a social situation and of ‘getting it wrong’. This aspect was focused around galleries. Many people felt shy about being asked to ‘play’ with technology or ‘perform’ in some unspecified way when engaging with interactive artworks, especially when other people might be watching. Some people preferred to wait and watch others before having a go, to make sure that they got it ‘right’. This conflicted with the ideas of interactive artists and curators, who said that there were no secret rules or intended messages, nor any ‘right’ way of doing it: their optimistic model of ‘visitor self-discovery’ encouraged visitors to explore freely and make their own interpretations. We therefore argued that this model was unrealistic insofar as it was not grounded in the lived experiences and situated practices of ordinary gallery and museum-goers. Artists, curators and gallery staff stand to gain a great deal from listening to such views from their visiting public, and by continuing to encourage community engagement in the arts. We also encourage these art providers to be more aware of shy visitors’ concerns, and to design exhibits that are more ‘shy-friendly’.
Identify factors which give rise to shyness in using pervasive computing, and develop appropriate models of these contexts. Studies in the classroom and gallery lead to simple models of the current situation, but the triggers for shyness are quite personal and to a large extent this objective became part of a model of detection – either through explicit signalling, physical detection or inference from settings arising as discussed below.
Develop models and implementations that manage personal and contextual data to give users greater control over presentation and interaction. We undertook a number of studies on the wider topic of choice in degree of exposure through pervasive computing, including: The design and simulation of a system for supporting plausibly deniable question asking and answering over networks with churn, which our work showed to be an effective means of communication. An infrastructure to support authentication of devices through physical demonstration, which allowed users to specify the modes of demonstration that they were comfortable with – some involving performance which might not be conducive to comfortable social interactions. We studied users of the MySpace? and Twitter social networks and developed models of “fitting in” to a social group for MySpace? and conversational use and use of links to other media in Twitter. In Twitter we found a range of classifications of behaviour, reflecting different temporal patterns of engagement and different approaches to maintaining relationships. We also developed a system called “ShineUS”, for commenting on exhibitions. This interfaced to Facebook, Twitter, web display (including on handhelds) and projections in the exhibition. This system was deployed at the White Night event and at PerCom? 2012. Users are able to control which modes of display they wished their comments to appear on and when, allowing them to configure their social exposure to comment-making. Results are still being analysed, but initial findings are that with randomised starting profiles users do change to a variety of settings reflecting both the piece they are commenting on and personal preference.
Develop interface models that facilitate interaction, self-presentation and social presence, to control the effects of shyness. There were two groups of studies: those which sought to project affective state and those which sought to facilitate interaction. For facilitating interaction, with control over anonymity to different groups of users we extended prior work on trust in farmers markets and then used this experience and that of a number of interns’ projects to develop the ShineUS system described above. These studies both modelled relations and controls but also had interfaces which facilitated their use in real world public settings with controls over presentation. Understanding affective state was one of the most challenging possibilities of the project and a number of different studies were run. We deployed a wearable computing jacket, with sensors that enabled discrete signalling of what was felt. Prior work on subtle stones was extended with positive response to the control of presentation afforded in a variety of settings An application was deployed in a classroom setting to enable students to discretely signal their feelings. A galvanic skin response and skin temperature sensing wrist band was built, and used in both a controlled study and one of the art works at White Night. Results from the study are still being analysed, but discrete sensing of state could form an important part of automatic adaptation. A study of synchrony in paired activities with an ambient display was undertaken, which found that even very subtle displays disturbed the rapport of the participants.
Consider ethical implications of manipulating the presentation of self and of employing this as an incentive to use pervasive computing. Ethics was addressed in our paper 'The reluctant researcher', which was about power relations, interaction dynamics and ethical implications of being a shy person oneself and researching 'shy' people; and also in the Artists and Curators workshop which we organised, which was about the ethical question of whether 'shy' visitors should be encouraged/forced to actively engage with technology in exhibitions.
Finally, our dissemination plans included a wider impact than the academic community, which has been achieved. BBC News online carried an article about the project. The White Night event has been discussed above. Four undergraduate interns were employed on developing prototypes and have taken this experience into industry or been motivated to undertake doctoral studies. A workshop for interactive artists and curators was held at Sussex. The Sociology team also collaborated on the Viewfinder project with partners from the Lighthouse digital culture agency and Aldridge Academy Community Secondary school, Brighton, and local artist Marianne Holm Hansen, which gave year 11 BTec art students the opportunity to plan and present their own digital art exhibition.