Formally verified simulations of state-rich processes using interaction trees in Isabelle/HOL
Simulation and formal verification are important complementary techniques necessary in
high assurance model-based systems development. In order to support coherent results, it is …
high assurance model-based systems development. In order to support coherent results, it is …
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
Model execution allows us to prototype and analyse software engineering models by
stepping through their possible behaviours, using techniques like animation and simulation …
stepping through their possible behaviours, using techniques like animation and simulation …
Without Loss of Satisfaction
MJH Heule - International Colloquium on Theoretical Aspects of …, 2023 - Springer
The success of automated reasoning presents us with an interesting peculiarity: while
modern solving tools can handle gigantic real-world instances, they often fail miserably on …
modern solving tools can handle gigantic real-world instances, they often fail miserably on …
UTP, Circus, and Isabelle
We dedicate this paper with great respect and friendship to He Jifeng on the occasion of his
80th birthday. Our research group owes much to him. The authors have over 150 …
80th birthday. Our research group owes much to him. The authors have over 150 …
Timed concurrent system modeling and verification of home care plan.
A home care plan (HCP) can be integrated with an electronic medical records (EMR)
system, serving as an example of a real-time system with concurrent processes. To ensure …
system, serving as an example of a real-time system with concurrent processes. To ensure …
Modelling and Verifying Robotic Software that Uses Neural Networks
Z Attala, A Cavalcanti, J Woodcock - International Colloquium on …, 2023 - Springer
Verifying learning robotic systems is challenging. Existing techniques and tools for
verification of an artificial neural network (ANN) are concerned with component-level …
verification of an artificial neural network (ANN) are concerned with component-level …
Model-Based Engineering for Robotics with RoboChart and RoboTool
Use of simulation to support the design of software for robotic systems is pervasive.
Typically, roboticists draw a state machine using an informal notation (not precise or …
Typically, roboticists draw a state machine using an informal notation (not precise or …
Formally Verified ZTA Requirements for OT/ICS Environments with Isabelle/HOL
The clean energy transformation includes the integration of distributed energy resources
with the power grid, which has led to a substantial increase in the complexity of power grids …
with the power grid, which has led to a substantial increase in the complexity of power grids …
Formally Verified ZTA Requirements
The clean energy transformation includes the integration of distributed energy resources
with the power grid, which has led to a substantial increase in the complexity of power grids …
with the power grid, which has led to a substantial increase in the complexity of power grids …
Verification of RoboChart Models with Neural Network Components
Z Attala - 2023 - etheses.whiterose.ac.uk
Current software engineering frameworks for robotics treat artificial neural networks (ANNs)
components as black boxes, and existing white-box techniques consider either component …
components as black boxes, and existing white-box techniques consider either component …