ALICE: An Advanced Logic for Interactive Component Engineering
It addresses the problem of formal verification for distributed systems using a stream-processing paradigm, but appears incremental as it builds on existing theorem prover technology.
The paper presents ALICE, a verification framework based on the Isabelle theorem prover, designed for specifying and verifying software or hardware components as stateful black-boxes with asynchronous message channels, supporting various specification styles for distributed systems.
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.