This paper presents an overview of the veri cation 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 speci ed 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 speci cation are supported. Hence, ALICE is well suited for the formalization and veri cation of distributed systems modeled with this stream-processing paradigm.
1.1
As software-based systems take ever more and more responsibility in this world, correctness and validity of a software-based system is increasingly important. As the complexity of such systems is also steadily increasing, it becomes ever more complicated to ensure correctness. This especially concerns the area of distributed systems like bus systems in transportation vehicles, operating systems, telecommunication networks or business systems on the Internet. Expenses for verication are an order of magnitude higher than the expenses of the software testing up to now. This, on the one hand, will not change easily in the short run but it will also become evident that crucial parts of software need a dierent handling than less critical ones. So verication will go along with testing in the future. Full verication, however, will at least be used for critical protocols and components. To reduce verication expenses, a lot has been achieved in the area of theorem provers, like Isabelle [Pau03a, Pau03b, NPW02], in the last years. Based on these foundational works and on the increasing demand for powerful domain specic theories for such theorem provers, we have decided to realize ALICE as a stream-processing-oriented, formal framework for distributed, asynchronously communicating systems.
ALICE is a still growing framework within Isabelle for the verication of logically or physically distributed, interactive systems, where the concept of communication or message exchange plays a central role. An interactive system (see also [BS01] for a characterization) consists of a number of components with precisely dened interfaces. An interactive component interacts with its environment via asynchronous message sending and receiving over directed and typed communication channels. Each channel incorporates an implicit, unbounded buer that decouples the sending and arrival of messages, and thus describing asynchronous communication. In timed channels, we can control how long these messages remain in this implicit buer. Fig. 1 illustrates the graphical notation for the syntactical interface of a simple interactive component with one input and one output channel.
<Name> : <Type>
<Name> : <Type> <Name>
In ALICE message ow over channels is modeled by possibly innite sequences of messages called streams. Such a stream represents the observation of what happens on a channel over time. Since innite sequences are also included, the liveness and fairness properties of systems can also be dealt with. ALICE provides type constructors astream for building (untimed) streams and tastream for timed streams over arbitrary types.
As an advanced verication framework, ALICE will oer precisely formalized and comfortably usable concepts based on an underlying logic language called HOL [NPW02] as available in Isabelle. Using a well explored and rather expressive logic language allows us to build on an elaborated set of verication techniques for ALICE.
ALICE will provide support for a number of techniques to specify a component. A specication can be a relation between input and output streams, a stream-processing function, a mapping of input to output, or a set of streamprocessing functions allowing to describe non-determinism and underspecication. All variants can be timed or untimed. Further support will be given to map between these styles, allowing to choose appropriate specication techniques for each problem and integrating those later.
Although ALICE does already provide some of these features in its current version, this workshop paper also reports on work still to be done (for the previous version see [GR06]). In a future version ALICE will provide the following: A verication framework based on Isabelle supporting development methods for real time, distributed, asynchronously communicating and object oriented systems, respectively. This supports e.g. the development methodologies of [Rum96] and Focus [BS01]. A formal semantics framework for various languages based on stream-processing, e.g. UML’s composite structure diagrams that will be formalized based on streams [BCR06, BCR07a, BCR07b].
A sophisticated verication tool for distributed, interactive systems or, at least, their communication protocols based on stream-processing (see [Ste97] for a survey of stream-processing).
In the following we give a compact overview of Isabelle’s HOL and HOLCF that acts as a reminder for experts of the eld. An introduction can be found in [NPW02, Reg94] before we start describing features of ALICE in Section 2 and demonstrating the use of ALICE in Section 3 on the Alternating Bit Protocol. Section 4 concludes the paper with a discussion. 1.2
HOL Isabelle is a generic theorem prover, hence, it can be instantiated with object logics and appropriate proof tactics. Isabelle/HOL [NPW02], in short HOL, is such an elaborated higher order logic, dealing amongst others with sets, relations, total functions, natural numbers, and induction.
HOL provides a term syntax close to mathematical syntax and constructs from functional languages. It also provides basic types like bool or nat. For building sets over arbitrary types, HOL provides the type constructor set. Function types are built with the inx type constructor ⇒ for total functions. To build more complex types, the mentioned, and a number of additional basic types and type constructors are provided.
HOL inherits the type system of Isabelle’s metalogic including its automatic type inference for variables. There are two kinds of implication: the implication on the level of object logic, in this case HOL, symbolized by −→, and the symbol =⇒ for Isabelle’s inference. Analogously, there is an object logics symbol for the equality, in this case =, and the metalogics symbol ≡ for the denitional equality.
In Isabelle assumptions of an inference rule are enclosed in [ ] and separated by ;. The metalogics universal quantier is symbolized by V. 1.3
Isabelle/HOLCF [Reg94, MNvOS99], shortly HOLCF, is a conservative extension of HOL with domain theoretical concepts, such as chains, continuity, admissibility, xpoint recursion and induction, as well as some basic types and datatypes e.g. for lazy lists.
HOLCF extends HOL with the central type class pcpo for pointed complete partial orders. Any type that is a member of this type class features a special relation symbol v for a partial order on its elements, the least element symbolized by ⊥, and the existence of the least upper bound for any chain of its elements with respect to v.
This extension is carried out in layers of theories, beginning with the denition of type class po for partial orders. po is extended to type class cpo, where the existence of the least upper bound for any chain, symbolized by F i. Y i, is introduced. Here, Y is a chain of growing elements and i the index over natural numbers. Based on these theories, monotonicity and continuity for HOL functions on cpo types is formalized.
Type class pcpo nally introduces the existence of the least element in its members. We call the members of this class HOLCF types. Subsequently, HOLCF provides the new inx type constructor → for the construction of continuous functions on HOLCF types. Analogously to the HOLCF types, we call these functions HOLCF functions or operations. These functions, by denition, exhibit the advantages of continuous functions, such as composability, implementability etc. A lambda-abstraction, denoted by Λ (not to confuse with HOL’s λ) and a corresponding function application, using the symbol · (opposite to HOL’s white space) is provided accordingly.
Subsequently, the xpoint theory Fix mainly implements a continuous xpoint operator, symbolized by fix, and the xpoint induction principle. Hence, with →, fix, and HOLCF datatypes a complete HOLCF syntax for dening and reasoning about HOLCF functions and types is provided, which is separate from HOL’s function space. As an advantage, by construction, HOLCF function abstraction and application remains in the HOLCF world. 1.4
A good outline on dierent approaches to formalize possibly innite sequences in theorem provers like Isabelle or PVS, as well as a detailed comparison can be found in [DGM97, Ml98]. In contrast to a HOLCF formalization given in [Ml98], where nite, partial, and innite sequences are dened to model traces of I/O-Automata, our streams have been developed using only partial sequences and their innite completions, which are more appropriate for modeling interactive systems as these are generally non-terminating. A pure HOL approach based on coinduction and corecursion is described in [Pau97].
Another approach is the formal specication language ANDL introduced in [SS95]. ANDL is a formalization of a subset of Focus with an untimed syntax and a xed and an untimed semantics. Currently, ANDL does not provide an appropriate verication infrastructure or extended sophisticated denition principles, but it is HOLCF oriented. In [SM97] ANDL is used as interface for an A/C renement calculus for Focus in HOLCF. In [Hin98] ANDL is extended to deal with time.
A recent work in this area is [Spi06], where a pure HOL approach to formalize timed Focus streams is used. By this approach (see also [DGM97, Ml98]), an innite stream is represented by a higher-order function from natural numbers to a set of messages. Furthermore a time-driven approach, as it will briey be mentioned in Section 2.4, has been chosen there.
Apart from our idea of building such a logical framework, the realization of ALICE is based on a rudimentary formalization of Focus streams in HOLCF, developed by D. von Oheimb, F. Regensburger, and B. Gajanovic (the session HOLCF/FOCUS in Isabelle’s release Isabelle2005), a concise depiction of HOLCF in [MNvOS99], as well as on the conclusions from [DGM97, SM97]. It is elaborately explained in [GR06]. Additionally, it is worth mentioning that, in the current version HOL’s construct typedef has been used to dene astream. 2
The newly dened logic ALICE includes the following parts:
HOL/HOLCF - all theories from HOLCF, like Pcpo, Cont, etc. that are used on the interface between HOL and HOLCF (as discussed in Section 1.3). HOLCF - using HOLCF application/abstraction (LCF sublanguage) only. ALICE - basic type constructors astream and tastream, as well as recursion, pattern-matching, automata, etc.
ALICE - lemmas provided by ALICE theories (they are generally partitioned in timed and untimed properties).
Please note that, for the development of ALICE, we use a combination of HOL and HOLCF syntax, but the user of ALICE does not need to. This is due to the fact that we internally use HOLCF to build up necessary types, operators, and proving techniques, but will encapsulate these as much as possible. 2.1
To understand ALICE in more detail, we rst summarize its basic features. ALICE provides: polymorphic type constructors astream and tastream for timed and untimed streams over arbitrary HOL types, sophisticated denition principles for streams and functions over streams, such as pattern-matching, recursion, and state-based denition techniques, incorporated domain theory (concepts of approximation and recursion), various proof principles for streams, incorporated automata constructs for state-based modeling, also supporting underspecication or non-determinism, extensive theories for handling timed streams, functions and properties, a powerful simplier (while developing ALICE, a proper set of simplication rules has been dened carefully in such a way as to be used by ALICE automatically), and an extensive library of functions on streams and theorems, as well as commonly needed types (just like in any other programming language, a good infrastructure makes a language user friendly).
The following sections provide brief insights in the above listed features. For a deeper understanding we refer to [GR06]. 2.2
ALICE provides a basic type constructor called astream for specifying untimed streams. For any Isabelle type t, the type t astream is member of the HOLCF type class pcpo as described in Section 1.3. The following exhaustion rule describes the basic structure of untimed streams as well as the fundamental operators for their construction: Vs. s = ε ∨ ( ∃ h rs. s = <h> _rs) A stream s is either empty, symbolized by ε, or there is a rst message h and a remaining stream rs so that pre-pending h to rs yields the stream s. The operator <.> builds single element streams and . _. denes the concatenation on streams. It is associative and continuous in its second argument and has the empty stream (ε) as a neutral element. If the rst argument of concatenation is innite, the second is irrelevant and the rst is also the result of the concatenation. This eectively means that the messages of the second stream then never appear in the observation at all.
According to the above rules, ALICE also oers selection functions, named aft for the head and art for the rest of a stream, respectively. Function atake allows us to select the rst n symbols from a stream. Function adrop acts as a counterpart of atake as it drops the rst n messages from the beginning of a stream s. The operator anth yields for a number n and a stream s, the n-th message. Beyond that, ALICE provides many other auxiliary functions, e.g. # for the length of a stream, yielding ∞ for innite streams, aflatten for the attening of streams of streams, aipower for the innite repetition, afilter for message ltering. In Section 2.5 we give a tabular review of operators that are available in the current version of ALICE.
Since streams are HOLCF datatypes, they carry a partial order (see also Section 1.3), which is described by the following lemma s1 v s2 =⇒ ∃ t. s1 _t = s2 The above rule characterizes the prex ordering on streams. It is induced by a at order on the messages, disregarding any internal structure of the messages themselves. Based on these operators, a larger number of lemmas is provided to deal with stream specications, like case analysis, unfolding rules, composition rules, associativity, injectivity, and idempotency. Some foundational lemmas are given in Tab. 1. Built on the untimed case, ALICE provides another type constructor called tastream for specifying timed streams. Structurally, both are rather similar. Again, for any Isabelle type t, the type t tastream is a member of pcpo. The following exhaustion rule describes the basic structure of timed streams. It shows that timed streams may still be empty, contain a message or a tick as their rst element: Vts. ts = ε ∨ ( ∃ z. ts = < √> _z) ∨ ( ∃ m z. ts = <Msg m> _z) In addition to ordinary messages, we use a special message √, called the tick, to model time progress. Each √ stands for the end of a time frame. To dierentiate between the tick and ordinary messages, we use the constructor Msg as shown above. This operator is introduced by type constructor addTick that extends any type with the tick.
Please note that any timed stream of type t tastream is also an ordinary stream of type (t addTick) astream. Therefore, all machinery for astream types is available.
In addition, ALICE provides a timed take function. ttake n ·s yields at most n time frames from the beginning of a timed stream s.
To allow inductive denitions, tastream streams may be empty. However, for specications we restrict ourselves to observations over innite time, which means that we will only use the subset of timed streams with innitely many ticks. Therefore, additional machinery is necessary to deal with those. For example, the predicate timeComplete is provided to check whether a stream contains innitely many time frames.
For an integration of both stream classes, operator timeAbs maps a timed stream into an untimed one, just keeping the messages, but removing any time information. 2.4
Having the necessary types and type classes as well as auxiliary functions and lemmas at hand, we can introduce proof principles for streams now. At rst, we handle the untimed case, as the timed case can be built on that. Proof Principles for Untimed Streams. A rather fundamental proof principle for untimed streams is the so called take-lemma for streams that gives us an inductive technique for proving equality ( ∀ n. atake n ·x = atake n ·y) =⇒ x = y Two streams are equal if all nite prexes of the same length of the streams are equal. More sophisticated proof principles, like pointwise comparison of two streams using the operator anth or the below given induction principles are built on the take-lemma. The following is an induction principle for proving a property P over nite (indicated by the constructor Fin) streams [[#x = Fin n; P ε; Va s. P s =⇒ P (<a> _s) ]] =⇒ P x As said, when necessary, we base our proof principles directly on HOLCF but try to avoid their extensive exposure. Here is a principle that uses admissibility from HOLCF (adm) for predicates to span validity to innite streams (see [Reg94]) [[adm P; P ε; Va s. P s =⇒ P (<a> _s) ]] =⇒ P x The above induction principles have also been extended to the general use of concatenation, where not only single element streams, but arbitrary streams can be concatenated.
The concept of approximation (provided by HOLCF) and induction on natural numbers can also be used to prove properties involving continuous functions over streams as discussed in Section 2.5.
Proof Principles for Timed Streams. Since timed streams can also be seen as normal untimed streams, the above given proof principles can also be used to prove properties of timed streams.
Please note that we have taken a message driven approach to inductively dene timed streams. Messages are added individually to extend a stream. This also leads to event driven specication techniques. In the contrary, it would have been possible to model timed streams inductively as a stream (t list) astream, where each list denotes the nite list of messages of type t occurring in one time frame. This denition would lead to time-driven specication principles. It is up to further investigation to understand and integrate both approaches. As a rst step in this direction, ALICE provides a timed-take-lemma for timed streams arguing that streams are equal if they are within rst n time frames for each n, as given in the following. ( ∀ n. ttake n ·x = ttake n ·y) =⇒ x = y ( ∀ n. tframe n ·x = tframe n ·y) =⇒ x = y Analogously, the following proof principle is based on time frame comparison ALICE provides more sophisticated proof principles for timed streams, but also for special cases of timed streams, such as time-synchronous streams, containing exactly one message per time unit, and the already mentioned time complete streams, containing innitely many time frames. 2.5
Specifying streams allows us to dene observations on communication channels. However, ALICE focusses on specication of components communicating over those channels. The behavior of a component is generally modeled as function over streams and is often dened recursively or even state-based.
A recursively dened function f processes a prex of its input stream s by producing a piece of the output stream and continues to process the remaining part of s recursively. All functions dened in this specication style are per construction correct behaviors for distributed components. This makes such a specication style rather helpful. Functions of this kind are dened in their simplest form as illustrated in the following (using the function out to process the message x appropriately) f (<x> _s) = (out x) _(f s) By construction, these functions are monotonic and continuous (lub-preserving, see below) wrt. their inputs, which allows us to dene a number of proof principles on functions.
A number of predened auxiliary operators assist in specifying components. Due to expressiveness, we also allow to use operators that are not monotonic or continuous in some arguments, such as _ in its rst argument or aipower. In ALICE, it is also possible to dene more such functions using pattern-matching and recursion. The above notions can also be found in standard literature on semantics like [Win93]. In the following we concentrate on continuous functions. Continuous Functions - The Approximation Principle. As briey discussed, continuous functions capture the notion of computability in interactive systems and therefore play a prominent role in stream-processing specication techniques. The behavior of a continuous function for an innite input can be predicted by the behavior for the nite parts of the input. Thus, its behavior can be approximated. As it has been shown amongst others in [Win93], composition of continuous functions results in continuous functions. Therefore, based on a number of basic functions and equipped with appropriate denition techniques, it becomes easy to specify further functions. ALICE provides amongst others pattern-matching and recursion (like in functional languages), state-based denitions (using I/O ∗-automata [Rum96], see Section 2.6), xpoint recursion (using HOLCF), and continuous function-chain construction (using HOL’s primrec and approximation, see [GR06]) Currently, we do have at least the operators on streams depicted in Tab. 2 and Tab. 3 available. For the sake of brevity, we do not explain those further, but refer to [GR06] as well as Section 2.2 and 2.3 and furthermore assume that readers will recognize the functionality through name and signature. Operator Signature timeComplete ’a tastream ⇒ bool timeSync ’a tastream ⇒ bool injectTicks nat astream → ’a astream → ’a tastream timeAbs ’a tastream → ’a astream ttake nat ⇒ ’a tastream → ’a tastream tframe nat ⇒ ’a tastream → ’a astream stretchTimeFrame nat ⇒ ’a tastream → ’a tastream getTime nat ⇒ ’a tastream ⇒ nat 2.6
There is quite a number of variants of state machines available that allow for a state-based description. We use I/O ∗-automata that do have transitions with one occurring message (event) as input and a sequence of messages (events) as output (hence I/O∗). They have been dened in [Rum96] together with a formal semantics based on streams and a number of renement techniques. In contrast to I/O automata [LT89], they couple incoming event and reaction and need no intermediate states.
As they are perfectly suited for a state-based description of component behavior, we provide assistance for the denition of an I/O ∗-automaton A in ALICE by modeling the abstract syntax as a 5-tuple in form of A = (stateSet A, inCharSet A, outCharSet A, delta A, initSet A) Automata of this structure can be dened using the type constructor ioa. I/O∗automata consist of types for its states, input and output messages. delta denotes the transition relation of an automaton. It consists of tuples of source state, input message, destination state and a sequence of output messages. The 5th element initSet describes start states and possible initial output (that is not a reaction to any incoming message).
As an illustration, we dene 1 an I/O∗-automaton representing a component dealing with auctions in the American style, where bidders spontaneously and repeatedly spend money and after a certain (previously unknown) timeout the last spender gets the auctioned artifact. The auction component is initialized with an arbitrary but a non-zero timeout. It counts down using the ticks and stores the last bidder as he will be the winner.
amiauction :: "((nat * Bid * IAP), Bid addTick, BidUclosed addTick) ioa" amiauction_def: "amiauction ≡ (UNIV, UNIV, UNIV, {t. ∃ k b m x.
(* handle time and accept the last bid
as soon as the time limit is reached *) t = ((k+1,b,x), √, (k,b,x), < √>) ∧ k > 0 ∨ t = ((0,b,x), √, (0,b,x), < √> _<Msg closed>) ∨ tt == ((((11,,bb,,IA)),, √√,, ((00,,bb,,IA)),, << √√>> __<<MMssgg (calcocseepdt>)b)∨> _<Msg closed>) ∨ (* store the new bid m if necessary *) t = ((k+1,b,x), Msg m, (k+1,m,A), ε) ∨ t = ((0,b,x), Msg m, (0,b,x), ε)}, {(( s. fst s > 0 ∧ snd (snd s) = I), ε)})" The above automaton is well-dened, deterministic and complete. By applying the operator ioafp, we map this automaton into a function that is continuous by construction. The recursive denition of a stream-processing function is now embedded in the ioafp operator, leaving a non-recursive but explicit denition of the actual behavior in an event based style.
In fact, a number of proof principles are established on these state machines that do not need inductive proof anymore, but just need to compare transitions and states. More precisely, the behaviors can then be compared by establishing a (bi-)simulation relation between the automata.
A non-deterministic I/O ∗-automaton is dened in an analogous form and not mapped to a single but a set of stream-processing functions. This is especially suitable to deal with underspecication.
As said, ALICE is still in development. Although we have initial results on this kind of specication style, we will further elaborate ALICE to comfortably deal with I/O∗-automata of this kind in the future. 1 Due to lack of space, we skip HOL’s keyword constdefs in front of a de nition but symbolize it by indentation. We also do not introduce the necessary type declarations, which is actually straightforward for the speci cations used here.
Based on the theory introduced so far, we show the usefulness of ALICE by developing a small, yet not trivial and well known example.
The Alternating Bit Protocol (ABP) is a raw transmission protocol for data over an unreliable medium. Goal of the ABP is to transmit data over a medium that looses some messages, but does not create, modify, rearrange or replicate them. The key idea is that the sender adds an identier to each message that is being sent back as acknowledgement by the receiver. If the acknowledgement does not arrive, the sender sends the same message again. When only one single message is in transmission, the identier can boil down to a single bit with alternating value hence the name of the protocol.
The ABP specication involves a number of typical issues, such as underspecication, unbounded non-determinism and fairness. Fig. 2 illustrates the overall structure of the ABP. A detailed explanation of a similar specication can be found in [BS01].
as : Bit ar : Bit i : Data
Sender
Receiver
o : Data Medium
(Bit) Medium (Data x Bit) ds : Data x Bit
dr : Data x Bit Please note that the medium is modeled after the existing, real world, while sender and receiver need to be specied and later implemented in such a way that they can safely deal with the given medium. So, we rst specify the behavior of the medium as described above.
Med_def: "Med x y ≡ ∃ p. #(afilter {True} ·p) = ∞ ∧
y = apro1 ·(afilter {a. ∃ b. a = (b, True)} ·(azip ·x ·p))" Through the use of an internal oracle stream p, we can describe that a medium does eventually transmit a message if we retry long enough. The fairness, as described below, is deduced from the above specication as follows. [[#x = ∞; Med x y ]] =⇒ #y = ∞ The lemma is proven easily using the following auxiliary lemma, since the lengths of the rst and the second pointwise projection ( apro1 and apro2 respectively) of a stream consisting of ordered pairs are equal. ∀ x. #x = ∞ −→ apro2 ·(afilter {a. ∃ b. a = (b, z)} ·(azip ·x ·p)) = afilter {z} ·p The above auxiliary lemma is again proven by induction on the free stream variable p using an appropriate proof principle from Section 2.4. 3.2
Now, relative to a given medium, we have to dene a sender and a receiver that establish the desired behavior: safe transmission of messages. The sender receives data from outside and transmits them together with the alternating bit. We give a specication in a functional style:
Snd :: "Data astream ⇒ Bit astream ⇒ (Data * Bit) astream ⇒ bool" Snd_def: "Snd i as ds ≡ let in fas = aremstutter ·as; fb = apro2 ·(aremstutter ·ds); fds = apro1 ·(aremstutter ·ds) fds v i ∧ fas v fb ∧ aremstutter ·fb = fb ∧ #fds = imin #i (iSuc (#fas)) ∧ (#fas < #i −→ #ds = ∞)" We explicitly dene the channel observations for the sender in Fig. 2. The conjuncts in the in part of the denition constrain the sender in the order of their appearance, using the abbreviations from the let part, as follows 1. Abstracting from consecutive repetitions of a message via aremstutter, we see that the sender is sending the input messages in the order they arrive. 2. The sender also knows which acknowledgement bit it is waiting for, nevertheless, it is underspecied which acknowledgment bit is sent initially. 3. Each new element from the data input channel is assigned a bit dierent from the bit previously assigned. 4. When an acknowledgment is received, the next data element will eventually be transmitted, given that there are more data elements to transmit. 5. If a data element is never acknowledged then the sender never stops transmitting this data element. 3.3
The receiver sends each acknowledgment bit back to the sender via the acknowledgment medium and the received data messages to the data output channel removing consecutive repetitions, respectively.
Rcv :: "(Data * Bit) astream ⇒ Bit astream ⇒ Data astream ⇒ bool" Rcv_def: "Rcv dr ar o ≡ ar = apro2 ·dr ∧ o = apro1 ·(aremstutter ·dr)" 3.4
The overall system is composed as dened by the architecture in Fig. 2. This composition is straightforwardly to formulate in ALICE:
ABP_def: "ABP i o ≡ ∃ as ds dr ar. Snd i as ds ∧ Med ds dr ∧ Rcv dr ar o ∧ Med ar as" This formalization of the ABP uses a relational approach similar to the specication in [BS01]. However, formalizations as sets of functions or in a statebased manner are possible as well. Using a more elaborate version of ALICE, we will be able to dene a state-based version of sender and receiver (similar to [GGR06]), which is on the one hand more oriented towards implementation and on the other hand might be more useful for inductive proof on the behaviors. Most important however, we will be able to prove that this relational and the state-based specications will coincide.
For this case study, we remain in the relational style and specify the expected property of the overall system (without actually presenting the proof): ABP i o =⇒ o = i Please note that, at this stage of the development of ABP, there are neither realizability nor sophisticated timing constraints considered in the above formalization. Due to relational semantics, additional renement steps are then needed to reduce the underspecication towards an implementation oriented or timing-aware style, since there are innite streams fullling the specication that are not valid protocol histories. These, however, would not occur, when using sets of stream-processing functions as they impose continuity on the overall behavior. 4
In this paper we have introduced ALICE, an advanced logic for formal specication and verication of communication in distributed systems. ALICE is embedded in the higher order logic HOL, which itself is formalized using the Isabelle generic theorem prover.
Our approach is based on using HOLCF to deal with partiality, innity, recursion, and continuity. We provide techniques to use ALICE directly from HOL, thus preventing the user to actually deal with HOLCF specialities.
ALICE is currently under development. So not all concepts and theories presented here are already completely mature. Further investigations will also deal with the question of expressiveness, applicability and interoperability. Beyond the ABP, we already have some experience with other formalizations that show that the overhead of formalizing a specication in ALICE as apposed to a mere paper denition is not too bad. However, it also shows where to improve comfort. [BCR06] [BCR07b]