
RoboChart & RoboSim: modelling robots and collections [slides]
Speaker:
Alvaro Miyazawa
23rd
of January 2019, 12h30, CSE/203

Reasoning in tockCSP 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 tockCSP 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 tockCSP, 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 finitelinear model. It remains, however, that the standard semantics of CSP is inadequate. In this talk we present an alternative semantic model for tockCSP 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 tockCSP, we establish a stepwise Galois connection with the finitelinear 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 omnisciencefree, 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 nontrivial rules for modular reasoning. Orca extends isar to offer a nice frontend for parsing programs with a Clike 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 HOLAnalysis and HOLODE 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 piecewisecontinuous 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 Riskaware 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 riskaware robots. Then, it will present a framework and method for the stepwise development of risk handling mechanisms. Last, it will illustrate how these mechanisms can be used in controllers of such robots.

Foundational endtoend verification of cyberphysical 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 highlevel models of safetycritical cyberphysical systems (CPSs) in differential dynamic logic to verified controller executables. VeriPhy proves that all safety results are preserved endtoend 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 differentialequation 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 crossverify 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 straightline pattern,
2) a followup study gives a realistic model for general freerange 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 domainspecific notation called RoboChart. This is a UMLlike 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 discretetime 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 domainspecific notation called RoboChart. This is a UMLlike 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 discretetime 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 HOLAnalysis and HOLODE 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 piecewisecontinuous 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.

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 HOLAnalysis and HOLODE 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 piecewisecontinuous 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 domainspecific notation called RoboChart. This is a UMLlike 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 discretetime 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 domainspecific notation called RoboChart. This is a UMLlike 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 discretetime 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 endtoend verification of cyberphysical 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 highlevel models of safetycritical cyberphysical systems (CPSs) in differential dynamic logic to verified controller executables. VeriPhy proves that all safety results are preserved endtoend 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 differentialequation 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 crossverify 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 straightline pattern,
2) a followup study gives a realistic model for general freerange 2D driving by following a series of arcs and was implemented in AirSim's realistic autonomous driving simulation.

Risk Structures: Towards Engineering Riskaware 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 riskaware robots. Then, it will present a framework and method for the stepwise 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 HOLAnalysis and HOLODE 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 piecewisecontinuous 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 nontrivial rules for modular reasoning. Orca extends isar to offer a nice frontend for parsing programs with a Clike 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 omnisciencefree, or expressiveness. The aim of this talk is to provide an overview of the epistemic and temporal epistemic logics of authentication.

Reasoning in tockCSP 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 tockCSP 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 tockCSP, 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 finitelinear model. It remains, however, that the standard semantics of CSP is inadequate. In this talk we present an alternative semantic model for tockCSP 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 tockCSP, we establish a stepwise Galois connection with the finitelinear 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