STRATA; Layers for Structuring Trustworthy Ambient Systems

Lead Research Organisation: Newcastle University
Department Name: Sch of Computing


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.

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.
Description We have developed the concept of holistic fault tolerance - this is a new way of ensuring system dependability by developing fault tolerence that crosscuts the system/layer boundaries.
Exploitation Route This idea could be explored in various domains to develop new architectures that can meet various non-functional properties
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Transport

Description We have been developing a toolset for formal automated verification of railway signalling to ensure its safety and to save the development cost 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. Other companies are integrating the toolset into the existing company processes of ensuring the correctness and quality of their signalling datasets.
First Year Of Impact 2019
Sector Transport
Impact Types Economic

Description Development of the tools for verifying safety of railway signalling/interlocking data
Amount £210,000 (GBP)
Funding ID These have been the 4 successive grants funded by the company. 
Organisation Siemens AG 
Department Siemens Rail Automation
Sector Private
Country Global
Start 01/2017 
End 05/2019
Description Discovery Grant
Amount $880,286 (AUD)
Funding ID DP190102142 
Organisation Australian Research Council 
Sector Public
Country Australia
Start 07/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 04/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 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 09/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 Frazer-Nash Consultency on railway safety assurence 
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
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 Network Rail on verification of signalling 
Organisation Network Rail Ltd
Country United Kingdom 
Sector Private 
PI Contribution We are contributing with developing tools fro 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 Alstom 
Organisation Alstom
Department Alstom Energy Technology Centre
Country United Kingdom 
Sector Private 
PI Contribution The work is starting on applying our solutions to automated verification of signalling under development in the company
Collaborator Contribution Experience in the field, real industrial projects.
Impact too early to report
Start Year 2018
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, The cooperation plans include tool integration, joint project proposals, and staff visits.
Collaborator Contribution The partner bring into thic cooperation the knowledge of teh French railway sector and their succesful expeirence in applying formal methods in. the domain
Impact We have lanched together a very succesful International Conference on reliability, safety and security of railway systems: modelling, analysis, verification and certification. We are now working on the 3rd edition RSSRail 2019 (Lille, June 2019).
Start Year 2012
Description Cooperation with SYSTRA Scott LIster on developing advisory systems 
Organisation SYSTRA Scott Lister
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
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 bring the expertise in scalable formal verification and tool development.
Collaborator Contribution In the area of formal verification of railway signalling SYSTRA brings 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 Autormation 
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 conributes 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 succesfully moving forward.
Start Year 2012
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 Joint papers.
Start Year 2017
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
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