
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.

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 stateoftheart. Her vision is a 21stcentury toolbox for robotcontroller 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 TeleoReactive Robotic Agent Programs
Speaker:
Brijesh Dongol
23rd
of January 2020, 14h30, CSE/102
Abstract: TeleoReactive (TR) robotic agent programs comprise sequences of guarded acti...
Abstract: TeleoReactive (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 teleoreactive 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 MetaModel
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 metamodel 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 modeltotext transformations, and instead generate Isabelle through more straightforward modeltomodel transformations. Our aim is to allow Isabellebased verification tools to be accessed at the push of a button within Eclipsebased graphical tools, such as RoboTool. We demonstrate this with a modeltomodel 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.

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 MetaModel
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 metamodel 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 modeltotext transformations, and instead generate Isabelle through more straightforward modeltomodel transformations. Our aim is to allow Isabellebased verification tools to be accessed at the push of a button within Eclipsebased graphical tools, such as RoboTool. We demonstrate this with a modeltomodel transformation from RoboChart to Isabelle/UTP.

Temporal Logic Semantics for TeleoReactive Robotic Agent Programs
Speaker:
Brijesh Dongol
23rd
of January 2020, 14h30, CSE/102
Abstract: TeleoReactive (TR) robotic agent programs comprise sequences of guarded acti...
Abstract: TeleoReactive (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 teleoreactive 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 stateoftheart. Her vision is a 21stcentury toolbox for robotcontroller 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 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