Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software

Ziggy Attala; Ana Lucia Caneca Cavalcanti; Simon David Foster; Fang Yan; Jim Woodcock

Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software

Ziggy Attala, Ana Lucia Caneca Cavalcanti^*, Simon David Foster^*, Fang Yan, Jim Woodcock^*

^*Corresponding author for this work

Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

Verification of robotic systems that use neural networks is a challenge. We focus on how we can verify robotic software modules where one or more of the controllers are implemented by a neural network. We present a formal technique supported by tools to model and verify control software involving neural networks. Our technique enables reasoning about the reactive, communication-based, properties of a system through a process-algebraic lens. We support our framework with a link to state-of-the-art ANN verification techniques, using them to prove contextual properties of a neural network. Our approach is flexible, platform-independent, and focuses on the logic of neural network models, instead of on a training method or specific use case.

Original language	English
Publication status	Accepted/In press - 17 Feb 2025
Event	The 17th NASA Formal Methods Symposium (NFM 2025) - William & Mary, Computer Science Department Williamsburg, Virginia, USA, Williamsburg, United States Duration: 11 Jun 2025 → 13 Jun 2025 https://shemesh.larc.nasa.gov/nfm2025/

Conference

Conference	The 17th NASA Formal Methods Symposium (NFM 2025)
Country/Territory	United States
City	Williamsburg
Period	11/06/25 → 13/06/25
Internet address	https://shemesh.larc.nasa.gov/nfm2025/

Keywords

verification
Circus
theorem proving
Isabelle
Marabou

Cite this

@conference{2e77511abccc49dfafd8c8a0fbe402a1,

title = "Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software",

abstract = "Verification of robotic systems that use neural networks is a challenge. We focus on how we can verify robotic software modules where one or more of the controllers are implemented by a neural network. We present a formal technique supported by tools to model and verify control software involving neural networks. Our technique enables reasoning about the reactive, communication-based, properties of a system through a process-algebraic lens. We support our framework with a link to state-of-the-art ANN verification techniques, using them to prove contextual properties of a neural network. Our approach is flexible, platform-independent, and focuses on the logic of neural network models, instead of on a training method or specific use case.",

keywords = "verification, Circus, theorem proving, Isabelle, Marabou",

author = "Ziggy Attala and Cavalcanti, {Ana Lucia Caneca} and Foster, {Simon David} and Fang Yan and Jim Woodcock",

year = "2025",

month = feb,

day = "17",

language = "English",

note = "The 17th NASA Formal Methods Symposium (NFM 2025)<br/> ; Conference date: 11-06-2025 Through 13-06-2025",

url = "https://shemesh.larc.nasa.gov/nfm2025/",

}

TY - CONF

T1 - Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software

AU - Attala, Ziggy

AU - Cavalcanti, Ana Lucia Caneca

AU - Foster, Simon David

AU - Yan, Fang

AU - Woodcock, Jim

PY - 2025/2/17

Y1 - 2025/2/17

N2 - Verification of robotic systems that use neural networks is a challenge. We focus on how we can verify robotic software modules where one or more of the controllers are implemented by a neural network. We present a formal technique supported by tools to model and verify control software involving neural networks. Our technique enables reasoning about the reactive, communication-based, properties of a system through a process-algebraic lens. We support our framework with a link to state-of-the-art ANN verification techniques, using them to prove contextual properties of a neural network. Our approach is flexible, platform-independent, and focuses on the logic of neural network models, instead of on a training method or specific use case.

AB - Verification of robotic systems that use neural networks is a challenge. We focus on how we can verify robotic software modules where one or more of the controllers are implemented by a neural network. We present a formal technique supported by tools to model and verify control software involving neural networks. Our technique enables reasoning about the reactive, communication-based, properties of a system through a process-algebraic lens. We support our framework with a link to state-of-the-art ANN verification techniques, using them to prove contextual properties of a neural network. Our approach is flexible, platform-independent, and focuses on the logic of neural network models, instead of on a training method or specific use case.

KW - verification

KW - Circus

KW - theorem proving

KW - Isabelle

KW - Marabou

M3 - Paper

T2 - The 17th NASA Formal Methods Symposium (NFM 2025)<br/>

Y2 - 11 June 2025 through 13 June 2025

ER -