STRATA; Layers for Structuring Trustworthy Ambient Systems
Lead Research Organisation:
Newcastle University
Department Name: Sch of Computing
Abstract
For computing as a whole, and ambient systems in particular, significant new challenges will have to be faced because of the rapid evolution in Cyber-Physical Systems (CPS). A major impetus towards CPS is the promised Internet of Things (IoT). The scale of the IoT could soon involve trillions of devices generating masses of real-time data and thus demanding unprecedented power. To sustain this scaling and huge surge in energy demand, ambient systems will need to be designed to trade off power, performance and reliability. Inevitably, this will require ever more sophisticated responses to achieve trustworthiness.
Our TrAmS-2 platform was shaped by two important factors affecting ambient system design. First, the power provision/consumption of devices, rather than cost, was becoming the limiting factor in the deployment of ambient systems. Second, novel paradigms such as cloud computing offered a new dimension of ambience in that data and programs can be migrated without physical movement of agents.
The TrAmS-2 platform grant has sustained our research group which has created new projects on sound technical foundations, methods and tools to model, design and analyse Trustworthy Ambient Systems. Our team, and the projects in which it is involved, are developing methods for designing mobile devices with energy-efficient and power-constrained hardware. Our project portfolio includes 13 EPSRC, EU, industry and other projects with applications in sectors including automotive, rail, space, business, healthcare and consumer electronics. Our current arsenal of tools and methods includes the powerful toolsets of Rodin, Workcraft and Symphony, advanced patterns for modelling fault tolerance and world-leading techniques in proof technology, simulation and ample evidence to support industrial deployment of formal engineering methods. With such a solid foundation we will enter Strata well equipped with formal engineering methods, advanced tool support, architectural and algorithmic approaches for embedded systems design and modelling, in particular capturing systems with multiple modes targeted at power and reliability.
In Strata, the research platform will receive extra impetus through a two-pronged attack on the challenges of future ambient systems design with the teams in Newcastle and York working together. This will facilitate making a qualitative step in terms of rigorous and model-based approaches to the design and analysis of future resource-limited ambient systems. The cornerstone of the platform approach and methodology is a shared vision that future complex ambient systems have to be structured in layers. These layers, or strata, of system resources and delivered functionality in terms of time and power will be combined with cross-layer fault tolerance and even adherence to the (levels of) specification in an environment where one has to accept that components will fail. Strata will address the challenges in four interlinked themes: methodology, cross-layer fault tolerance, real-time layering and real power.
The skills of the three involved research groups are complementary and form a solid research base in software, systems and microelectronics to establish a unique team in terms of capability and expertise, with international profiles in formal methods, dependability, real-time and energy-modulated systems. Strata will provide continuity for research staff, encouraging new, risky, research in areas created by this novel mix of expertise.
Our TrAmS-2 platform was shaped by two important factors affecting ambient system design. First, the power provision/consumption of devices, rather than cost, was becoming the limiting factor in the deployment of ambient systems. Second, novel paradigms such as cloud computing offered a new dimension of ambience in that data and programs can be migrated without physical movement of agents.
The TrAmS-2 platform grant has sustained our research group which has created new projects on sound technical foundations, methods and tools to model, design and analyse Trustworthy Ambient Systems. Our team, and the projects in which it is involved, are developing methods for designing mobile devices with energy-efficient and power-constrained hardware. Our project portfolio includes 13 EPSRC, EU, industry and other projects with applications in sectors including automotive, rail, space, business, healthcare and consumer electronics. Our current arsenal of tools and methods includes the powerful toolsets of Rodin, Workcraft and Symphony, advanced patterns for modelling fault tolerance and world-leading techniques in proof technology, simulation and ample evidence to support industrial deployment of formal engineering methods. With such a solid foundation we will enter Strata well equipped with formal engineering methods, advanced tool support, architectural and algorithmic approaches for embedded systems design and modelling, in particular capturing systems with multiple modes targeted at power and reliability.
In Strata, the research platform will receive extra impetus through a two-pronged attack on the challenges of future ambient systems design with the teams in Newcastle and York working together. This will facilitate making a qualitative step in terms of rigorous and model-based approaches to the design and analysis of future resource-limited ambient systems. The cornerstone of the platform approach and methodology is a shared vision that future complex ambient systems have to be structured in layers. These layers, or strata, of system resources and delivered functionality in terms of time and power will be combined with cross-layer fault tolerance and even adherence to the (levels of) specification in an environment where one has to accept that components will fail. Strata will address the challenges in four interlinked themes: methodology, cross-layer fault tolerance, real-time layering and real power.
The skills of the three involved research groups are complementary and form a solid research base in software, systems and microelectronics to establish a unique team in terms of capability and expertise, with international profiles in formal methods, dependability, real-time and energy-modulated systems. Strata will provide continuity for research staff, encouraging new, risky, research in areas created by this novel mix of expertise.
Planned Impact
Strata's way of generating impact, both economic and societal, fits with our scientific approach in that it can be understood as bands of impact activity. One band relates to the existence of the platform grant itself and the work that will be carried out within it: we will have an impact on the people involved in it, on the academic community and on the wider society. The other band of impact will come from Strata offspring projects because of the new avenues of research that will be explored in structuring methods for complex ambient systems with limited resources.
Within the first band, we envisage producing strong societal and economic impact of our research through the effect of the new methodology on the practices of developing complex fault-tolerant mixed-criticality systems with limited resources through the radically new concepts of layers in systems structuring.
The extension of TrAmS-2 into real-time and layered ambience offers great potential for impact in broad areas of industry and society. Beneficiaries include businesses providing infrastructure, devices and services for ambient systems, and end users for whom major concerns are the security, safety and quality of experience provided by the system as a whole.
Several groups have a stake in ensuring fault-tolerance and resilience of ambient systems. Economic beneficiaries include companies and sectors that develop software and services for such systems, for whom the cost of development, modification and upgrading directly depends on the complexity of the systems. The disciplined application of the cross-layer fault tolerance will allow them to reduce the cost of development and make their products more competitive.
The entire ICT sector is being strongly influenced by societal and economic demands for systems to be green, energy-frugal and power-proportional. Through the promotion of better understanding of the holistic nature of system design issues, Strata will promote methods and tools for rigorous development through the interplay of power and timing constraints. This vision will be passed to existing and new SMEs and R&D organisations, particularly in the embedded systems sector, where the drive for smart-energy utilisation is increasing.
In the second band we will ensure that Strata enables the impact of the new projects that result from the platform grant. Our approach is therefore to ensure that the Strata group interacts with potential beneficiaries of these "offspring projects", and takes account of their needs when formulating research strategy and developing project proposals.
A major impact route is through developing tools supporting the well-founded modelling and analysis methods for dependable ambient systems that Strata offspring projects will generate. We will build on our extensive experience at developing usable tools that have achieved industry deployment. To overcome the difficulty of accessing formal methods tools, we will set up the infrastructure to allow new and existing tools to be wrapped with standardised service-based interoperable interfaces. This approach is intended to increase, by orders of magnitude, the number and range of organisations that can then benefit from these tools. In particular it will allow SMEs to benefit from tooling that has hitherto been limited to large organisations with expertise and computing power.
All the investigators have established records of creating impact from their research both from the previous TrAmS-2 Platform Grant and other extensive research careers. Much of the existing evidence is of solid industrial impact via projects that benefited from the previous tranche of TrAmS-2 funding.
Within the first band, we envisage producing strong societal and economic impact of our research through the effect of the new methodology on the practices of developing complex fault-tolerant mixed-criticality systems with limited resources through the radically new concepts of layers in systems structuring.
The extension of TrAmS-2 into real-time and layered ambience offers great potential for impact in broad areas of industry and society. Beneficiaries include businesses providing infrastructure, devices and services for ambient systems, and end users for whom major concerns are the security, safety and quality of experience provided by the system as a whole.
Several groups have a stake in ensuring fault-tolerance and resilience of ambient systems. Economic beneficiaries include companies and sectors that develop software and services for such systems, for whom the cost of development, modification and upgrading directly depends on the complexity of the systems. The disciplined application of the cross-layer fault tolerance will allow them to reduce the cost of development and make their products more competitive.
The entire ICT sector is being strongly influenced by societal and economic demands for systems to be green, energy-frugal and power-proportional. Through the promotion of better understanding of the holistic nature of system design issues, Strata will promote methods and tools for rigorous development through the interplay of power and timing constraints. This vision will be passed to existing and new SMEs and R&D organisations, particularly in the embedded systems sector, where the drive for smart-energy utilisation is increasing.
In the second band we will ensure that Strata enables the impact of the new projects that result from the platform grant. Our approach is therefore to ensure that the Strata group interacts with potential beneficiaries of these "offspring projects", and takes account of their needs when formulating research strategy and developing project proposals.
A major impact route is through developing tools supporting the well-founded modelling and analysis methods for dependable ambient systems that Strata offspring projects will generate. We will build on our extensive experience at developing usable tools that have achieved industry deployment. To overcome the difficulty of accessing formal methods tools, we will set up the infrastructure to allow new and existing tools to be wrapped with standardised service-based interoperable interfaces. This approach is intended to increase, by orders of magnitude, the number and range of organisations that can then benefit from these tools. In particular it will allow SMEs to benefit from tooling that has hitherto been limited to large organisations with expertise and computing power.
All the investigators have established records of creating impact from their research both from the previous TrAmS-2 Platform Grant and other extensive research careers. Much of the existing evidence is of solid industrial impact via projects that benefited from the previous tranche of TrAmS-2 funding.
Organisations
- Newcastle University (Lead Research Organisation)
- Vilnius University (Collaboration)
- ClearSy (Collaboration)
- SYSTRA Scott Lister (Collaboration)
- The Formal Route (Collaboration)
- Dialog Semiconductor (Collaboration)
- ScubaTx Limited (Collaboration)
- Australian Government (Collaboration)
- Microsoft Research (Collaboration)
- EMVCo (Collaboration)
- Invensys Rail (Collaboration)
- Mastercard UK (Collaboration)
- Frazer-Nash Consultancy (Collaboration)
- National Institute of Informatics (NII) (Collaboration)
- Network Rail (Collaboration)
Publications

A.V. Papadopoulos
(2018)
AdaptMC: A Control-Theoretic Approach for Achieving Resilience in Mixed-Criticality Systems



Aalsaud A
(2020)
Low-Complexity Run-time Management of Concurrent Workloads for Energy-Efficient Multi-Core Systems
in Journal of Low Power Electronics and Applications


Abdulfattah A
(2019)
Performance Analysis of MICS-Based RF Wireless Power Transfer System for Implantable Medical Devices
in IEEE Access

Abeyrathna K
(2021)
A multi-step finite-state automaton for arbitrarily deterministic Tsetlin Machine learning
in Expert Systems


Ait-Ameur Y, Bogomolov S, Dupont G, Iliasov A, Romanovsky A, Stankaitis P
(2023)
A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems
Description | We have developed the concept of holistic fault tolerance - this is a new way of ensuring system dependability by developing fault tolerance that crosscuts the system/layer boundaries. Holistic fault tolerance supports a novel approach to system structuring and allows trading off the non-functional system properties, such as reliability, power consumption and performance, during system design. The wide-ranging experiment in two domains, many-core systems and Android app design, demonstrated its applicability. We have developed and deployed in the UK railway industry the SafeCap toolset supporting scalable fully-automated verification of railway signalling/interlocking. This research has been driven by the needs of the railway industry focusing on the overcoming the typical barriers to industrial deployment of the academic research in the area of formal methods. The work is based on the research supported by EPSRC and other funders since 2012. In the core of the original SafeCap development was the concept of the open and extendable modelling that enables reasoning about various (often, contradicting) requirements such as, reliability, safety, performance/capacity and energy consumptions in the railway domain. The collaboration by Jones (Newcastle) with Burns at York has been very productive. The 2019 Computer Journal paper tackles the important issue of how one arrives at the formal specification of a cyber-physical system. More recently, we have jointly studied how to apply the same core ideas to "Mixed Criticality Scheduling" - a joint paper was accepted by the most relevant workshop in this research area and we are currently working on both a short paper and a long paper for journals that take these ideas further. Slightly less advanced - but still on the Jones/Burns axis - is research that applies ideas from the Computer Journal paper to automotive systems. We expect to report more on all of these developments next year. The Leverhulme Grant reported under "Other Outputs" both grew out of work on the Platform Grant and was kick-started by its funding. The PDRA was bridged by the Platform Grant and some early trips (e.g. to discuss the project with Prof Gerard Alberts in Amsterdam) benefited from the Platform grant. This made it possible to present a paper at an international workshop and to prepare a paper that is in the process of being published (a version of this paper is available as the returned Technical Report CS-TR-1531). Of course, a full reference to the workshop publication will be added next year. Jones(Ncl) and Burns (York) continue their collaboration on formalising "Mixed Criticality Scheduling". One paper will appear in a "Festschrift" but can be seen now as ttp://arxiv.org/abs/2012.01493; another conference paper is about to be submitted. |
Exploitation Route | The idea of holistic fault tolerance could be explored in various domains to develop new architectures that can meet various non-functional properties. The experimental tools and libraries developed by the project team could be used and extended by others. The SME we have created (The Formal Route) further develops the work on SafeCap and is now working with a number of industrial partners in the UK on extending the SafeCap toolset and applying it in real industrial settings. |
Sectors | Aerospace Defence and Marine Digital/Communication/Information Technologies (including Software) Financial Services and Management Consultancy Transport |
Description | We have been developing a toolset (called SafeCap) for formal automated verification of railway signalling to ensure its safety and to save the development cost and reduce time to market in railway industry. This approach has demonstrated its efficiency in running a number of pilot studies in which real railway datasets have been analysed. For some companies working closely with us this is opening new business opportunities in offering new business services on the market. Other companies are integrating the toolset into the existing company processes of ensuring the correctness and quality of their signalling datasets. The SafeCap approach is unique in ensuring the high scalability of automated verification and in minimising the upfront cost of training for signalling engineers. Starting from 2021 the SafeCap technology is widely used by Siemens Mobility and Volker Rail in their signalling projects delivered to Network Rail. The SME created by the STARTA project team called The Formal Route Ltd is now developing and expanding the SafeCap verification technology, and providing the consultancy services to the signalling companies. |
First Year Of Impact | 2019 |
Sector | Transport |
Impact Types | Economic |
Description | Case studentship |
Amount | £35,000 (GBP) |
Organisation | Siemens AG |
Sector | Private |
Country | Germany |
Start | 01/2014 |
End | 09/2020 |
Description | Development of the tools for verifying safety of railway signalling/interlocking data |
Amount | £1 (GBP) |
Funding ID | Several successive consultancy grants funded by the company. |
Organisation | Siemens AG |
Department | Siemens Rail Automation |
Sector | Private |
Country | Global |
Start | 01/2016 |
End | 05/2020 |
Description | Discovery Grant |
Amount | $880,286 (AUD) |
Funding ID | DP190102142 |
Organisation | Australian Research Council |
Sector | Public |
Country | Australia |
Start | 06/2019 |
End | 06/2022 |
Description | Newton Fund Grant Institutional Links |
Amount | £99,926 (GBP) |
Funding ID | 273018638 |
Organisation | British Council |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 03/2017 |
End | 03/2019 |
Description | PayCal - payment calculus for dependable payment protocols |
Amount | £35,000 (GBP) |
Organisation | Innovate UK |
Sector | Public |
Country | United Kingdom |
Start | 01/2018 |
End | 04/2018 |
Description | Separation and interference: learning from the history of concurrency |
Amount | £138,000 (GBP) |
Funding ID | RPG-2019-020 |
Organisation | The Leverhulme Trust |
Sector | Charity/Non Profit |
Country | United Kingdom |
Start | 11/2019 |
End | 10/2022 |
Description | Several consultancy projects on safety verification of railway signalling data |
Amount | £1 (GBP) |
Organisation | Siemens AG |
Department | Siemens Rail Automation |
Sector | Private |
Country | Global |
Start | 02/2020 |
End | 05/2020 |
Description | Siemens iCASE: Theories, techniques and tools for engineering complex railway systems consisting of mixed signalling areas |
Amount | £35,000 (GBP) |
Organisation | Siemens AG |
Department | Siemens Rail Automation |
Sector | Private |
Country | Global |
Start | 08/2016 |
End | 02/2020 |
Description | Asynchronous Design Automation |
Organisation | Dialog Semiconductor |
Country | United Kingdom |
Sector | Private |
PI Contribution | Development of methodology, design flow and tools for asynchronous control of analog-mixed signal electronics |
Collaborator Contribution | Provision of R&D case studies and guidance on design methodologies and tools |
Impact | Research papers and tools. |
Start Year | 2014 |
Description | Collaboration with Dialog Semiconductor |
Organisation | Dialog Semiconductor |
Country | United Kingdom |
Sector | Private |
PI Contribution | Providing R&D and tool support for automated design of asynchronous circuits |
Collaborator Contribution | Supporting developments of both open source software and company service, funding a PhD scholarship at Newcastle |
Impact | Publications, software, training courses |
Start Year | 2015 |
Description | Collaboration with EMVCo |
Organisation | EMVCo |
Sector | Charity/Non Profit |
PI Contribution | Formal specification and analysis of next generation payment protocols kernel |
Collaborator Contribution | Close collaboration and early research opportunities for future payment protocols |
Impact | Three publications: 2 at SBMF 2018; 1 at Overture 2018 |
Start Year | 2017 |
Description | Collaboration with Frazer-Nash Consultancy on railway safety assurance |
Organisation | Frazer-Nash Consultancy |
Country | United Kingdom |
Sector | Private |
PI Contribution | We bring the knowledge of formal verification and tool development |
Collaborator Contribution | FN brings the domain expertise and the knowledge of assurance processes in railway |
Impact | Too early to report |
Start Year | 2018 |
Description | Collaboration with MasterCard |
Organisation | Mastercard UK |
Country | United Kingdom |
Sector | Public |
PI Contribution | Formal specification and analysis of current commercial payment protocols |
Collaborator Contribution | Work on payment protocols |
Impact | Contractually confidential |
Start Year | 2017 |
Description | Collaboration with Microsoft Research |
Organisation | Microsoft Research |
Country | Global |
Sector | Private |
PI Contribution | Dr Andrey Mokhov, member of the Newcastle team has been working closely with Microsoft Research on developing modelling foundation based on graph algebra for build systems. Andrey Mokhov holds a research fellowship from Royal Society in which MSR is a key partner. |
Collaborator Contribution | Dr Simon Peyton-Jones, one of the leading Research Scientists at MSR, Cambridge, collaborated with Dr Andrey Mokhov. They published a number of papers. Andrey Mokhov holds a research fellowship from Royal Society in which MSR is a key partner. |
Impact | Joint publications |
Start Year | 2015 |
Description | Collaboration with Network Rail on verification of signalling |
Organisation | Network Rail Ltd |
Country | United Kingdom |
Sector | Private |
PI Contribution | We are contributing with developing tools for formal verification of signalling |
Collaborator Contribution | NR contributes with the knowledge of the domain and the market trends |
Impact | Too early to report |
Start Year | 2017 |
Description | Cooperation with ClearSy |
Organisation | ClearSy |
Country | France |
Sector | Private |
PI Contribution | We have established a close cooperation with ClearSy (French SME working in railway domain, http://www.clearsy.com/). The cooperation plans include tool integration, joint project proposals, and staff visits. |
Collaborator Contribution | The partner bring into this cooperation the knowledge of the French railway sector and their successful experience in applying formal methods in the domain. |
Impact | We have lunched together a very successful International Conference on reliability, safety and security of railway systems: modelling, analysis, verification and certification (RSSRail). The 3rd edition RSSRail 2019 was held in June 2019 in Lille. |
Start Year | 2012 |
Description | Cooperation with SYSTRA Scott Lister on developing advisory systems |
Organisation | SYSTRA Scott Lister |
Country | Australia |
Sector | Private |
PI Contribution | We are cooperating with SYSTRA on developing new methods for engineering trustworthy advisory systems for railway. Our team brings the expertise in trustworthy system engineering, knowledge base engineering, and requirement engineering. |
Collaborator Contribution | Feedback on the industrial relevance of our results in developing the advisory system. |
Impact | Too early to report |
Start Year | 2017 |
Description | Cooperation with SYSTRA Scott Lister on formal verification of railway signalling |
Organisation | SYSTRA Scott Lister |
Country | Australia |
Sector | Private |
PI Contribution | We are now working with the company on developing new techniques and tools for formal verification of railway signalling data and programs to ensure their safety . Our team brings the expertise in scalable formal verification and tool development. |
Collaborator Contribution | In the area of formal verification of railway signalling SYSTRA brings into this collaboration their expertise in railway signalling and knowledge of the domain and of the market needs. |
Impact | Too early to report |
Start Year | 2017 |
Description | Cooperation with Siemens Rail Automation |
Organisation | Invensys Rail |
Country | United Kingdom |
Sector | Private |
PI Contribution | We are developing new methods for engineering trustworthy advisory systems for railway traffic management. Our team contributes the expertise in trustworthy system engineering and in requirement engineering. |
Collaborator Contribution | Feedback and advice on the research results developed |
Impact | No outputs at this stage except for a number of publications. But the work on developing novel practical techniques for safety verification is successfully moving forward. |
Start Year | 2012 |
Description | Cooperation with Sydney Trains on formal verification of railway signalling/interlocking |
Organisation | Australian Government |
Department | Sydney Trains |
Country | Australia |
Sector | Public |
PI Contribution | Our team is developing a practical scalable and automated approach to verification of railway signalling |
Collaborator Contribution | The real datasets and experience of working in the sector |
Impact | Too early to report |
Start Year | 2018 |
Description | Cooperation with Vilnius University, Faculty of Mathematics and Informatics |
Organisation | Vilnius University |
Country | Lithuania |
Sector | Academic/University |
PI Contribution | Our work of developing tools for verification of railway safety |
Collaborator Contribution | Deep knowledge of the foundational theories of formal modelling/analysis. |
Impact | Publication of several papers prepared by the members of th two teams. |
Start Year | 2017 |
Description | Scuba Tx spin out |
Organisation | ScubaTx Limited |
Country | United Kingdom |
Sector | Private |
PI Contribution | 2 patent on underlying technology 1 journal paper |
Collaborator Contribution | Novel organ preservation technologies |
Impact | 4 UK patents 1.8M£ seed fund raising ongoing 1 Industrial PhD |
Start Year | 2018 |
Description | cooperation with National Institute of Informatics, Japan |
Organisation | National Institute of Informatics (NII) |
Country | Japan |
Sector | Public |
PI Contribution | Experience in developing and deploying the Event-B technology |
Collaborator Contribution | Knowledge and experience in deploying formal methods and tools in Japanese industry. |
Impact | Joint papers and books. Jointly organised seminars, tutorials, conferences and workshops. Organisation of training sessions for industrial engineers in Tokyo and Kyoto. |
Start Year | 2016 |
Description | cooperation with The Formal Route on railway signalling verification |
Organisation | The Formal Route |
Country | United Kingdom |
Sector | Private |
PI Contribution | Knowledge and experience in formal modelling and automated verification. |
Collaborator Contribution | The SME contributes with the experience and knowledge of the technology transfer in the railway sector. |
Impact | Application of the tools developed in the university |
Start Year | 2020 |
Title | Body tissue preservation system and method |
Description | Method to securely and dependably control and simplify interface of a medical device through security protocol approach. |
IP Reference | GB2004380.8 |
Protection | Patent application published |
Year Protection Granted | 2021 |
Licensed | Commercial In Confidence |
Impact | Method to securely and dependably control and simplify interface of a medical device through security protocol approach. |
Title | System and Method |
Description | Method to summarise and provide medically usable audit for body preservation control system |
IP Reference | GB2004378.2 |
Protection | Patent application published |
Year Protection Granted | 2021 |
Licensed | Commercial In Confidence |
Impact | Method to summarise and provide medically usable audit for body preservation control system |
Title | The SafeCap toolset for improving railway capacity while ensuring its safety. |
Description | SafeCap is an Eclipse-based tool for entering and analysing railway junction schemas. The tool aims to be extensible and configurable and may be applied in a number of contexts such the analysis of control table for junction signals, assessment of capacity impact of signal positioning and train detection circuit boundaries, and also for conducting semi-automatic or automatic changes to schema topology or control tables. Among other functionalities the toolset supports scalable fully-automated verification of railway signalling/interlocking and is easy to integrate into the current development processes in the railway companies. |
Type Of Technology | Software |
Year Produced | 2013 |
Open Source License? | Yes |
Impact | SafeCap is an Eclipse-based toolset for entering and analysing railway junction schemas. The toolset aims to be extensible and configurable and may be applied in a number of contexts such the analysis of control table for junction signals, assessment of capacity impact of signal positioning and train detection circuit boundaries, and also for conducting semi-automatic or automatic changes to schema topology or control tables. Among other functionalities the toolset supports scalable fully-automated verification of railway signalling/interlocking. This version of the toolset targets the signalling designed in the standard digital notations (SSI, SDEF, RailML, et.) used in the industry and is easy to integrate into the current development processes in the railway companies. In 2019 the toolset was approved for the use for formal verification of signalling in the UK for and has been used by several major railway companies in the country. |
URL | https://safecap.co.uk/ |
Title | dgdguk/drs: v1.0.0 |
Description | Initial release of DRS, corresponds to version used for publication. Future versions will add new features / fix bugs. |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
URL | https://zenodo.org/record/4118059 |
Title | dgdguk/drs: v2.0.0 |
Description | Implementation of the Dirichlet Rescale Algorithm (DRS). See the README for additional information. If you wish to use this software, the preferred method is to install via
pip install drs . Changes in v2.0.0: Changes to the behaviour of the algorithm mean that this release breaks compatibility with v1.0.0. Changes behaviour so that
lower_bound == upper_bound behaves as expected rather than being an error Replaces
constraints with
bounds (shorter variable names as before these were getting out of hand) Updates internal variable names to be more consistent and less influenced by the real-time systems use case Improvements to documentation |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
URL | https://zenodo.org/record/4264857 |
Title | dgdguk/drs: v2.0.0 |
Description | Implementation of the Dirichlet Rescale Algorithm (DRS). See the README for additional information. If you wish to use this software, the preferred method is to install via
pip install drs . Changes in v2.0.0: Changes to the behaviour of the algorithm mean that this release breaks compatibility with v1.0.0. Changes behaviour so that
lower_bound == upper_bound behaves as expected rather than being an error Replaces
constraints with
bounds (shorter variable names as before these were getting out of hand) Updates internal variable names to be more consistent and less influenced by the real-time systems use case Improvements to documentation |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
URL | https://zenodo.org/record/4118058 |
Company Name | ScubaTx |
Description | ScubaTx develops an organ preservation system. |
Year Established | 2020 |
Impact | 1.8M£ ongoing fund raise, development of new medical device for organ preservation |
Website | https://www.scubatx.com/ |
Company Name | The Formal Route Limited |
Description | The Formal Route specializes in applying formal methods to computerized railway signaling, with a focus on providing mathematical models and tools for industrial design and safety verification. |
Year Established | 2011 |
Impact | Too early to say |
Website | http://www.rodintools.com |
Description | Blog on Energetic Computing |
Form Of Engagement Activity | Engagement focused website, blog or social media channel |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | This blog is intended to communicate my views on a number of topics around Energy-Modulated Computing, such as Energy-driven computing, Real Power Computing, Electromagnetism, Causality, Asynchronous Circuits and Systems etc. |
Year(s) Of Engagement Activity | 2012,2013,2014,2015,2016,2017,2018,2019,2020 |
URL | https://blogs.ncl.ac.uk/alexyakovlev/ |
Description | Exhibiting the SafeCap tool at the industrial conference |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Industry/Business |
Results and Impact | We had a stand at the SIG X-20 event organised by Network Rail in February 2020 in Bristol. Our aim was to demo the SafeCap toolset and to engage with the companies that could use it. |
Year(s) Of Engagement Activity | 2020 |
Description | Interview to IET on the IET Achievement Award |
Form Of Engagement Activity | A press release, press conference or response to a media enquiry/interview |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | I was awarded an Achievement Medal by IET and gave a brief interview expressing how my research impacts industry and academia. |
Year(s) Of Engagement Activity | 2018 |
URL | https://conferences.theiet.org/achievement/winners/achievement/achieve-medals-winners.cfm |
Description | Keynote at the ISSRE 2020 conference entitled Holistic Fault Tolerance |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | A keynote outlining the main ideas and the application of holistic fault tolerance |
Year(s) Of Engagement Activity | 2019 |
Description | Research presentation at MasterCard UK HQ on EMVCo's payment protocols |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Reporting on the analysis of EMV Next Generation protocols |
Year(s) Of Engagement Activity | 2018 |
Description | Tutorial on using SafeCap for signalling verification |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | Tutorial entitled SafeCap: Automated formal verification of railway signalling interlockings was given at the RSSRail 2019 conference in Lille. RSSRail is a unique conference focusing on advancing the cooperation between academia and industry. The tutorial was well received with many followup discussions and new cooperations established. |
Year(s) Of Engagement Activity | 2019 |
URL | https://conferences.ncl.ac.uk/rssrail2019/tutorials/ |