ALICE: An Advanced Logic for Interactive Component Engineering
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.
Cite
@article{arxiv.1410.4381,
title = {ALICE: An Advanced Logic for Interactive Component Engineering},
author = {Borislav Gajanovic and Bernhard Rumpe},
journal= {arXiv preprint arXiv:1410.4381},
year = {2014}
}
Comments
15 pages, 2 figures, 3 tables, Bernhard Beckert (Ed.) 4th International Verification Workshop (Verify'07). Proceedings, Bremen, July 2007