-
RoboChart & RoboSim: modelling robots and collections [slides]
Speaker:
Alvaro Miyazawa
23rd
of January 2019, 12h30, CSE/203
-
Reasoning in tock-CSP with FDR
Speaker:
Pedro Ribeiro
30th
of January 2019, 12h30, PZA/022 (Piazza Building)
Abstract: Specifying budgets and deadlines using a process algebra like CSP requires an...
Abstract: Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The dialect tock-CSP embeds a rich and flexible approach for modelling discrete timed behaviours with powerful tool support using the CSP model checker FDR. Analysis, however, has traditionally used the standard semantics of CSP, which is inadequate for reasoning about timed refinement. Previous approaches have focused on traces refinement only or not considered the role of deadlines. The most recent version of FDR provides support for tock-CSP, including specific operators. For instance, to ensure maximal progress internal events can be prioritised over tock using a prioritise operator, whose denotational semantics is given in the finite-linear model. It remains, however, that the standard semantics of CSP is inadequate. In this talk we present an alternative semantic model for tock-CSP that encompasses a definition for prioritise. To enable the use of FDR to reason using this model, we use an encoding of refusals via traces. For validation, and to obtain a suitable definition for prioritise in tock-CSP, we establish a stepwise Galois connection with the finite-linear model. Our results have been mechanised using the proof assistant Isabelle/HOL.
-
Epistemic and Temporal Epistemic Logics of Authentication [slides]
Speaker:
Sharar Ahmadi
12th
of February 2019, 12h30, CSE/203
Abstract: The authentication properties of a security protocol are specified based on t...
Abstract: The authentication properties of a security protocol are specified based on the knowledge gained by the principals that exchange messages with respect to the steps of that protocol. As there are many successful attacks on authentication protocols, different formal systems, in particular epistemic and temporal epistemic logics, have been developed for analysing such protocols. However, such logics may fail to detect some attacks. To promote the specification and verification power of these logics, researchers try to construct them in such a way that they preserve some properties such as soundness, completeness, being omniscience-free, or expressiveness. The aim of this talk is to provide an overview of the epistemic and temporal epistemic logics of authentication.
-
Orca: a functional correctness verifier based on Isabelle/UTP
Speaker:
Yakoub Nemouchi
26th
of February 2019, 12h30, CSE/203
Abstract: We present Orca, a functional correctness verifier based on Isabelle/UTP. A n...
Abstract: We present Orca, a functional correctness verifier based on Isabelle/UTP. A novelty of Orca is the ability to tackle a variety of language aspects at the semantic level by leveraging the semantics combination facilities of Hoare and He’s Unifying Theories of Programming. This supports genericity by allowing application of the underlying verification theorems to various languages. Orca comes with a set of Isabelle/HOL rules for Hoare Logic and laws of programming for the standard programming operators as well as non-trivial rules for modular reasoning. Orca extends isar to offer a nice front-end for parsing programs with a C-like syntax. Automatic reasoning is supported via Orca's backend which consists of a verification condition generator (VCG) and a parallel version of sledgehammer. The VCG is equipped with Hoare rules for forward reasoning to automatically compute the strongest postcondition(SP) and backward reasoning to automatically compute the weakest precondition (WP). Orca's VCG comes with two modes, the first mode is proof annotation where loop invariants are annotated interactively during the proof. The second mode of the VCG assumes that the program is already annotated with invariants.
-
CANCELLED - A UTP theory for Hybrid Computation
Speaker:
Simon Foster
9th
of April 2019, 12h30, CSE/202
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extend...
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid dynamical systems, supported by our mechanisation in Isabelle/UTP, which employs the HOL-Analysis and HOL-ODE packages for functional analysis. The hybrid relational calculus is built upon the same foundation as the UTP's theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise-continuous functions that we will describe. From this foundation, we give semantics to the core operators of the hybrid relational calculus, including ODEs and preemption, and show how the theory can be used to verify sequential hybrid systems. We also highlight our work in using the theory to give a denotational semantics to the Modelica language for hybrid dynamical systems modelling.
-
Risk Structures: Towards Engineering Risk-aware Autonomous Robots
Speaker:
Mario Gleirscher
16th
of April 2019, 16h00, CSE/202
Abstract: To achieve acceptable safety, autonomous robots will have to reduce risk by i...
Abstract: To achieve acceptable safety, autonomous robots will have to reduce risk by incorporating autonomous risk handling mechanisms that enhance their mission controllers. The missing fallback to local or remote human operators as well as complex operational environments pose hard challenges to the engineering of appropriate risk handlers, particularly, to the hazard analysis and risk modelling activities leading to such handling mechanisms. This talk will give a brief introduction to risk analysis and modelling for risk-aware robots. Then, it will present a framework and method for the step-wise development of risk handling mechanisms. Last, it will illustrate how these mechanisms can be used in controllers of such robots.
-
Foundational end-to-end verification of cyber-physical systems: The VeriPhy pipeline and its Applications
Speaker:
Brandon Bohrer
17th
of July 2019, 11h30, PZA/016
Abstract: We first present VeriPhy, a verified pipeline which automatically transforms ...
Abstract: We first present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end as it bridges abstraction gaps, including:
1) the gap between mathematical reals in physical models and machine arithmetic in the implementation,
2) the gap between real physics and its differential-equation models, and
3) the gap between nondeterministic controller models and machine code.
VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle. To minimize the trusted base, we cross-verify the KeYmaera X prover core in Isabelle.
We discuss two practical case studies applying VeriPhy to ground robots:
1) the initial study, tested on commodity hardware, uses a robot moving in a simple straight-line pattern,
2) a follow-up study gives a realistic model for general free-range 2D driving by following a series of arcs and was implemented in AirSim's realistic autonomous driving simulation.
-
CANCELLED - Testing Robots using CSP
Speaker:
James Baxter
18th
of September 2019, 15h00, CSE/203
Abstract: We present a technique for automatic generation of tests for robotic systems ...
Abstract: We present a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the defini- tion of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock- CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to gen- erate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.
-
Testing Robots using CSP
Speaker:
James Baxter
25th
of September 2019, 15h00, CSE/102
Abstract: We present a technique for automatic generation of tests for robotic systems ...
Abstract: We present a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the defini- tion of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock- CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to gen- erate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.
-
[CANCELLED] RoboChart & RoboTool: modelling and verification of probabilistic systems
Speaker:
Kangfeng Ye
1st
of October 2019, 12h30, CSE/102&103
Abstract: In addition to standard state machines and time primitives, RoboChart also su...
Abstract: In addition to standard state machines and time primitives, RoboChart also supports probabilistic choices, which allows us to model probabilistic systems in RoboChart. This seminar starts with an introduction of probability modelling in RoboChart using a robotic example. Then it will more focus on how to verify these systems in RoboTool by using PRISM, an existing probabilistic model checker. With recently designed probabilistic assertion language in RoboTool, users are able to use RoboTool even without knowledge of PRISM. However, for advanced users or complicated models, this seminar will give you some hints on how to flexibly use RoboTool and PRISM to verify the properties that are not easily verified by just clicking buttons on RoboTool.
-
A UTP theory for Hybrid Computation
Speaker:
Simon Foster
3rd
of October 2019, 16h00, CSE/202
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extend...
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid dynamical systems, supported by our mechanisation in Isabelle/UTP, which employs the HOL-Analysis and HOL-ODE packages for functional analysis. The hybrid relational calculus is built upon the same foundation as the UTP's theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise-continuous functions that we will describe. From this foundation, we give semantics to the core operators of the hybrid relational calculus, including ODEs and preemption, and show how the theory can be used to verify sequential hybrid systems. We also highlight our work in using the theory to give a denotational semantics to the Modelica language for hybrid dynamical systems modelling.
-
RoboChart & RoboTool: modelling and verification of probabilistic systems
Speaker:
Kangfeng Ye
15th
of October 2019, 12h30, CSE/202
Abstract: In addition to standard state machines and time primitives, RoboChart also su...
Abstract: In addition to standard state machines and time primitives, RoboChart also supports probabilistic choices, which allows us to model probabilistic systems in RoboChart. This seminar starts with an introduction of probability modelling in RoboChart using a robotic example. Then it will more focus on how to verify these systems in RoboTool by using PRISM, an existing probabilistic model checker. With recently designed probabilistic assertion language in RoboTool, users are able to use RoboTool even without knowledge of PRISM. However, for advanced users or complicated models, this seminar will give you some hints on how to flexibly use RoboTool and PRISM to verify the properties that are not easily verified by just clicking buttons on RoboTool.
-
From computer says no to robot says yes: engineering a positive future for robotics
Speaker:
Ana Cavalcanti
6th
of January 2020, 15h30, CSE/203
Abstract: With the prospect of sophisticated robots working ever more closely with huma...
Abstract: With the prospect of sophisticated robots working ever more closely with humans, it is vital that software engineers have the tools and techniques to ensure safety and reliability. Professor Ana Cavalcanti, a computer scientist whose research is changing the very language of robotic software development, is on a mission to ensure that, unlike the computer, the robot never says no: that it does the right thing at the right time, every time. To achieve this, Professor Cavalcanti and her team are developing a framework for the modelling and simulation of mobile and autonomous robots, bringing outdated software engineering practices, based on trial and error, into the state-of-the-art. Her vision is a 21st-century toolbox for robot-controller developers that will enable the safe application of socially beneficial robotics, allowing the UK to tap into a multibillion dollar global robotics market.
-
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs
Speaker:
Brijesh Dongol
23rd
of January 2020, 14h30, CSE/102
Abstract: Teleo-Reactive (TR) robotic agent programs comprise sequences of guarded acti...
Abstract: Teleo-Reactive (TR) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a TR programmed robotic agent has a deductive Belief Store comprising constantly changing predicate logic percept facts, and knowledge facts and rules for querying the percepts. In this paper we introduce TR programming using a simple example expressed in the teleo-reactive programming language TeleoR, which is a syntactic extension of QuLog, a typed logic programming language used for the agent’s Belief Store. We give a formal definition of the regression property that rules of TeleoR procedures should satisfy, and an informal operational semantics of the evaluation of a TeleoR procedure call. We then formally express key features of the evaluation in LTL. Finally we show how this LTL formalisation can be used to prove that a procedure’s rules satisfy the regression property by proving it holds for one rule of the example TeleoR program. The proof requires us: to formally link a TeleoR agent’s percept beliefs with sensed configurations of the external environment; to link the agent’s robotic device action intentions with actual robot actions; to specify the eventual physical effects of the robot’s actions on the environment state.
-
Towards an Isabelle EMF Meta-Model
Speakers:
Bestoon Hussien and Simon Foster
23rd
of September 2020, 10h30, Online
Abstract: Isabelle is both a proof assistant and a platform for developing verification...
Abstract: Isabelle is both a proof assistant and a platform for developing verification tools based on unification of mathematical theories of programming. It can be used to greatly improve software quality by automated formal analysis. However, Isabelle is out of reach for most software engineers, due to its steep learning curve. The aim of this work is to allow the integration of Isabelle into the software engineering lifecycle through integration with the EMF and Epsilon tool sets. We are developing a meta-model frontend to Isabelle's textual input language, Isar, which allows development of syntax and semantics for a variety of DSLs. This will allow us to bypass the need to write complex model-to-text transformations, and instead generate Isabelle through more straightforward model-to-model transformations. Our aim is to allow Isabelle-based verification tools to be accessed at the push of a button within Eclipse-based graphical tools, such as RoboTool. We demonstrate this with a model-to-model transformation from RoboChart to Isabelle/UTP.
-
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
Speaker:
James Baxter
7th
of October 2020, 10h30, Online
Abstract: Lenses are a useful algebraic structure for giving a unifying semantics to pr...
Abstract: Lenses are a useful algebraic structure for giving a unifying semantics to program variables in a variety of store models, which support efficient automated proof in the Isabelle/UTP verification framework. In this presentation, we expand our lens library with (1) dynamic lenses, that support mutable indexed collections, such as arrays, and (2) symmetric lenses, that allow partitioning of a state space into disjoint local and global regions to support variable scopes. From this basis, we provide an enriched program model in Isabelle/UTP for collection variables and variable blocks that can support a variety of data structures and state spaces.
-
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
Speaker:
Simon Foster
19th
of May 2021, 10h30, Online
Abstract: Simulation and formal verification are important complementary techniques nec...
Abstract: Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for both activities. In this presentation we show how to apply Interaction Trees in Isabelle/HOL to produce a verification and simulation framework for state-rich process languages. We develop the core theory and verification techniques for Interaction Trees, use them to give a semantics to deterministic fragments of the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model. We also show how the Isabelle code generator can be used to generate verified executable simulations for reactive and concurrent programs. We hope in the future to apply this work in providing a route to formally verified animations of RoboChart/RoboSim models.
-
The Pi-puck: a Raspberry Pi enhanced e-puck robot platform
Speaker:
Alan Millard
17th
of November 2021, 10h30, Online
Abstract: This talk will present the Pi-puck extension board - an interface between the...
Abstract: This talk will present the Pi-puck extension board - an interface between the e-puck robot and a Raspberry Pi single-board computer that enhances the robot's processing, sensing, and networking capabilities. This enhanced robot platform was designed specifically for swarm robotics research, but is also suitable for multi-robot and single-robot applications. The hardware was developed across multiple projects at the University of York, the final form of which is now commercially available. Software support for this hardware is currently being developed in collaboration with our international partners. This talk will highlight the main hardware features of the platform, and will detail the existing software ecosystem, including integration with the ARGoS and Webots robot simulators, as well as the Robot Operating System (ROS). Our aim is to allow robot control code to be prototyped in simulation and then deployed on physical hardware without modification. The talk will conclude with a discussion of future plans for the platform, and the research that it hopes to facilitate.
-
Transforming RoboSim Models into UPPAAL
Speaker:
Mingzhuo Zhang
1st
of December 2021, 10h30, Online
Abstract: RoboSim is a tool-independent notation for modeling software simulations of r...
Abstract: RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this presentation, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.
-
From RoboSim to another CSP - CLEARSY Safety Platform [slides]
Speaker:
Thierry Lecomte
26th
of January 2022, 10h30, Online
Abstract: RoboSim is a diagrammatic language to model simulations of robotic systems to...
Abstract: RoboSim is a diagrammatic language to model simulations of robotic systems to define concurrent and distributed designs. In this presentation, we explore the use of the CLEARSY Safety Platform (https://lnkd.in/drwW_RDf) as a safety critical execution platform for these models. We draw the outline of a model-transformation strategy to translate RoboSim models into B models as supported by the CLEARSY Safety Platform. The transformation of several simple examples illustrate the preliminary results of this on-going joint research between CLEARSY and Metrópole Digital - IMD/UFRN.
-
Visual Specification of Properties for Robotic Designs
Speakers:
Waldeck Lindoso Jr., Sidney C. Nogueira, and Lucas Lima
9th
of March 2022, 10h30, Online
Abstract: RoboChart is a diagrammatic notation based on UML designed for modelling robo...
Abstract: RoboChart is a diagrammatic notation based on UML designed for modelling robotic software that has well-defined semantics in the notation of CSP process algebra, enabling the automatic proof of process refinements using the FDR tool. Although RoboChart allows the specification of the robot software, the definition of application-specific properties of RoboChart models must be specified using the CSP notation. Thus, the designer must be familiar with CSP to define and verify properties. This work proposes an approach for the automatic verification of properties using a diagrammatic notation that expresses the behaviour of RoboChart models. The approach proposes a diagrammatic notation based on UML activity diagrams that support the specification of behaviour mixing standard elements of the activity diagram with elements of RoboChart as events and operations. The diagram behaviour is formalised as a CSP process used to verify the properties of a RoboChart component. A plug-in for the Astah modelling tool has been developed to translate the diagram to CSP and call the FDR refinement checker, which verifies whether the RoboChart model refines the property specified with the proposed notation. Our proposed approach allows the designer to specify and verify properties of RoboChart models using diagrammatic notations with no knowledge of the underlying formal semantics.
-
[CANCELLED] Mixed Signals: audio and wearable data analysis for health diagnostics
Speaker:
Cecilia Mascolo
22nd
of June 2022, 13h30, Online
Abstract: Wearable and mobile devices are very good proxies for human behaviour. Yet, m...
Abstract: Wearable and mobile devices are very good proxies for human behaviour. Yet, making the inference from the raw sensor data to individuals’ behaviour remains difficult. The list of challenges is very long: from collecting the right data and using the right sensor, respecting resource constraints, identifying the right analysis techniques, labelling the data, limiting privacy invasion, to dealing with heterogeneous data sources and adapting to changes in behaviour.
In this talk, I plan to reflect on these challenges and highlight the opportunities that mobile and wearable health systems are introducing for community, the developers as well as the users. I will use examples from my group's ongoing research on exploring machine learning and data analysis for health application in collaboration with epidemiologists and clinicians. In particular I will concentrate a part of the talk on an project focusing on leveraging audio signals from the human body to help automated diagnostics and disease progression analysis.
Bio: Cecilia Mascolo is the mother of a teenage daughter but also a Full Professor of Mobile Systems in the Department of Computer Science and Technology, University of Cambridge, UK. She is a director of the Centre for Mobile, Wearable System and Augmented Intelligence. She is also a Fellow of Jesus College Cambridge and the recipient of an ERC Advanced Research Grant. Prior joining Cambridge in 2008, she was a faculty member in the Department of Computer Science at University College London. She holds a PhD from the University of Bologna. Her research interests are in mobile systems and machine learning for mobile health. She has published in a number of top tier conferences and journals in the area and her investigator experience spans projects funded by Research Councils and industry. She has served as steering, organizing and programme committee member of mobile and sensor systems, data science and machine learning conferences. More details at www.cl.cam.ac.uk/users/cm542
-
CSP in Practice: Timed Verification of Robot Software.
Speaker:
Matt Windsor
10th
of August 2022, 10h30, Online
Abstract: This talk describes work done by myself and the RoboStar team in York to tack...
Abstract: This talk describes work done by myself and the RoboStar team in York to tackle the verification of timed properties of robotic control software. We reduce the problem into one of concurrency reasoning, where Communicating Sequential Processes is the underlying formalism. On top of CSP, we build domain-specific languages that present specifications and implementation models in a manner that is both approachable to robotics experts and suitable for use in other ways (simulation model extraction, code generation, other formalisms, etc.). I discuss RoboChart, RoboStar's DSL for software models, and RoboCert, a DSL I am working on to handle specifications.
-
Formal Verification of ANN Components in RoboChart.
Speaker:
Ziggy Attala
24th
of August 2022, 10h30, Online
Abstract: We present a framework for obtaining system-level formal proofs of properties...
Abstract: We present a framework for obtaining system-level formal proofs of properties of robotic systems involving artificial neural network (ANN) controller components. Our focus is on neural networks for control, as opposed to neural networks for recognition. Existing verification work for these components is concerned with component-level properties, but our work deals with system-level properties. We describe our framework through its application is RoboChart, a domain-specific modelling language for robotics with support for formal verification. In particular, we define a method to prove refinement queries concerning these components.
-
Probabilistic modelling and verification using RoboChart and PRISM
Speaker:
Kangfeng Ye
5th
of October 2022, 10h30, Online
Abstract: RoboChart is a timed domain-specific language for robotics, distinctive in it...
Abstract: RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart’s probabilistic semantics is given in PRISM and implemented as an automatic technique in RoboTool (an accompanying tool of RoboChart) to transform a RoboChart model into a PRISM model for verification. We have also extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language. In this presentation, we describe probabilistic modelling and verification in RoboChart using a mail delivery robot as an example.
-
Formally Verified Animation for RoboChart Using Interaction Trees
Speaker:
Kangfeng Ye
19th
of October 2022, 10h30, Online
Abstract: RoboChart is a core notation in the RoboStar framework. It is a timed and pro...
Abstract: RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has formal denotational semantics given in CSP. Interaction Trees (ITrees) is a semantic technique to represent behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisation of ITrees along with ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this talk, we present the operational semantics of RoboChart using ITrees and its implementation in Isabelle. And then we use Isabelle’s code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector model. With animation, we show two concrete scenarios when the robot encounters different environmental inputs.
-
Formal Verification and Mechanisation of Cryptographic Constructions, Algorithms and Protocols
Speaker:
Roberto Metere
2nd
of November 2022, 10h30, Online
Abstract: Cybersecurity is a critical aspect in more and more real-world contexts. Comm...
Abstract: Cybersecurity is a critical aspect in more and more real-world contexts. Commonly, security is achieved through the (proper) employment of cryptographic constructions, algorithms and protocols. It is therefore fundamental to perform a correct analysis of security properties and their formalisation in a scientific, reproducible manner. Easier said than done, those tasks conceal difficult challenges and require complex arguments. One way to progressively tame such complexity is through mechanising cryptographic constructions (and computer networks at a higher level) by describing them in a mathematical, rigorous model, as well as providing automation for generating executable code that is linked to formal analysis.
-
Generalizing the Elo rating system for multiplayer games and races: why endurance is better than speed
Speaker:
Ben Powell
8th
of February 2023, 10h30, Online
Abstract: I will talk about a recent applied statistics project motivated by Formula On...
Abstract: I will talk about a recent applied statistics project motivated by Formula One racing. Specifically, I will introduce a non-standard generalization of the Elo rating system for sports competitions involving two or more participants. The new system can be understood as an online estimation algorithm for the parameters of a Plackett-Luce model, which can be used to make probabilistic forecasts for the results of future competitions. The system's distinguishing feature is the way it treats competitions as sequences of elimination-type rounds that sequentially identify the worst competitors rather than sequences of selection-type rounds that identify the best. The significance of this simple but important modelling choice will be discussed and its consequences explored.
-
Probabilistic relations for modelling epistemic and aleatoric uncertainties: its semantics and automated reasoning with theorem proving
Speaker:
Kangfeng Ye
28th
of June 2023, 10h30, CSE/082
Abstract: Probabilistic programming combines general computer programming, statistical ...
Abstract: Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, having a significant impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has attracted much interest. Many challenges, however, remain.
This talk presents probabilistic relations, a probabilistic sequential programming language for modelling both epistemic (or model) and aleatoric (or data) uncertainties. The language is a combination of Eric Hehner's Probabilistic Predicative Programming (PPP) and UTP alphabetised relations. In the language, sequential composition models condition probability and parallel composition models joint probability. It supports Bayesian inference using both compositions. Probabilistic relations are also equipped with a semantic framework for automated reasoning.
In the talk, I will discuss the motivations for this work, the complexity of analysing probabilistic programs, the syntax and semantics of probabilistic relations, along with a collection of algebraic laws. In particular, I will detail our approach that uses fixed-point theorems to give the semantics to probabilistic loops and present a unique fixed-point theorem to simplify the reasoning of probabilistic loops. I demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination and expected runtime of probabilistic loops.
We note that the language and its semantics are mechanised in the theorem prover Isabelle/UTP, and the algebraic laws and the examples are all proved too.
-
Probabilistic relations for modelling epistemic and aleatoric uncertainties: its semantics and automated reasoning with theorem proving
Speaker:
Kangfeng Ye
28th
of June 2023, 10h30, CSE/082
Abstract: Probabilistic programming combines general computer programming, statistical ...
Abstract: Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, having a significant impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has attracted much interest. Many challenges, however, remain.
This talk presents probabilistic relations, a probabilistic sequential programming language for modelling both epistemic (or model) and aleatoric (or data) uncertainties. The language is a combination of Eric Hehner's Probabilistic Predicative Programming (PPP) and UTP alphabetised relations. In the language, sequential composition models condition probability and parallel composition models joint probability. It supports Bayesian inference using both compositions. Probabilistic relations are also equipped with a semantic framework for automated reasoning.
In the talk, I will discuss the motivations for this work, the complexity of analysing probabilistic programs, the syntax and semantics of probabilistic relations, along with a collection of algebraic laws. In particular, I will detail our approach that uses fixed-point theorems to give the semantics to probabilistic loops and present a unique fixed-point theorem to simplify the reasoning of probabilistic loops. I demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination and expected runtime of probabilistic loops.
We note that the language and its semantics are mechanised in the theorem prover Isabelle/UTP, and the algebraic laws and the examples are all proved too.
-
Generalizing the Elo rating system for multiplayer games and races: why endurance is better than speed
Speaker:
Ben Powell
8th
of February 2023, 10h30, Online
Abstract: I will talk about a recent applied statistics project motivated by Formula On...
Abstract: I will talk about a recent applied statistics project motivated by Formula One racing. Specifically, I will introduce a non-standard generalization of the Elo rating system for sports competitions involving two or more participants. The new system can be understood as an online estimation algorithm for the parameters of a Plackett-Luce model, which can be used to make probabilistic forecasts for the results of future competitions. The system's distinguishing feature is the way it treats competitions as sequences of elimination-type rounds that sequentially identify the worst competitors rather than sequences of selection-type rounds that identify the best. The significance of this simple but important modelling choice will be discussed and its consequences explored.
-
Formal Verification and Mechanisation of Cryptographic Constructions, Algorithms and Protocols
Speaker:
Roberto Metere
2nd
of November 2022, 10h30, Online
Abstract: Cybersecurity is a critical aspect in more and more real-world contexts. Comm...
Abstract: Cybersecurity is a critical aspect in more and more real-world contexts. Commonly, security is achieved through the (proper) employment of cryptographic constructions, algorithms and protocols. It is therefore fundamental to perform a correct analysis of security properties and their formalisation in a scientific, reproducible manner. Easier said than done, those tasks conceal difficult challenges and require complex arguments. One way to progressively tame such complexity is through mechanising cryptographic constructions (and computer networks at a higher level) by describing them in a mathematical, rigorous model, as well as providing automation for generating executable code that is linked to formal analysis.
-
Formally Verified Animation for RoboChart Using Interaction Trees
Speaker:
Kangfeng Ye
19th
of October 2022, 10h30, Online
Abstract: RoboChart is a core notation in the RoboStar framework. It is a timed and pro...
Abstract: RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has formal denotational semantics given in CSP. Interaction Trees (ITrees) is a semantic technique to represent behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisation of ITrees along with ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this talk, we present the operational semantics of RoboChart using ITrees and its implementation in Isabelle. And then we use Isabelle’s code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector model. With animation, we show two concrete scenarios when the robot encounters different environmental inputs.
-
Probabilistic modelling and verification using RoboChart and PRISM
Speaker:
Kangfeng Ye
5th
of October 2022, 10h30, Online
Abstract: RoboChart is a timed domain-specific language for robotics, distinctive in it...
Abstract: RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart’s probabilistic semantics is given in PRISM and implemented as an automatic technique in RoboTool (an accompanying tool of RoboChart) to transform a RoboChart model into a PRISM model for verification. We have also extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language. In this presentation, we describe probabilistic modelling and verification in RoboChart using a mail delivery robot as an example.
-
Formal Verification of ANN Components in RoboChart.
Speaker:
Ziggy Attala
24th
of August 2022, 10h30, Online
Abstract: We present a framework for obtaining system-level formal proofs of properties...
Abstract: We present a framework for obtaining system-level formal proofs of properties of robotic systems involving artificial neural network (ANN) controller components. Our focus is on neural networks for control, as opposed to neural networks for recognition. Existing verification work for these components is concerned with component-level properties, but our work deals with system-level properties. We describe our framework through its application is RoboChart, a domain-specific modelling language for robotics with support for formal verification. In particular, we define a method to prove refinement queries concerning these components.
-
CSP in Practice: Timed Verification of Robot Software.
Speaker:
Matt Windsor
10th
of August 2022, 10h30, Online
Abstract: This talk describes work done by myself and the RoboStar team in York to tack...
Abstract: This talk describes work done by myself and the RoboStar team in York to tackle the verification of timed properties of robotic control software. We reduce the problem into one of concurrency reasoning, where Communicating Sequential Processes is the underlying formalism. On top of CSP, we build domain-specific languages that present specifications and implementation models in a manner that is both approachable to robotics experts and suitable for use in other ways (simulation model extraction, code generation, other formalisms, etc.). I discuss RoboChart, RoboStar's DSL for software models, and RoboCert, a DSL I am working on to handle specifications.
-
[CANCELLED] Mixed Signals: audio and wearable data analysis for health diagnostics
Speaker:
Cecilia Mascolo
22nd
of June 2022, 13h30, Online
Abstract: Wearable and mobile devices are very good proxies for human behaviour. Yet, m...
Abstract: Wearable and mobile devices are very good proxies for human behaviour. Yet, making the inference from the raw sensor data to individuals’ behaviour remains difficult. The list of challenges is very long: from collecting the right data and using the right sensor, respecting resource constraints, identifying the right analysis techniques, labelling the data, limiting privacy invasion, to dealing with heterogeneous data sources and adapting to changes in behaviour.
In this talk, I plan to reflect on these challenges and highlight the opportunities that mobile and wearable health systems are introducing for community, the developers as well as the users. I will use examples from my group's ongoing research on exploring machine learning and data analysis for health application in collaboration with epidemiologists and clinicians. In particular I will concentrate a part of the talk on an project focusing on leveraging audio signals from the human body to help automated diagnostics and disease progression analysis.
Bio: Cecilia Mascolo is the mother of a teenage daughter but also a Full Professor of Mobile Systems in the Department of Computer Science and Technology, University of Cambridge, UK. She is a director of the Centre for Mobile, Wearable System and Augmented Intelligence. She is also a Fellow of Jesus College Cambridge and the recipient of an ERC Advanced Research Grant. Prior joining Cambridge in 2008, she was a faculty member in the Department of Computer Science at University College London. She holds a PhD from the University of Bologna. Her research interests are in mobile systems and machine learning for mobile health. She has published in a number of top tier conferences and journals in the area and her investigator experience spans projects funded by Research Councils and industry. She has served as steering, organizing and programme committee member of mobile and sensor systems, data science and machine learning conferences. More details at www.cl.cam.ac.uk/users/cm542
-
Visual Specification of Properties for Robotic Designs
Speakers:
Waldeck Lindoso Jr., Sidney C. Nogueira, and Lucas Lima
9th
of March 2022, 10h30, Online
Abstract: RoboChart is a diagrammatic notation based on UML designed for modelling robo...
Abstract: RoboChart is a diagrammatic notation based on UML designed for modelling robotic software that has well-defined semantics in the notation of CSP process algebra, enabling the automatic proof of process refinements using the FDR tool. Although RoboChart allows the specification of the robot software, the definition of application-specific properties of RoboChart models must be specified using the CSP notation. Thus, the designer must be familiar with CSP to define and verify properties. This work proposes an approach for the automatic verification of properties using a diagrammatic notation that expresses the behaviour of RoboChart models. The approach proposes a diagrammatic notation based on UML activity diagrams that support the specification of behaviour mixing standard elements of the activity diagram with elements of RoboChart as events and operations. The diagram behaviour is formalised as a CSP process used to verify the properties of a RoboChart component. A plug-in for the Astah modelling tool has been developed to translate the diagram to CSP and call the FDR refinement checker, which verifies whether the RoboChart model refines the property specified with the proposed notation. Our proposed approach allows the designer to specify and verify properties of RoboChart models using diagrammatic notations with no knowledge of the underlying formal semantics.
-
From RoboSim to another CSP - CLEARSY Safety Platform [slides]
Speaker:
Thierry Lecomte
26th
of January 2022, 10h30, Online
Abstract: RoboSim is a diagrammatic language to model simulations of robotic systems to...
Abstract: RoboSim is a diagrammatic language to model simulations of robotic systems to define concurrent and distributed designs. In this presentation, we explore the use of the CLEARSY Safety Platform (https://lnkd.in/drwW_RDf) as a safety critical execution platform for these models. We draw the outline of a model-transformation strategy to translate RoboSim models into B models as supported by the CLEARSY Safety Platform. The transformation of several simple examples illustrate the preliminary results of this on-going joint research between CLEARSY and Metrópole Digital - IMD/UFRN.
-
Transforming RoboSim Models into UPPAAL
Speaker:
Mingzhuo Zhang
1st
of December 2021, 10h30, Online
Abstract: RoboSim is a tool-independent notation for modeling software simulations of r...
Abstract: RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this presentation, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.
-
The Pi-puck: a Raspberry Pi enhanced e-puck robot platform
Speaker:
Alan Millard
17th
of November 2021, 10h30, Online
Abstract: This talk will present the Pi-puck extension board - an interface between the...
Abstract: This talk will present the Pi-puck extension board - an interface between the e-puck robot and a Raspberry Pi single-board computer that enhances the robot's processing, sensing, and networking capabilities. This enhanced robot platform was designed specifically for swarm robotics research, but is also suitable for multi-robot and single-robot applications. The hardware was developed across multiple projects at the University of York, the final form of which is now commercially available. Software support for this hardware is currently being developed in collaboration with our international partners. This talk will highlight the main hardware features of the platform, and will detail the existing software ecosystem, including integration with the ARGoS and Webots robot simulators, as well as the Robot Operating System (ROS). Our aim is to allow robot control code to be prototyped in simulation and then deployed on physical hardware without modification. The talk will conclude with a discussion of future plans for the platform, and the research that it hopes to facilitate.
-
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
Speaker:
Simon Foster
19th
of May 2021, 10h30, Online
Abstract: Simulation and formal verification are important complementary techniques nec...
Abstract: Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for both activities. In this presentation we show how to apply Interaction Trees in Isabelle/HOL to produce a verification and simulation framework for state-rich process languages. We develop the core theory and verification techniques for Interaction Trees, use them to give a semantics to deterministic fragments of the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model. We also show how the Isabelle code generator can be used to generate verified executable simulations for reactive and concurrent programs. We hope in the future to apply this work in providing a route to formally verified animations of RoboChart/RoboSim models.
-
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
Speaker:
James Baxter
7th
of October 2020, 10h30, Online
Abstract: Lenses are a useful algebraic structure for giving a unifying semantics to pr...
Abstract: Lenses are a useful algebraic structure for giving a unifying semantics to program variables in a variety of store models, which support efficient automated proof in the Isabelle/UTP verification framework. In this presentation, we expand our lens library with (1) dynamic lenses, that support mutable indexed collections, such as arrays, and (2) symmetric lenses, that allow partitioning of a state space into disjoint local and global regions to support variable scopes. From this basis, we provide an enriched program model in Isabelle/UTP for collection variables and variable blocks that can support a variety of data structures and state spaces.
-
Towards an Isabelle EMF Meta-Model
Speakers:
Bestoon Hussien and Simon Foster
23rd
of September 2020, 10h30, Online
Abstract: Isabelle is both a proof assistant and a platform for developing verification...
Abstract: Isabelle is both a proof assistant and a platform for developing verification tools based on unification of mathematical theories of programming. It can be used to greatly improve software quality by automated formal analysis. However, Isabelle is out of reach for most software engineers, due to its steep learning curve. The aim of this work is to allow the integration of Isabelle into the software engineering lifecycle through integration with the EMF and Epsilon tool sets. We are developing a meta-model frontend to Isabelle's textual input language, Isar, which allows development of syntax and semantics for a variety of DSLs. This will allow us to bypass the need to write complex model-to-text transformations, and instead generate Isabelle through more straightforward model-to-model transformations. Our aim is to allow Isabelle-based verification tools to be accessed at the push of a button within Eclipse-based graphical tools, such as RoboTool. We demonstrate this with a model-to-model transformation from RoboChart to Isabelle/UTP.
-
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs
Speaker:
Brijesh Dongol
23rd
of January 2020, 14h30, CSE/102
Abstract: Teleo-Reactive (TR) robotic agent programs comprise sequences of guarded acti...
Abstract: Teleo-Reactive (TR) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a TR programmed robotic agent has a deductive Belief Store comprising constantly changing predicate logic percept facts, and knowledge facts and rules for querying the percepts. In this paper we introduce TR programming using a simple example expressed in the teleo-reactive programming language TeleoR, which is a syntactic extension of QuLog, a typed logic programming language used for the agent’s Belief Store. We give a formal definition of the regression property that rules of TeleoR procedures should satisfy, and an informal operational semantics of the evaluation of a TeleoR procedure call. We then formally express key features of the evaluation in LTL. Finally we show how this LTL formalisation can be used to prove that a procedure’s rules satisfy the regression property by proving it holds for one rule of the example TeleoR program. The proof requires us: to formally link a TeleoR agent’s percept beliefs with sensed configurations of the external environment; to link the agent’s robotic device action intentions with actual robot actions; to specify the eventual physical effects of the robot’s actions on the environment state.
-
From computer says no to robot says yes: engineering a positive future for robotics
Speaker:
Ana Cavalcanti
6th
of January 2020, 15h30, CSE/203
Abstract: With the prospect of sophisticated robots working ever more closely with huma...
Abstract: With the prospect of sophisticated robots working ever more closely with humans, it is vital that software engineers have the tools and techniques to ensure safety and reliability. Professor Ana Cavalcanti, a computer scientist whose research is changing the very language of robotic software development, is on a mission to ensure that, unlike the computer, the robot never says no: that it does the right thing at the right time, every time. To achieve this, Professor Cavalcanti and her team are developing a framework for the modelling and simulation of mobile and autonomous robots, bringing outdated software engineering practices, based on trial and error, into the state-of-the-art. Her vision is a 21st-century toolbox for robot-controller developers that will enable the safe application of socially beneficial robotics, allowing the UK to tap into a multibillion dollar global robotics market.
-
RoboChart & RoboTool: modelling and verification of probabilistic systems
Speaker:
Kangfeng Ye
15th
of October 2019, 12h30, CSE/202
Abstract: In addition to standard state machines and time primitives, RoboChart also su...
Abstract: In addition to standard state machines and time primitives, RoboChart also supports probabilistic choices, which allows us to model probabilistic systems in RoboChart. This seminar starts with an introduction of probability modelling in RoboChart using a robotic example. Then it will more focus on how to verify these systems in RoboTool by using PRISM, an existing probabilistic model checker. With recently designed probabilistic assertion language in RoboTool, users are able to use RoboTool even without knowledge of PRISM. However, for advanced users or complicated models, this seminar will give you some hints on how to flexibly use RoboTool and PRISM to verify the properties that are not easily verified by just clicking buttons on RoboTool.
-
A UTP theory for Hybrid Computation
Speaker:
Simon Foster
3rd
of October 2019, 16h00, CSE/202
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extend...
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid dynamical systems, supported by our mechanisation in Isabelle/UTP, which employs the HOL-Analysis and HOL-ODE packages for functional analysis. The hybrid relational calculus is built upon the same foundation as the UTP's theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise-continuous functions that we will describe. From this foundation, we give semantics to the core operators of the hybrid relational calculus, including ODEs and preemption, and show how the theory can be used to verify sequential hybrid systems. We also highlight our work in using the theory to give a denotational semantics to the Modelica language for hybrid dynamical systems modelling.
-
[CANCELLED] RoboChart & RoboTool: modelling and verification of probabilistic systems
Speaker:
Kangfeng Ye
1st
of October 2019, 12h30, CSE/102&103
Abstract: In addition to standard state machines and time primitives, RoboChart also su...
Abstract: In addition to standard state machines and time primitives, RoboChart also supports probabilistic choices, which allows us to model probabilistic systems in RoboChart. This seminar starts with an introduction of probability modelling in RoboChart using a robotic example. Then it will more focus on how to verify these systems in RoboTool by using PRISM, an existing probabilistic model checker. With recently designed probabilistic assertion language in RoboTool, users are able to use RoboTool even without knowledge of PRISM. However, for advanced users or complicated models, this seminar will give you some hints on how to flexibly use RoboTool and PRISM to verify the properties that are not easily verified by just clicking buttons on RoboTool.
-
Testing Robots using CSP
Speaker:
James Baxter
25th
of September 2019, 15h00, CSE/102
Abstract: We present a technique for automatic generation of tests for robotic systems ...
Abstract: We present a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the defini- tion of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock- CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to gen- erate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.
-
CANCELLED - Testing Robots using CSP
Speaker:
James Baxter
18th
of September 2019, 15h00, CSE/203
Abstract: We present a technique for automatic generation of tests for robotic systems ...
Abstract: We present a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the defini- tion of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock- CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to gen- erate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.
-
Foundational end-to-end verification of cyber-physical systems: The VeriPhy pipeline and its Applications
Speaker:
Brandon Bohrer
17th
of July 2019, 11h30, PZA/016
Abstract: We first present VeriPhy, a verified pipeline which automatically transforms ...
Abstract: We first present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end as it bridges abstraction gaps, including:
1) the gap between mathematical reals in physical models and machine arithmetic in the implementation,
2) the gap between real physics and its differential-equation models, and
3) the gap between nondeterministic controller models and machine code.
VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle. To minimize the trusted base, we cross-verify the KeYmaera X prover core in Isabelle.
We discuss two practical case studies applying VeriPhy to ground robots:
1) the initial study, tested on commodity hardware, uses a robot moving in a simple straight-line pattern,
2) a follow-up study gives a realistic model for general free-range 2D driving by following a series of arcs and was implemented in AirSim's realistic autonomous driving simulation.
-
Risk Structures: Towards Engineering Risk-aware Autonomous Robots
Speaker:
Mario Gleirscher
16th
of April 2019, 16h00, CSE/202
Abstract: To achieve acceptable safety, autonomous robots will have to reduce risk by i...
Abstract: To achieve acceptable safety, autonomous robots will have to reduce risk by incorporating autonomous risk handling mechanisms that enhance their mission controllers. The missing fallback to local or remote human operators as well as complex operational environments pose hard challenges to the engineering of appropriate risk handlers, particularly, to the hazard analysis and risk modelling activities leading to such handling mechanisms. This talk will give a brief introduction to risk analysis and modelling for risk-aware robots. Then, it will present a framework and method for the step-wise development of risk handling mechanisms. Last, it will illustrate how these mechanisms can be used in controllers of such robots.
-
CANCELLED - A UTP theory for Hybrid Computation
Speaker:
Simon Foster
9th
of April 2019, 12h30, CSE/202
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extend...
Abstract: In this talk I will describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid dynamical systems, supported by our mechanisation in Isabelle/UTP, which employs the HOL-Analysis and HOL-ODE packages for functional analysis. The hybrid relational calculus is built upon the same foundation as the UTP's theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise-continuous functions that we will describe. From this foundation, we give semantics to the core operators of the hybrid relational calculus, including ODEs and preemption, and show how the theory can be used to verify sequential hybrid systems. We also highlight our work in using the theory to give a denotational semantics to the Modelica language for hybrid dynamical systems modelling.
-
Orca: a functional correctness verifier based on Isabelle/UTP
Speaker:
Yakoub Nemouchi
26th
of February 2019, 12h30, CSE/203
Abstract: We present Orca, a functional correctness verifier based on Isabelle/UTP. A n...
Abstract: We present Orca, a functional correctness verifier based on Isabelle/UTP. A novelty of Orca is the ability to tackle a variety of language aspects at the semantic level by leveraging the semantics combination facilities of Hoare and He’s Unifying Theories of Programming. This supports genericity by allowing application of the underlying verification theorems to various languages. Orca comes with a set of Isabelle/HOL rules for Hoare Logic and laws of programming for the standard programming operators as well as non-trivial rules for modular reasoning. Orca extends isar to offer a nice front-end for parsing programs with a C-like syntax. Automatic reasoning is supported via Orca's backend which consists of a verification condition generator (VCG) and a parallel version of sledgehammer. The VCG is equipped with Hoare rules for forward reasoning to automatically compute the strongest postcondition(SP) and backward reasoning to automatically compute the weakest precondition (WP). Orca's VCG comes with two modes, the first mode is proof annotation where loop invariants are annotated interactively during the proof. The second mode of the VCG assumes that the program is already annotated with invariants.
-
Epistemic and Temporal Epistemic Logics of Authentication [slides]
Speaker:
Sharar Ahmadi
12th
of February 2019, 12h30, CSE/203
Abstract: The authentication properties of a security protocol are specified based on t...
Abstract: The authentication properties of a security protocol are specified based on the knowledge gained by the principals that exchange messages with respect to the steps of that protocol. As there are many successful attacks on authentication protocols, different formal systems, in particular epistemic and temporal epistemic logics, have been developed for analysing such protocols. However, such logics may fail to detect some attacks. To promote the specification and verification power of these logics, researchers try to construct them in such a way that they preserve some properties such as soundness, completeness, being omniscience-free, or expressiveness. The aim of this talk is to provide an overview of the epistemic and temporal epistemic logics of authentication.
-
Reasoning in tock-CSP with FDR
Speaker:
Pedro Ribeiro
30th
of January 2019, 12h30, PZA/022 (Piazza Building)
Abstract: Specifying budgets and deadlines using a process algebra like CSP requires an...
Abstract: Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The dialect tock-CSP embeds a rich and flexible approach for modelling discrete timed behaviours with powerful tool support using the CSP model checker FDR. Analysis, however, has traditionally used the standard semantics of CSP, which is inadequate for reasoning about timed refinement. Previous approaches have focused on traces refinement only or not considered the role of deadlines. The most recent version of FDR provides support for tock-CSP, including specific operators. For instance, to ensure maximal progress internal events can be prioritised over tock using a prioritise operator, whose denotational semantics is given in the finite-linear model. It remains, however, that the standard semantics of CSP is inadequate. In this talk we present an alternative semantic model for tock-CSP that encompasses a definition for prioritise. To enable the use of FDR to reason using this model, we use an encoding of refusals via traces. For validation, and to obtain a suitable definition for prioritise in tock-CSP, we establish a stepwise Galois connection with the finite-linear model. Our results have been mechanised using the proof assistant Isabelle/HOL.
-
RoboChart & RoboSim: modelling robots and collections [slides]
Speaker:
Alvaro Miyazawa
23rd
of January 2019, 12h30, CSE/203
