Safety and security guarantees for individual applications in general depend on assumptions on the given context provided by distributed instances of operating systems, hardware platforms, and other application level programs that are executed on these platforms. The problem for formal approaches is to formalize these assumptions without having to look at the details of the (formal) model of the operating system (including the machines that execute applications). The work described in this paper presents a modular approach which uses histories of observable events to specify runs of distributed instances of the system. The overall verification approach decomposes the given verification problem into local tasks along the lines of assume-guarantee reasoning. In this paper we focus on this methodology and on its realization in the Verification Support Environment (VSE). We also illustrate the proposed approach with the help of a suitable example, namely the specification and verification of an SMTP server whose implementation makes extensive use of various system calls as e.g. fork and socket commands.
The theory developed in the following aims at a modular approach for the specification and verification of concurrent systems with heterogeneous components. Concurrency typically results from the actual parallel execution of independent systems and the abstraction from a concrete scheduler within the context of a given platform. Like the systems themselves their formal models will consist of various types of components specified by different types of state transition systems. In the composed (global) system the components interact with each other by certain communication mechanisms.
In this paper we consider an instantiation of the general approach which is
taken from the context of the Verisoft project where a pervasive formal model
of a distributed collection of hardware-software platforms with application level
programs running on each of these was established, [
Instead of verifying application level programs directly on the Verisoft model,
we propose to use traces of observable events that according to a given view are
attached to steps of computations (or runs) of the distributed system as they
have been formally defined in Verisoft. Since for a state in a run we collect all
events that have happened so far we call these (finite) lists of events histories.
The behavior of the global system as well as that of single components is then
specified by sets of histories thereby abstracting from the local state spaces of the
components. Like an input-output specification for a sequential piece of software
sets of histories describe the concurrent, typically non-terminating computation
of a global system or component thereof. Event traces defined by a certain view
on a given model provide an appropriate interface for an inductive analysis of
cryptographic protocols, [
Our approach is modular in the sense that the task of verifying a history
specification against runs of the global system can be decomposed into local
verification tasks for its components. Following the general assume-guarantee
approach, see [
Each history specification, possibly obtained by a combination of sub-specifications, has to be verified against all components of the overall model. Here we focus on the verification of C01 machines that execute (and give meaning to) C0 programs extended by external calls that allow to exchange information with the corresponding operating system and, via a network component, with C0 machines that run on different (remote) instances of the operating system. As an example we consider the implementation of an e-mail system consisting of an e-mail client, a (so-called) mail bag, a SMTP-server, and a SMTP-client.
In the next section we summarize the instantiation of the general approach by the Verisoft model of distributed systems. As a concrete example in section 3 we provide the specification of the SMTP server by a set of histories. In Section 4 we describe the verification of application-level C0 programs, like the implementation of the SMTP server, by means of a transformation to abstract sequential programs that replay and extend histories. Section 5 summarizes the described approach and outlines possible future work. 2 2.1
In the Verisoft project a formal model of an operating system was developed
and verified with respect to its implementation, [
In C0 there are besides others no side effects in expressions and pointers are strictly typed (see [
A model of a distributed system consists of instances of (the same) system and an abstract network component connecting them. Each system is identified by a unique network address na ∈ N a. It basically consists of two parts. The simple operating system provides resources like input-output devices, a file system, and sockets for the communication over the network component. A process is identified by a process identifier pid ∈ P id and the network address of the system instance it is running on. For each process given by p = mk proc(pid, na) a machine (interpreter) is part of the system na. In this paper we are interested in applications implemented in C0, the subset of C considered in Verisoft. Hence our processes represent abstract execution mechanisms where the program part of a configuration is a C0 program π.
From point of view of an application programmer the system context consists of all operating systems and the network connecting them. Hence we consider this complete context as a single component in our decomposition. It will be denoted by the constant SOS.
The view we have chosen is depicted in Figure 1. pid@na The communication between user programs and the surrounding operating sysos@na tem (instance) is by so called external calls.
Net External calls cext(τ¯ : z¯, res) take the same
syntax as ordinary function calls. We use τ¯ system-context as a sequence of value parameters and z¯, res as a sequence of return parameters. Typically the value of res will indicate success or failure. Whenever a system call is reached
Fig. 1. Verisoft Model during the computation of a process p the normal execution as given by the (small step) semantics RC0 ⊆ Conf × Conf is interrupted (stopped) and a request is sent to the corresponding operating system. With these steps of a global computation we associate events of the form mk ev(p, SOS, m) where the message m encodes the particular call given by cext and the values of the parameters (τ¯ : z¯) in mem′. For a call of socket read socket read(sid : length, buffer, ec) the corresponding message will by Sread(sid, length) where Sread is a constructor symbol for an abstract data type and sid, length are the values of the programming variables sid, length in mem′. They indicate the socket and the length of the string to be read.
To model the return of external calls the standard C0 machines have to be extended by steps where the resulting configuration is determined by an answer (message) from the corresponding operating system. The (answer) information intended for process p will be written to the return parameters (of the pending call). The event we associate with these steps is of the form mk ev(SOS, p, m) where the message m represents the return information. For example a successful call of socket read the message will be Succ sread(length, buf f er) where length indicates the elements in the fixed length array buf f er that have actually been read. These values uniquely determine the values of the result parameters after return of that external call. 2.2
Having defined events for all external calls (and also RPC calls) we may specify global system runs by a set (or unary predicate) H of finite sequences of events. A global System SOS(π0, , . . . , πn−1) consisting of arbitrary many instances of the operating system with arbitrary many C0-processes executing π0, , . . . , πn−1.
By SOS(π0, , . . . , πn−1) |= H we denote the fact that for each state in a global run of SOS(π0, , . . . , πn−1) the sequence of events that have happened so far satisfies H. Given an event e = mk ev(s, r, m) we say that s (the sender) is responsible for that event. In addition we define that e is relevant for s as well as the receiver r. By SOS(π0, , . . . , πn−1) ↓ i |= H we denote the fact that no process p executing πi ∈ {π0, , . . . , πn−1} violates H first, i.e. in a step p is responsible for. Similarly we use SOS(π0, , . . . , πn−1) ↓ SOS |= H for a projection to the operating systems themselves.
To establish SOS(π0, , . . . , πn−1) ↓ i |= H locally outside the context of a global system we transform πi into a program π˜i where the external calls manipulate histories. Altogether π˜i replays and possibly extends histories.
Using π˜i |= H for the fact that π˜i preserves H, soundness of this method (w.r.t. the verification of application level programs) is demonstrated by a kind of simulation theorem that allows to conclude that π˜i |= H ⇒ SOS(π0, , . . . , πn−1) ↓ i |= H holds. The simulation theorem is application independent and established by looking at the C0 execution mechanism. As opposed to that π˜i |= H is concerned with the verification of individual programs.
Before we present the specification of the SMTP-server and the verification technique given by the ˜-transformation we have to discuss special events that provide the binding between programs πi and processes in a given history. 2.3
Histories cover the whole life cycle of processes. This includes the association of process identifiers with the programs that are executed. This binding takes place upon creation of a new process. The lifetime of a process ends by an explicit termination event.
In the verification process we are interested in a particular program (text) π. To associate programs with process identifiers we assume a fixed enumeration of programs. In histories π = πi is then represented by the constant i.
Create events hSOS, p, Create(i)i are caused by the corresponding instance of the SOS while the identifier for the new process p = mk proc(na, pid) is considered as the recipient of the message indicating the program text πi to be executed starting with a fixed initial state.
Clone create events hSOS, p, Clone Create(p′, b)i are caused by the corresponding SOS as possible positive reaction to a call of fork. p = mk proc(na, pid) indicates the child process which continues to execute the program of the parent process given by p′ in the message. b ∈ {0, 1} is a flag indicating access to the terminal. The initial state of p is the state of p′ reached before execution of fork.
A process p (executing some πi) is terminated by exit or kill events. Exit events are caused by p while kill events are caused by the corresponding instance of the SOS.
A sub-history h0 of h is called a thread of p in h if there is exactly one create event for p in h0 which is the first event (in h0) relevant for p. The thread is called open if h0 does not contain a terminating event for p.
Now in defining π˜i |= H by a program π˜(i) that replays and (possibly) extends histories h we have to consider all threads in h that execute πi. Since a given specification H can only be violated if some h ∈ H is actually extended by π˜ we restrict ourselves to open threads executing πi. It is a simple observation that for each p there is at most one open thread in a given h. Therefore we provide a (guess of) p as an argument to the replay and extend procedure. If there is no open thread of p that executes πi, then the given history h is delivered unchanged as the result.
Open threads chosen in this way include those where a child p of p′ is created by an event hSOS, p, Clone Create(p′, b)i following a call of fork during the execution of πi. Since we have to know the correct internal state the replay and extend procedure has to start with the first ancestor p′′ of p. The computation of this process is initiated by a create event hSOS, p′′, Create(i)i .
In the start of the replay and extend procedure for πi as well as in the implementation of calls of fork we use the function anc(i, p, h) which computes the sequence of ancestor threads for a given p and h. In case there is no open thread of p in h executing πi anc(p, h) = []. For anc(p, h) = [h0, . . . , hn1], hn1 is the open thread of p in h with hSOS, p, Create(i)i or hSOS, p, Clone Create(p′, b)i as first event and h0 is the first ancestor thread with first element hSOS, p′′, Create(i)i. 3
As already mentioned earlier we considered a non-trivial example in the Verisoft context, namely the full implementation (in a C-like language) and the full specification (in terms of histories) of an SMTP-Server as part of an Simple Mail Transfer Scenario. All in all this implementation required about 7.500 lines of code.
The SMTP server listens for connections from SMTP clients. If a connection has been established, it spawns a child process, which inherits the socket granting access to that new connection. The child communicates with the remote SMTP client while obeying the so-called SMTP Protocol. In the meantime, the main SMTP server process listens again for new connections and spawns child processes to handle the session. This behaviour can be formalised by a step by step description of the main process and its child processes. For the formalisation we fix the constant SOS (Simple Operating System) representing the operating system. Any process – and thus the SOS as well – is determined by a network address (the host) and a process id on this host. We assume that – for a given process p – we can access the network address by get na(p).
For simplicity we make use of the following definitions: For every history h and process p we define h ↓ p as the projection of the history h on process p. I. e., () ↓ p = () (hs, r, mi ◦ h) ↓ p = hs, r, mi ◦ h ↓ p if s=p or r=p (hs, r, mi ◦ h) ↓ p = h ↓ p otherwise With h+ = {h′ ∈ Hist | h′ ↓ p = h} we can describe (for a given history h and an implicitly given process p) the set of histories whose projection on p is just h. Recall that we defined the binary operator ◦ on histories as the concatenation of its two arguments. In what follows we also use this operator for the ”concatenation” of two history sets: H1 ◦ H2 = {h1 ◦ h2 | h1 ∈ H1, h2 ∈ H2}.
The top-level specification (in terms of histories) of the SMTP-Server then looks as follows: we consider the prefix-closure of the set HSMT P Server(p) where HSMTP Server(p) = HINIT(p) ◦ HLOOP(p, sid) for some process p representing the SMTP-Server process and some socket id sid.
The history set HINIT(p) describes the initialization phase of the SMTP-Server. I. e., the SOS first creates the SMTP-process (represented by the message Create(SMTP Server , SOS, 1)). Then the newly created SMTP-process sends a message to the SOS that it wants a socket to be opened on port 25 (the standard SMTP-port). After the SOS successfully responds with a new socket id the SMTP-Server requests to listen to this new socket. The history set HINIT(p) is thus easily defined as
HINIT(p) = (hSOS, p, Create(SMTP Server , SOS, 1)i ◦ hp, SOS, Sopen(25)i ◦ hSOS, p, Succ sopen(sid)i ◦ hp, SOS, Slisten(sid)i ◦ hSOS, p, Succi)+ for a process p representing the SMTP-Server process and a socket id sid. The history set HLOOP(p, sid) is supposed to cover the parent process of the SMTPserver together with all the children processes that might be initiated. It is defined as the smallest set of histories that satisfies the equation HLOOP(p, sid) = (hp, SOS, Saccept(sid)i)+ ∪ (HACC(p, sid, sid′) ◦ HFORK CALL(p) ◦ ((HFORK ANS C(p′) ◦ HCHILD(p′, sid)) ∩ (HFORK ANS P(p) ◦ HCLOSE(p, sid′) ◦ HLOOP(p, sid)))) for some socket id sid′ 6= sid and some process p′ 6= p .
This history set HLOOP(p, sid) might require some more explanation. First the SMTP-Server issues a socket-accept command. This command might never be answered and thus the SMTP-Server might wait forever (first line in the definition of HLOOP(p, sid)). If, however, there is an answer to the accept-request (another process issued a corresponding connect-request) then the SMTP-Server calls a fork-command, thus producing a child of its own process. Now, both the SMTP-Server and its child run concurrently as indicated by the intersection of the two history sets in the last two lines of the HLOOP(p, sid) definition.
With this explanation the definition of the history sets HACC(p, sid, sid′), ′ HFORK(p), and HCLOSE(p, sid ) should be fairly obvious, namely HACC(p, sid, sid′) = (hp, SOS, Saccept (sid)ihSOS, p, Succ saccept (sid′, rna, rpn)i)+ for some remote network address rna and port number rpn HFORK CALL(p) = (hp, SOS, Afork(1)i)+ HFORK ANS P(p) = (hSOS, p, Succ afork (hdl)i)+ for some handle hdl 6= none HFORK ANS C(p) = (hSOS, p, Create Clone(iC , p, 1)ihSOS, p, Succ afork (none)i)+ HCLOSE(p, sid) = (hp, SOS, Sclose(sid)ihSOS, p, Succi)+ Note that the first argument of the Create Clone message indicates the (index of the) program that is supposed to run as the child process.
Remains the most complicated case, namely the specification of the child process which is responsible for carrying out the SMTP protocol. As above, we consider only the successful case here.
HCHILD(p, sid) = HGREETING(p, sid) ◦ HReadEmails(p, sid) ◦
HQUIT(p, sid) ◦ HCLOSE(p, sid)
The history set for HCLOSE(p,sid) is already defined above. HGREETING(p, sid) and HQUIT(p, sid) look as follows:
HGREETING(p, sid) = HREADY(p, sid) ◦ HReadLine(p, sid, ”EHLO ” + ipr) ◦
HGREETS(p, sid, ipr) for some remote ip address ipr HREADY(p, sid) = (hp, SOS, Swrite(sid, ”220 ” + get na(p) +
” SMT Service Ready”)ihSOS, p, Succi)+ HGREETS(p, sid, ipr) = (hp, SOS, Swrite(sid, ”250 ” + get na(p) + ” greets ” + ipr)i hSOS, p, Succi)+ HQUIT(p, sid) = HReadLine(p, sid, ”QUIT”) ◦ (hp, SOS, Swrite(sid, ”221 ” + p + ” closing”)i ◦ hSOS, p, Succi ◦ hp, SOS, Exiti)+
ReadLine consists essentially of successively reading one character after the other. A slight complication arises as it may be possible that the attempt to read a single character may be successful, yet results in an empty string (i. e., we assume the socket-read command to be non-blocking).
8 HReadString(p, sid, string) if ∃s : string = sˆCRˆLF HReadLine(p, sid, string) = < and s does not contain CRˆLF : Ø otherwise i. e., reading a line means to read a string that (uniquely) ends with a carriage return (CR) followed by a line feed (LF).
HReadString is defined as the smallest set satisfying the equations HReadString(p, sid, ””) = ()+
HReadString(p, sid, c ˆ s) = HReadChar(p, sid, c) ◦ HReadString(p, sid, s) where
HReadChar(p, sid, c) = HReadEmpty(p, sid) ◦ HReadChar1(p, sid, c)
HReadChar1(p, sid, c) = (hp, SOS, Sread (sid, 1)ihSOS, p, Succ sread (1, ”c”)i)+ and HReadEmpty(p, sid) = μH.(H = ()+ ∪ HReadEmpty1(p, sid) ◦ H ) where HReadEmpty1(p, sid) = (hp, SOS, Sread (sid, 1)ihSOS, p, Succ sread (0, ””)i)+ Remains to specify the history set HReadEmails (which in addition covers writing the email to the Inbox file). HReadEmails is the smallest set satisfying the equation HReadEmails(p, sid) = ()+ ∪
HReadEmail(p, sid) ◦ HReadEmails(p,sid) , i. e.,
HReadEmails(p, sid) = μH. H = ()+ ∪ HReadEmail(p, sid) ◦ H where HReadEmail(p, sid) splits into several parts, namely in reading the sender’s address, the recipient’s address, the email data and the writing of the email to the file system.
HReadEmail(p, sid) = HReadS(p, sid, s) ◦ HReadR(p, sid, r) ◦ HReadD(p, sid, d) ◦
HWriteEmail(p, sˆr ˆd) for some s, r, d HReadS(p, sid, s) = HReadLine(p, sid, ”MAIL FROM: ” + s) ◦
(hp, SOS, Swrite(sid, ”OK”)i ◦ hSOS, p, Succi)+ HReadR(p, sid, r) = HReadLine(p, sid, ”RCPT TO: ” + r) ◦
(hp, SOS, Swrite(sid, ”OK”)i ◦ hSOS, p, Succi)+ HReadD(p, sid, d) = HReadLine(p, sid, ”DATA:”) ◦ (hp, SOS, Swrite(sid, ”354 Start mail input;
end with CRLF . CRLF”)i ◦ hSOS, p, Succi)+ ◦ HReadD′(p, sid, d) ◦ (hp, SOS, Swrite(sid, ”OK”)i ◦ hSOS, p, Succi)+ HReadD′(p, sid, ”.”) = HReadLine(p, sid, ”.”)
HReadD′(p, sid, l ˆd) = HReadLine(p, sid, l) ◦ HReadD′(p, sid, d) provided l 6= ”.”
HWriteEmail(p, e) = (hp, SOS, Flock (Inbox)ihSOS, p, Succi ◦ hp, SOS, Fseek (Inbox, 1, 0)ihSOS, p, Succ fseek(pos1)i ◦ hp, SOS, Fwrite(Inbox, e)ihSOS, p, Succ fwrite(pos2, n)i ◦ hp, SOS, Funlock (Inbox)ihSOS, p, Succi)+ for some file positions pos1 and pos2.
It is certainly out of the scope of this paper to show all the verification details for the whole SMTP-Server. Instead, we emphasise on a small portion of it, namely the readLine procedure as specified above.
In a VSE-like fashion the procedure is listed below: PROCEDURE readLine(sid:length,buffer,res) int length, ec; buffer buffer_array; char c, cprevious; bool res; BEGIN length := 1; res := true; c := null; cprevious := null; cl := nil; WHILE ((cprevious /= CR OR c /= LF) AND res = true) DO length := 1; socket_read(sid:length,buffer,ec); if (ec = SUCC) then res := true else res := false fi; if (length = 1 and res = t) then cprevious := c; c := buffer[0]; cl := write(cl,c) fi OD; END
The readline procedure is supposed to read characters from the given TCP/IP socket until it finds a CR followed by a LF. This behaviour is described by the history set HReadLine(p, sid, cl) for a procedure identifier p, socket id sid and a list of characters (string) cl. The segments of the histories that are members of this set are the results of calling the readLine procedure from above. Therefore, for the verification of the SMTP server, we need to make sure that this procedure (implementation) meets its intended semantics (the corresponding history sets from above).
According to the technique described above we have to prove the following property: hc0 = hc ∧ ho0ut = hout ∧ mode = f in → hreadLine(p, sid : hc, hout, mode, cl, res)i mode 6= stop →
0 ∃h : hout = hout ◦ h ∧ ((mode = f in ∧ res = t) ↔ h ∈ HReadLine(p, sid, cl)) The proof of this property is split into three main lemmas (and several small lemmas about the data structures used): The first lemma is formulated close to an invariant used to deal with the (single) while loop occurring in the body of readLine.
0 hout = hout ∧ mode = f in → hreadLine(p, sid : hc, hout, mode, cl, res)i mode 6= stop
0 → ∃h : hout = hout = h ∧ ((mode = f in ∧ res = t)
→ h ∈ HReadString(p, sid, cl) ◦ HReadEmpty(p, sid)) ∧ (h ∈ HReadString(p, sid, cl) ◦ HReadEmpty(p, sid) ∧ cl 6= hi → (mode = f in ∧ res = t))
The following lemma states that we can drop the history sets HReadEmpty, because HReadEmpty(p, sid) \ HReadEmpty1(p, sid) = {[]}.
0 hout = hout ∧ mode = f in → hreadLine(p, sid : hc, hout, mode, cl, res)i
0 mode 6= stop → ∃h : hout = hout ◦ h ∧
((mode = f in ∧ res = t) → h ∈/ HReadEmpty1(p, sid) ◦ H)
Finally, we need a lemma that deals with the fact that end of lines are marked with hCR, LF i. Notably, the proof for this lemma does not require any knowledge about the external call simulation socket read sim. Thus this example shows how a proof can be separated into parts dealing with concurrent communication and those dealing with properties independent of the communication, even if the properties are not separated by the program structure. hreadLine(p, sid : hc, hout, mode, cl, res)i
mode = f in ∧ res = t → ∃cl0 : cl = cl0 ◦ hCR, LF i 4
In this section we describe the construction of π˜i out of πi. The C0 program π with external calls is transformed into a program π˜ that takes histories as input and produces histories as output but uses only standard function calls. Since histories describe initial segments of nonterminating behaviors the new program is intended always to terminate. We consider its result as an approximation of the computation of π following the general replay and extend strategy outline above.
We suggest a uniform transformation of the program into an approximation
exhibiting the same behavior as the original program with respect to prefixes
of event histories. The transformation preserves the structure of the program.
Thus it is possible to use a verification approach that follows the structure of
the implementation. Moreover this approach enables us to employ well known
verification techniques for sequential programs as described in, for instance, [
In this section the uniform procedure to convert programs πi into their approximations π˜i is described. Let the program πi be given as πi = (δi|αi(x¯)), where x¯ are the (program) variables occurring free in αi and δi is the list of procedure declarations used in αi. The function approxπi(p0, h0) will be computed by the program π˜i given by ( approx i(p, hin : hout, mode) ⇐ declare hc := hin; x¯ := σ¯ begin mode := f in; hout := []; start i(: p, hc, hout); αei(x¯);
stop(: hout, hc, mode) end, ext call(πi), δ˜i | approx i(p0, h0 : h1, m0) ) where the initial values of h1 and m0 (used to return the results) are not relevant.
The sequence ext call(πi) contains declarations for the procedures that simulate the external calls occurring in πi together with additional start and stop procedure, start i and stop, respectively.
In the computation of the approximation a local variable hc is used that contains the currently remaining history during the execution of αei. It is set to hin initially. The output history is collected in hout as the computation proceeds while the mode is kept in mode.
The construction is guided by the following general idea. An initial segment of the computation of αi executed by p is replayed using (consuming) h and extending hout.
External calls c(τ¯ : z¯, res) are replaced (or simulated) by procedures with declarations c sim(p, x¯ : y¯, res, hc, hout, mode) ⇐ bodyc. The simulating procedures analyze and shorten (consume) the current history h and extend the current output hout. The first argument indicates the process that is executing αi. Let v¯ and w¯ be the values of τ¯ and z¯, respectively.
If in hc there is no event generated by p, then the computation (of α˜i) stops with hout ◦ h ◦ [evc(p, v¯ : w¯)] as final output, where evc(p, v¯ : w¯) is the event generated by this call of c.
If in hc there is a further event generated by p, then it has to be evc(p, v¯ : w¯). Otherwise the computation stops signalling a failure. In that case the particular hc is not realized by πi (and π˜i) which might happen due to over specification.
For hc = h0 ◦ h′1, where in h0 there is no event generated by p and f st(h′1) = evc(p, v¯ : w¯), h′1 is scanned for a matching answer event. If there is no such answer, then the computation stops with hout ◦ h as the final output history and mode being set to stop.
In all these cases the procedure simulating the external call leaves the result parameters untouched since they are not needed anymore.
In the following paragraph we make use of the predicate M atch ev(e1, e2) which checks whether the event e2 represents a matching answer for the event e1. hp, SOS, Sread(sid, 1)i and hSOS, p, Succ sread(1, ”c”)i represents an example for a pair of matching messages. These two messages represent the call of a socket read on the socket identified by sid and the corresponding answer message containing the read string c (see also chapter 3).
For h′1 = h1 ◦ h2, where rst(h1) contains no answer matching f st(h′1) = f st(h1) = evc(p, v¯ : w¯) and f st(h2) = e such that M atch ev(evc(p, v¯ : w¯), e) the procedure returns values for the result parameters according to the message contained in e and the computation of α˜i continues with rst(h2) as the new remaining history and hout ◦ h0 ◦ h1 ◦ [f st(h2)] as the new current output.
The above mentioned analysis of the current history h with respect to an external call c(τ¯ : z¯, res) of p is given by parsec(p, h, v¯, w¯) ∈ His × His × His, where again v¯ and w¯ are the values of τ¯ and z¯, respectively.
parsec(p, h, v¯, w¯) = (h0, h1, h2) ↔ (h = h0 ◦ h1 ◦ h2 ∧ evc(p, v¯ : w¯) 6∈ h0 ∧ (h1 6= [] → (f st(h1) = evc(p, v¯ : w¯) ∧
∀e ∈ rst(h1).¬M atch ev(evc(p, v¯ : w¯), e))) ∧ (h2 6= [] → M atch ev(evc(p, v¯ : w¯), f st(h2)))) The body of the procedure is given below. bodyc :≡ declare h0 := parsec(p, hc, x¯, y¯).0; h1 := parsec(p, hc, x¯, y¯).1; h2 := parsec(p, hc, x¯, y¯).2 begin if mode 6= f in then skip else if ∃e ∈ h0.Gen(p, e) then mode := f ail else if h2 = [] then mode := stop; if h1 = [] then hout := hout ◦ h ◦ [evc(p, x¯, y¯)]; hc := [] fi else hout := hout ◦ h0 ◦ h1 ◦ [f st(h2)]; hc := rst(h2); y0 := ret valc1(f st(h2)) . . . yn−1 := ret valcn−1(f st(h2)) res := ret resc(f st(h2)) fi fi fi where Gen(p, e) is true if the event e is generated by the process represented by p. The function ret valci(e) extracts the result parameters from the event e and ret resc(e) returns the result value of the corresponding external call c.
Before the execution of α˜i is started the begin of an active thread of p has to be determined by the start procedure, or if p has been started by a fork call, the start of the ancestor’s thread who was running the very beginning of the program has to be found. If there is no p-thread executing πi (or no suitable ancestor), then the given input history is returned as output and mode is set to term.
The procedure that simulates the start of a process πi is given by the declaration start i(: p, hc, h out, mode) ⇐ bodystart i. It parses the given history h according to the definition of P roc.
parsestart i(p, hc) = (h0, h1) ↔ h = h0 ◦ h1 ∧ (h1 6= [] → (Create(i, p, f st(h1)) ∧
∀e ∈ rst(h1).¬T erm(i, p, e))) The procedure body then is given below.
bodystart i :≡ declare ah := anc(i, p, h); h0 := []; h1 := []; begin if ah = [] then mode := term; hout := hc; else h1 := f st(ah); h0 := Δ(hc, h1); hc := rst(h1); hout := h0 ◦ [f st(h1)]; p := get rec(f st(h1)) fi
Finally we need a stop procedure stop(: hout, h, mode) ⇐ bodystop that finalizes the simulation. It restores the original history by appending the remaining h to hout. Note that in those cases where a new (final) event was generated hc will be []. If we have reached the end of α˜i, indicated by mode = f in, we check whether according to the remaining history something needs to be done a signal the result by setting mode to f in or term, respectively. This information is needed for decomposing verification problems. The body of the stop procedure is then given as bodystop :≡ hout := hout ◦ h;
if mode = f in ∧ ∀e ∈ h.¬Gen(p, e) then mode := term fi
Whenever mode is changed (to m ∈ {stop, f ail}) by a procedure simulating an external call the rest of α˜i has to be skipped. This is achieved by adding a kind of guards to while loops and (possibly) recursive procedures. In addition h, hout, and mode have to be passed as arguments to the procedures declared in δi.
q(x¯ : y¯) ⇐ β , δ 7→∼ q˜(x¯ : y¯, hc, hout, mode) ⇐ Commands are modified as follows.
if mode 6= f in then skip else β˜ fi , δe skip 7→∼ skip x := τ 7→∼ x := τ α0; α1 7→∼ αf0; αf1 if ǫ then α0 else α1 fi 7→∼ if ǫ then αf0 else αf1 fi while ǫ do α od 7→∼ while ǫ ∧ mode 6= f in do αe od q(τ¯ : z¯) 7→∼ q˜(τ¯ : z¯, hc, hout, mode) c(τ¯ : z¯, res) 7→∼ c sim(p, τ¯ : z¯, res, hc, hout, mode) 5
Our work was motivated by the problem of verifying application level programs
with certain communication primitives given a complex formal model for
distributed instances of an operating system that are connected by a network and
include machines for the interpretation of C0 programs. Instead of working
directly on the model we have introduced sets of (finite) sequences H of
communication events to specify open distributed systems. This is a particular kind of
stream specification as discussed in [
Apart from abstracting from the local state spaces these histories were used
for a reduction to local verification problems (compositionality). In case of
application level programs this reduction is provided by a uniform transformation
π 7→ π˜. Once and for all we had to establish a relation to the original model
by a simulation theorem. This proof is based on the Verisoft C0 interpreter and
is the only semantic consideration necessary in our approach. As opposed to
the Hoare-style proof system presented in [
An earlier attempt to map the Verisoft model to the temporal framework
implemented in VSE failed. Temporal verification techniques, like those
mentioned in [
Despite many technical differences the basic idea for the reduction to π˜ is
similar to the use of (prefix closed) time diagrams in [