Trustworthy Adaptive and Autonomous Systems & Processes — TASP

TASP is a research team within the Department of Computer Science at the University of York. Our research focuses on the development of tool-supported formal approaches for the engineering of autonomous and self-adaptive robotic, cyber-physical, embedded, service-based and cloud computing systems and critical business processes. The interests of the team include
  • probabilistic model checking for autonomous, self-adaptive, secure and resilient systems and processes
  • automated and model-driven software and process engineering
  • runtime formal specification, modelling, analysis, verification and controller synthesis
and the application of the theories, approaches and techniques specific to the above research areas to the engineering of trustworthy autonomous, cyber-physical, service-based and cloud computing systems, and critical business processes. The team's research has been supported by EPSRC, Dstl, Lloyds Register Foundation and Welcome Trust grants totalling over £2M.
This page summarises some of the recent TASP activities. For additional information, contact the team leader,
Prof Radu Calinescu.

Recently Developed TASP Techniques and Tools
FACT probabilistic model checker
FACT computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. Find out more on the FACT website, watch the demo below, or read our IEEE Trans Reliability paper.
  OMNI observation-based Markov chain refinement
OMNI greatly improves the accuracy with which non-functional properties of component-based software can be analysed using continuous-time Markov chains. Learn more on the OMNI website, watch the demo below, or read our ICSA-2017 paper.
EvoChecker search-based synthesis of probabilistic models for quality-of-service software engineering
EvoChecker employs multiobjective optimisation genetic algorithms to automate the synthesis of Pareto-optimal designs for systems with competing non-functional requirements. Find out more on the EvoChecker website or read our ASE-2015 paper.
approach
  DECIDE - Decentralised control in distributed
self-adaptive software
DECIDE is a rigorous approach to decentralising the control loops of distributed self-adaptive software used in mission-critical applications. Find out more on the DECIDE website, watch the demo below, or read our ETAPS-2015 Best Paper Award nominated paper.
UNDERSEA simulator for engineering self-adaptive unmanned underwater vehicles
UNDERSEA is a simulated unmanned underwater vehicle system that other researchers can use to develop and evaluate new self-adaptation solutions. Find out more on
the UNDERSEA website, watch the demo below, or read
our SEAMS-2017 paper.
RODES - Designing robust systems through
synthesis of parametric Markov chains
RODES is a method for the synthesis of system designs that satisfy strict quality requirements, are Pareto-optimal with respect to a set of quality optimisation criteria, and are robust to variations in the system parameters. Find out
more on the DECIDE website, or read our ICSA-2017 paper.
Other methods and tools developed by the TASP research team include:
ARL — an assured reinforcement learning approach that uses quantitative verification to restrict the exploration of RL agents to Markov decision process regions guaranteed to yield solutions compliant with the given safety and performance constraints. Read our ICAART-2017 Best Student Paper Award winner paper.
saRBAC — an approach for dynamically reconfiguring the role-based access control (RBAC) of information systems running business processes, to protect them against insider threats. Read our SEAMS-2017 paper.
INVEST — a tool-supported framework for the efficient reverification of component-based systems after changes such as additions, removals or modifications of components. Find out more on the INVEST website, or read our CBSE-2013 paper.
COVE — an adaptive probabilistic model learning method for continual verification of nonfunctional properties. Find out more on the COVE website or read our ICPE-2014 paper.
Team Members

Latest News

February 2021
Paper accepted in ACM Computing Surveys
Our paper Assuring the Machine Learning Lifecycle: Desiderata, Methods, and Challenges was accepted for publication in ACM Computing Surveys.
Read preprint
December 2020
Paper accepted at ICSE'21
Our paper Fast Parametric Model Checking through Model Fragmentation was accepted at the 43rd International Conference on Software Engineering.
Read preprint
August 2020
Paper accepted at ASE'20
Our paper Interval Change-Point Detection for Runtime Probabilistic Model Checking was accepted at the 35th IEEE/ACM International Conference on Automated Software Engineering.
Read paper
December 2019
UCC'19 Keynote
Taming Service Uncertainty through Probabilistic Model Learning, Analysis and Synthesis keynote given at the 12th IEEE/ACM International Conference on Utility and Cloud Computing.
Read summary
December 2019
Paper published in Acta Crystallographica
Our paper Comparison of automated crystallographic model-building pipelines was published in Acta Crystallographica Section D: Structural Biology.
Read paper
April 2019
Paper published in IEEE Trans. Softw. Eng.
Our paper Efficient Parametric Model Checking Using Domain Knowledge was published in IEEE Transactions on Software Engineering.
Read paper
November 2018
Paper published in IEEE Trans. Softw. Eng.
Our paper Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases describing joint work with researchers at KU Leuven and Linnaeus University was published in IEEE Transactions on Software Engineering.
Read paper