ALICE: An Advanced Logic for Interactive Component Engineering

TL;DR

ALICE is a verification framework based on Isabelle that models and verifies distributed systems using stream-based, asynchronous communication specifications, supporting various styles including timed, untimed, and state-based approaches.

Contribution

It introduces ALICE, a comprehensive framework for formalizing and verifying distributed components with diverse specification styles within Isabelle.

Findings

Supports multiple specification styles including timed and state-based

Enables formal verification of distributed systems modeled as stream-processing

Built on Isabelle for rigorous theorem proving

Abstract

This paper presents an overview of the verification framework ALICE in its current version 0.7. It is based on the generic theorem prover Isabelle [Pau03a]. Within ALICE a software or hardware component is specified as a state-full black-box with directed communication channels. Components send and receive asynchronous messages via these channels. The behavior of a component is generally described as a relation on the observations in form of streams of messages flowing over its input and output channels. Untimed and timed as well as state-based, recursive, relational, equational, assumption/guarantee, and functional styles of specification are supported. Hence, ALICE is well suited for the formalization and verification of distributed systems modeled with this stream-processing paradigm.