Computing at Leicester

Software Modelling and Evolution (SOME)

We use mainstream modelling languages and methods UML or BPMN and mathematical models such as automata, term and graph rewriting, process calculi, logics and semantic web languages and use their theory, techniques and tools, as well as transformations and mappings between them, to address software engineering problems.

Learn more about SOME on our research pages.

Suggested topics

Abstractions for mobile distributed systems:

Supervisor: Emilio Tuosto

The widespread use of distributed and concurrent systems urges to use formal models to rigorously describe and analyse computations where remotely executing processes interact through among communication infrastructures that can dynamically change. I'm interested in studying models for several aspects of modern distributed computations from theoretical as well as applied points of view. 

My favourite models are based on process algebras, automata, and hypergraphs.

1) Process Algebras: 

Process algebras are particularly suitable for formally describing and reasoning on distributed communicating processes that operates in a dynamically changing environment. Indeed, many different theories (e.g., behavioural type systems) have been shown adequate to tackle modelling and verification problems rising in distributed computing (e.g., distributed coordination, behavioural types, model- or type-checking).

I have been working on calculi featuring event-notification primitives and, more recently, I am interested in applying process algebras to study choreography-based, contracts, and behavioural types of distributed applications.

Required skills 

Good mathematical and logical skills. If interested in implementation aspects, good programming skills (either functional or object oriented programming).

References

  • Robin Milner, Joachim Parrow, David Walker. A Calculus of Mobile Processes Part I and Part II. Information and Computation 100:1-77 (1992).
  • Emilio Tuosto: Contract-Oriented Services. WS-FM 2012: 16-29
  • Laura Bocchi, Hernán C. Melgratti, Emilio Tuosto: Resolving Non-determinism in Choreographies. ESOP 2014: 493-512
  • Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino: Honesty by Typing. FMOODS/FORTE 2013: 305-320
  • Julien Lange, Emilio Tuosto: Synthesising Choreographies from Local Session Types. CONCUR 2012: 225-239
  • Roberto Bruni, Ivan Lanese, Hernan Melgratti, Emilio Tuosto. Multiparty sessions in SOC. In D. Lea and G. Zavattaro editors. Coordination Models and Languages, volume 5052 of Lecture Notes in Computer Science, Springer-Verlag, May 2008.
  • GianLuigi Ferrari, Daniele Strollo, Roberto Guanciale, and Emilio Tuosto. Coordination Via Types in an Event-Based Framework. In J. Derrick and J. Vain, editors, 27th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems Special focus on service oriented computing and architectures, volume 4574 of Lecture Notes in Computer Science. Springer-Verlag, June 2007.

2) Automata for mobile and distributed applications 

Automata are foundamental tools in theoretical computer science as well as in more applied aspects of our discipline. In my research I use automata models to study choregraphy-based design theories as well as nominal automata models. The latter enrich traditional automata to capture computational phenomena arising in mobile applications. Not only automata can be used to check behavioural equivalences of systems, but they are also suitable to design and verify e.g., service compatibility.

Required skills

Good mathematical and logical skills. Notions of automata theory.

References

  • Robin Milner, Joachim Parrow, David Walker. A Calculus of Mobile Processes - Part I and Part II. Information and Computation 100:1-77 (1992).
  • Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto: On Nominal Regular Languages with Binders. FoSSaCS 2012: 255-269
  • Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto: A Characterisation of Languages on Infinite Alphabets with Nominal Regular Expressions. IFIP TCS 2012: 193-208
  • J. Lange, E. Tuosto, N. Yoshida: From Communicating Machines to Graphical Choreographies. POPL 2015
  • G. Ferrari, U. Montanari, E. Tuosto. Coalgebraic Minimisation of HD-Automata for the pi-calculus Using Polymorphic Types. TCS 331:325-365 (2005).
  • V. Ciancia, G. Ferrari, M. Pistore, E. Tuosto. History Dependent Automata for Service Compatibility. In P. Degano, R. De Nicola, and J. Meseguer editors. Concurrency, Graphs and Models, volume 5065 of Lecture Notes in Computer Science, Springer-Verlag, July 2008.

3) Graphs model

Graph and graph transformation can be envisaged as a generalisation of terms and term rewriting. In last years, graphs have been widely used to model concurrent and distributed systems and nowadays many tools rely on such theories. I'm interested in the use of a recent techniques for rewriting hypergraphs, a class of graphs where edges can connect more than 2 nodes. An interesting line of research is the implementation of the rewriting techniques defined for hypergraphs.

Required skills 

Good programming skills (preferably functional programming). Some mathematical and logical skills.

References

  • Kyriakos Poyias, Emilio Tuosto: On Recovering from Run-time Misbehaviour in ADR. ICE 2013: 68-84
  • Kyriakos Poyias, Emilio Tuosto: Enforcing Architectural Styles in Presence of Unexpected Distributed Reconfigurations. ICE 2012: 67-82
  • Gianluigi Ferrari and Dan Hirsch and Ivan Lanese and Ugo Montanari and Emilio Tuosto. Synchronised Hyperedge Replacement as a Model for Service Oriented Computing. F. de Boer, M. M. Bonsangue, S. Graf and W. P. de Roever editors. Formal Methods for Components and Objects: 4th International Symposium, FMCO, volume 4111 of Lecture Notes in Computer Science, Springer-Verlag, November 2005.

  • See Emilio Tuosto's homepage and contact details.

Access control matrices 

Supervisor: Tom Ridge

Access control matrices (related to access control lists) are used to specify who has access to what resources. For example, the following states that user tom has access to all files, whereas jen has access only to File A. 

   |File A|File B|File C
tom|  Y   |  Y   |  Y   
jen|  Y   |  N   |  N

Access control matrices are easy to implement. Unfortunately they are very difficult to manage, because high-level access control rules (e.g. only users with the role of administrator should be able to access all files) are not explicitly captured. Much existing research has been directed at this problem, but it should be possible to do something new and interesting by expressing the high-level rules in higher-order logic, then using automated provers to check that the properties are enforced. 

Analyses for Understanding Embedded Software Evolution

Supervisor: Jan Oliver Ringert

Embedded software typically executes within a larger system of software and hardware components. Examples of embedded software are found in the avionics, automotive, and robotics domain. These domains are leading adopters of model-based software development where systems are described, analysed, and simulated using software models.

Software models constantly evolve as new requirements are added and bugs are fixed. Efficient means for understanding evolution are paramount for effective change management and maintenance. However, there are still many open questions for the successful application evolution analyses in practice. On the one hand, this project will extend underlying theories to support important concerns of embedded software development, including support for different operation modes and software variants. On the other hand, the project will analyse typical modelling activities and evolution steps of embedded software models. These will be supported with suitable algorithms and means for interaction with engineers to support the analysis and understanding of software model evolution.

Feature-oriented Modelling, Analysis and Simulation

Supervisor: Reiko Heckel

Feature models allow to define variants of systems or products.  The same approach is useful in models of social or software systems if we want to reuse more general models by specialising them to specific requirements, e.g., in order to compare versions with or without certain features. This use of feature modelling for model management raises questions for analysis techniques, which are currently not modular enough to support a feature-oriented approach.

We will look at graph transformation models and their analysis though differential equations or simulation, with applications to social sciences, biology, health or software engineering.

Skills Required

Strong background in at least two out of the following three areas is required:

  • OO development (programming and design).
  • theoretical computer science (automata and formal languages, propositional and first order logic, basic set theory).
  • maths (specifically analysis and probability theory).

  • See Reiko Heckel's homepage and contact details.

Graph Transformation Games

  • for Social Networks
  • for Autonomous Software Agents

Supervisor: Reiko Heckel

The idea is to apply game-theoretic concepts to networks with dynamic topology. For example, in the case of social networks, the network topology may change by individuals joining or leaving, connecting or breaking up. Networks of autonomous software agents can show similar behaviour.

In both cases it is interesting to understand how local actions of individuals or agents trying to maximise their own goals lead to global outcomes, or vice versa, how incentives for individuals need to be defined in order for desirable global outcomes to become possible.

A network can be seen as a graph, and its evolution over time modelled by graph transformation rules. See https://www.cs.le.ac.uk/people/rh122/papers/2006/Hec06Nutshell.pdf for an introduction to graph transformation and google 'social network analysis' to get an idea of the problem.

We have made first steps combining graph transformation with game theory in this contribution focusing on negotiation of features for services slides.

Model Inference

  • for Social Networks
  • for Web, Cloud or Mobile Services

Supervisor: Reiko Heckel

Reverse engineering of models from existing systems helps understanding, analyses and redesign. For example, we have already developed techniques to derive visual contracts (a diagrammatic modelling language based on graph transformation) from existing services or components in Java and we are currently looking into reverse engineering the behaviour of Twitter bots.

Similar questions can be asked of a number of platforms, technologies and applications, such as semantic web, cloud technologies, or machine learning applications.

The following references give an idea of our existing work in this area:

Modelling of reversibility of complex systems

Supervisor: Irek Ulidowski

Most simple bio-chemical reactions are in principle reversible, so one might think that such reactions typically fluctuate, going forwards and backwards between a number of states. However, nature is synonymous with change or progress. In nature, reversibility is used in a number of important mechanisms such as, for example, signal passing, recycling of molecular resources and stimulating reactions by catalisys. 

This project aims at studying the role that reversibility plays in major families of bio-chemical reactions and, more generally, in the behaviour of complex systems, including artificial systems such as distributed or quantum systems, and robotics, with the view to model them formally at an appropriate level of abstraction. It is fairly well known how to model the so-called causal reversibility: we can use process calculi, event structures or modal logics (see publications below).

 There are, however, more general forms of reversibility, the so-called out-of-causal-order reversibility, that are very crutial in nature as well as in artificial system. But we do not know how to model them appropriately yet. We are currently experimenting with a variety of formal models, including process calculi where processes can change their structure.

References

  • Iain Phillips, Irek Ulidowski and Shoji Yuen, A reversible process calculus and the modelling of the ERK signalling pathway. Proceedings, Reversible Computation 2012, LNCS, volume 7581, pp. 218-232.
  • Iain Phillips and Irek Ulidowski, Reversibility and asymmetric conflict in event structures. Proceedings of CONCUR 2013, LNCS, volume 8052, pp. 303-318. Springer, 2013. doi:10.1007/978-3-642-40184-8_22
  • Iain Phillips and Irek Ulidowski, An Event Identifier Logic. Mathematical Structures in Computer Science. doi:10.1017/S0960129513000510
  • Irek Ulidowski, Iain Phillips and Shoji Yuen, Concurrency and reversibility. Proceedings, Reversible Computation 2014, LNCS 8507, pp. 1-14. Springer 2014.

  • View Irek Ulidowski's webpage and contact details

Filesystem implementation

Supervisor: Tom Ridge

The project is to develop a C implementation of a filesystem I have implemented in OCaml. The OCaml version is verified correct. Ideally the C implementation would have some direct (formal, mathematical) connection to the OCaml version, so that the C version would also be correct (there are several ways to make this more precise).

OCaml to C compilation 

Supervisor: Tom Ridge

The project is to define how to translate OCaml (more likely, a simple functional programming language such as MiniML) to C. This would provide a general way to achieve the results of the "filesystem implementation" project above. The L4.verified project, to develop a verified operating system, did something similar, and it should be possible to use this existing work.

OCaml to Scheme compilation 

Supervisor: Tom Ridge

The project is to define how to translate OCaml (more likely, a simple functional programming language such as MiniML) to Scheme, similar to the OCaml to C compilation project above. Scheme is available pretty much everywhere, but implementations of ML-like languages are not so readily available. When new technologies such as Java (or .NET) come along, you want to be able to use all the new features and technology, combined with everything you love about ML. Scheme is usually supported very quickly e.g. from within Java via JScheme or Kawa, but it is still difficult to use ML-like languages with Java. This project aims to develop an ML to Scheme translator, allowing ML programmers to take advantage of existing Scheme/Java technology to run their ML code on the Java platform.

Reasoning above operational semantics 

Supervisor: Tom Ridge

One way to prove programs correct is to reason directly about their operational behaviour, as defined by the operational semantics for the language. There are many things that need to be done here, such as developing good operational semantics to support high-level reasoning; developing tools to make symbolic evaluation quicker; developing reasoning techniques for operational reasoning; porting existing techniques to the operational setting etc

Verified computational complexity 

Supervisor: Tom Ridge

Lots of effort has been dedicated to reasoning formally about program correctness. We would now like to prove that implemented code has time and space complexity that it is claimed to have. A simple approach would be to define the atomic steps of a language, and count the number of steps a piece of code takes. However, informal reasoning tends to be at a much higher level than this. The aim of this project is to start developing the formal verification of computational complexity by looking at simple functional implementations e.g. of mergesort etc. Some recent work by Bob Harper et al. is relevant, here.

Back to top
MENU