ALICE: An Advanced Logic for Interactive Component Engineering

This paper presents an overview of the verication 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 specied 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 owing over its input and output channels. Untimed and timed as well as state-based, recursive, relational, equational, assumption/guarantee, and functional styles of specication are supported. Hence, ALICE is well suited for the formalization and verication of distributed systems modeled with this stream-processing paradigm.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Borislav Gajanovic, Bernhard Rumpe
• Keywords: Automated Reasoning, CADE 2007, Directed Communication Channels, Theorem Prover Isabelle, Verication Framework Alice