ALICE: An Advanced Logic for Interactive Component Engineering

11 years 12 months ago
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.
Borislav Gajanovic, Bernhard Rumpe
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Borislav Gajanovic, Bernhard Rumpe
Comments (0)