Rely-guarantee Reasoning about Concurrent Reactive Systems]Rely-guarantee Reasoning about Concurrent Reactive Systems
The  Framework, Languages Integration and Applications

This article is an extended version of <cit.>.

This work has been supported by the National Natural Science Foundation of China (NSFC) under the Grant No. 61872016, and the National Satellite of Excellence in Trustworthy Software Systems, funded by NRF Singapore under National Cyber-security R&D (NCR) programme.

Yongwang Zhao

Zhejiang University
School of Cyber Science and Technology, College of Computer Science and Technology
38 Zheda Road

David Sanán

Nanyang Technological University
School of Computer Science and Engineering
50 Nanyang Avenue

The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control systems and business process systems. However, specifications using heterogeneous reaction patterns, different abstraction levels, and the complexity of real-world CRSs are still challenging the rely-guarantee approach.
This article proposes , a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach the specification and logic of reactive aspects of CRSs from event behaviours.  parametrizes the language and its rely-guarantee system for event behaviour using a rely-guarantee interface and allows to easily integrate 3rd-party languages via rely-guarantee adapters. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs.  has been applied to two real-world case studies, i.e. formal verification of concurrent memory management in Zephyr RTOS and a verified translation for a standardized Business Process Execution Language (BPEL) to .

<concept_desc>Theory of computation Logic and verification</concept_desc>
<concept_desc>Software and its engineering Specification languages</concept_desc>
<concept_desc>Theory of computation Program reasoning</concept_desc>
<concept_desc>Software and its engineering Software verification</concept_desc>
<concept_desc>Software and its engineering Concurrent programming languages</concept_desc>

[500]Theory of computation Logic and verification
[500]Software and its engineering Specification languages
[500]Theory of computation Program reasoning
[500]Software and its engineering Software verification
[500]Software and its engineering Concurrent programming languages

§ INTRODUCTION

Nowadays high-assurance systems are often designed as concurrent reactive systems (CRSs) <cit.>, which react to their computing environment by executing a sequence of commands under an input event.
Examples of CRSs are concurrent operating systems (OSs), interrupt-driven control systems and business process systems, whose implementation follows a shared-variable event-driven paradigm. However, formal verification of shared-variable CRSs is still challenging <cit.>.

The rely-guarantee technique <cit.> represents a fundamental approach to compositional reasoning of concurrent programs with shared variables, where imperative languages with extensions for concurrency describes the programs.
The interference that occurs when concurrent programs access and update shared variables is explicitly specified by rely and guarantee conditions in the rely-guarantee method. This article concentrates on compositional reasoning about shared-variable CRSs using the rely-guarantee technique.

§.§ Motivation and Challenges

Reactive systems respond to continuous stimulus from their computing environment <cit.> by changing their state and, in turn, affecting their environment by sending back signals to it or initiating other operations. The inherent features of state-of-the-art CRSs are as follows.

* CRSs may involve many different competitive agents executed concurrently with shared resources. Such concurrency might be due to multicore setting, embedded interrupts or task preemption, like in concurrent OS kernels <cit.> and interrupt driven control systems, where the execution of handlers is not atomic.

* CRSs have various reaction structures, such as peer reaction, flow reaction and hierarchical reaction. Concurrent OS kernels behave as peer reactions, where kernel services behaves as reactors providing a fair scheduler to user calls. Modern business processes are regarded as flow reaction structures, which has a set of complex flow activities. An example of CRSs with a hierarchical reaction structure is Real-time Control Systems (RCSs) <cit.>, which is a layered reference model architecture for unmanned vehicles.

* The configuration and context of the underlying hardware of systems are not usually encoded in programs, which represent only a portion of the whole system behaviour. For instance, when and how interrupts are triggered, and which handlers are invoked to react with an interrupt, are out of the handler code when considering the models for interrupt handlers in OS kernels (e.g. kernel services and scheduling).

In such a setting of CRSs, we observe that the rely-guarantee approach faces the following challenges.

Challenge 1: Tackling complex reaction structures
Whilst rely-guarantee provides a general framework and can certainly be applied for CRSs, the languages in existing mechanizations of rely-guarantee (e.g. in <cit.>) are imperative and designed only for pure programs, i.e, programs following a flow of procedure calls from an entry point.
Examples of the reactive systems mentioned above are far more complex than pure programs because they involve many different agents as well as heavy interactions with their environment.
Without statements for such system behaviour, we often use imperative programs to simulate them. For instance, in the setting of imperative languages, concurrent OS kernels in the peer reaction structure are usually modelled as the parallel composition of reactive systems, each of which is simulated by a non-terminating loop program. The relevant handlers are invoked in the loop body adding the input arguments from user calls (e.g. in <cit.>).
First, the environment non-deterministically decides the event handler being triggered and its arguments.
Second, some critical properties, such as noninterference of OS kernels <cit.>, concern traces of reactions rather than program states only.
Without native support in the language semantics, while loop programs have to use auxiliary logical/program variables to simulate the non-deterministic choice of handlers and parameters, and to capture the event context of each reactive system.
This adds an additional level of complexity in programs and rely-guarantee conditions, in particular for realistic CRSs with many event handlers.
The reason of these problems is the lack of a rely-guarantee approach for system reactions and, as a result, the mixture of system and program behaviours.

Challenge 2: Reusing 3rd-party languages and their rely-guarantee proof systems
Deep specification and verification is a trend in formal methods for both academy and industry <cit.>.
High assurance of critical systems demands that formal verification of functional correctness and safety/security properties is applied not only at the specification level <cit.>, but also at the code level in the highest assurance levels <cit.>. Verification of the specification can be conducted using abstract specification languages, but the verification of the implementation requires that modelling languages capture the features in programming languages such as exceptions and procedure calls. To formally verify CRSs at different levels, the rely-guarantee approach should be flexible enough to incorporate various 3rd-party languages and their rely-guarantee proof systems, and thus to be able to integrate and to reuse them. The challenge is to design a rely-guarantee framework to deal with interoperability of languages and bridge the gap between their rely-guarantee components.

Challenge 3: Reasoning about real-world concurrent reactive systems.
Formal verification of real-world CRSs at low-level design and source code levels is challenging because of their complexity, being necessary to apply scalable methods.
As a typical class of CRSs, formal verification of concurrent OSs is a challenge <cit.>, in particular the formal verification of the memory management. Data structures and algorithms of memory management in OSs are usually laid out in a complex manner to achieve a high performance. This complexity implies as well complex invariants that the formal model must preserve. In order to prevent memory leaks and block overlapping, these invariants have to guarantee the well-formedness and consistency of the structures, meanwhile keeping a precise reasoning to track both numerical and shape properties. Moreover, thread preemption and fine-grained locking often make the kernel execution of memory services to be concurrent.

§.§ Approach Overview

In this article,  takes the level of abstraction and reusability of the rely-guarantee method a step further by proposing an expressive event language for complex reaction structures at the system level, as well as decoupling the system and program levels. The result is a flexible rely-guarantee framework for CRSs, which can integrate existing rely-guarantee implementations at program level without any change of them.  is organized in two levels:

* The system level introduces the notion of “events” <cit.> into the rely-guarantee method to modelling system reactions. This level defines the events composing a system, and how and when they are triggered. It specifies the language, semantics, and mechanisms to reason on sequences of events and their execution conditions.  provides a rely-guarantee interface which is an abstraction for common rely-guarantee components for the program level.

* The program level focuses on the specification and reasoning of the behaviour of the events in the first level.  can easily integrate concrete languages used to model the behaviour of events by using a rely-guarantee adapter which implements the rely-guarantee interface. This design allows  to be independent of program languages and thus to easily reuse existing rely-guarantee frameworks.

$ \left .
\begin{aligned}
& \stmtevthead{mem\_pool\_alloc}{Ref\ pool, Nat\ size, Int\ timeout}{t}
\\
& \isacommand{WHEN}
\\
& \quad pool\ {\isasymin}\ {\isasymacute}mem{\isacharunderscore}pools\
{\isasymand}\ timeout\ {\isasymge}\ {\isacharminus}{\isadigit{1}}
\end{aligned}
\quad \right \}\  \textbf{Event declaration}

$ \left .
\begin{aligned}
& \isacommand{THEN}
\\
& \quad ...... \text{\color{ACMGreen} // we omit some statements here. }
\\
& \quad \isacommand{IF}\ timeout\ {\isachargreater}\ {\isadigit{0}}\ \isacommand{THEN}
\\
& \quad \quad  {\isasymacute}endt\ {\isacharcolon}{\isacharequal}\ {\isasymacute}endt{\isacharparenleft}t\ {\isacharcolon}{\isacharequal}\ {\isasymacute}tick\ {\isacharplus}\ timeout{\isacharparenright}
\\
& \quad \isacommand{FI};;
\\
& \quad ......
\\
& \quad \isacommand{FOR}\ {\isasymacute}from\_l := {\isasymacute}from\_l(t := {\isasymacute}free\_l\ t);
{\isasymacute}from\_l \ t < {\isasymacute}alloc\_l\ t;
\\
& \quad \quad \quad {\isasymacute}from\_l := {\isasymacute}from\_l(t:={\isasymacute}from\_l\ t + 1)\ \isacommand{DO}
\\
& \quad \quad \isacommand{ATOMIC}
\\
& \quad \quad \quad {\isasymacute}mem\_pool\_info := set\_bit\_divide\ {\isasymacute}mem\_pool\_info\ p \ ({\isasymacute}from\_l\ t)\ ({\isasymacute}bn\ t);;
\\
& \quad \quad \quad ......
\\
& \quad \quad \isacommand{END}
\\
& \quad \isacommand{ROF}
\\
& \quad  ......
\\
& \isacommand{END}
\end{aligned}
\quad \right \}\  \textbf{Event body}

An Example of Event

At the system reaction level, we consider a reactive system as a set of event handlers called event systems responding to stimulus from the environment.
<ref> illustrates an event for memory allocation in OSs. The event declaration has an event name, a list of input parameters, and a guard condition to determine the conditions triggering the event. In addition to the input parameters, an event has a special parameter $\textbf{OF}\ t$, which indicates the execution context, e.g. the thread invoking the service and the external devices triggering the interrupt. The behaviour of an event is specified as the event body by using an imperative program described in a 3rd-party language.

To deal with complex reaction structures, we design an event specification language in  supporting a structural compositions of  set events, e.g. join and nondeterministic choice that defines an event system. For instance, an event system composed of a nondeterministic choice of events models a peer reaction structure.

The execution of an event system concerns the continuous evaluation of the guards of the events with their arguments. From the set of events for which their associated guard condition holds in an execution state, one event is non-deterministically selected to be triggered, and its body executed. After the event finishes, the guard evaluation starts again looking for the next event to be executed. We call the semantics of event systems reactive semantics.
A CRS is modelled as the parallel composition of event systems interleaving their execution.
Different from other modelling approaches (e.g., Event-B <cit.>) where the execution of events are atomic, we consider the interleaved semantics of events and relax the atomicity of them in .

CRSs representation in PiCore presents the following advantages:

* Expressivity: the event language in  is able to model complex reaction structures of CRSs. We have built two different cases studies showing how does  specify a peer and a flow reaction systems.

* Reusability: the  framework can integrate and thus reuse 3rd-party languages and their rely-guarantee frameworks. In this work we describe events on two different imperative languages by using the PiCore integration interface.

* Simplicity: compared to using imperative languages, the event language in  can considerably simplify the formal specification of CRSs. We formalize the Zhephyr RTOS memory management to show how complex concurrent reactive systems can be elegantly and simply described with .

At the time of writing this article,  supports the verification of total correctness of events, whose execution is usually assumed to be terminating, as well as the properties of event systems, whose execution is often non-terminating.
In this article, we consider the verification of two different classes of properties for CRSs: pre and post conditions and invariants in the fine-grained execution. Invariants are used on the verification of safety properties concerning the small steps inside events, which must preserve such invariants.
For instance, in the case of Zephyr RTOS, one safety property is that memory blocks do not overlap each other even during the internal steps of the alloc and free services.
The execution trace of events can define other critical properties like noninterference <cit.>, which is part of our ongoing work.

Following the above principles, the  architecture is shown in  <ref>, where the lines represent the uses relation of blocks. We use Isabelle/HOL theorem prover as the specification and verification system. The  framework use Isabelle's locales to define the rely-guarantee interface, which is a set of common rely-guarantee components that existing languages may respect.
For the integration of external languages, we adopt the adapter design pattern <cit.>. By implementing a rely-guarantee adapter that respects the rely-guarantee interface, 3rd-party languages and their rely-guarantee proof systems are integrated into  by instantiating the  framework.

We have integrated two existing languages (<cit.> and <cit.>) and their rely-guarantee proof systems into the  framework. As a result we create two instances of :  and .  is a simple imperative language in Isabelle/HOL, which follows the specification in <cit.>.
is a generic and expressive imperative language designed for modelling real world concurrent languages.  extends Simpl <cit.> with concurrency, and provides a rely-guarantee proof system in Isabelle/HOL. Simpl is composed of the necessary constructs to capture most of the features present in common sequential languages, such as conditional branching, loops, abrupt termination and exceptions, assertions, mutually recursive functions, expressions with side effects, and nondeterminism. Additionally, Simpl can express memory-related features like the memory heap, pointers, and pointers to functions.
Simpl is able to represent a large subset of C99 code and has been applied to the formal verification of seL4 OS kernel <cit.> at C code level.

The  Approach

Finally, we apply the  framework in two case studies. As a peer reaction case study, we model in  the memory management of Zephyr OS <cit.>, a real-world concurrent RTOS. We use the  proof system to prove complex properties about the Zephyr concurrent memory management correctness and partial termination. As a case of flow reactions, we model the BPEL language <cit.> in , a standard of business process execution language, showing soundness and completeness of the model.

Zephyr RTOS
Considering an OS Kernel as a reactive system with a peer reaction structure, the OS is in an idle loop until it receives an interruption which is handled by an interruption handler.
Whilst interrupt handlers execution is atomic in sequential kernels, they can be interrupted in concurrent kernels <cit.> allowing services invoked by threads to be interrupted and resumed later. We have applied  to the formal specification and mechanized proof of the concurrent buddy memory allocation of Zephyr RTOS. The formal specification is fine-grained, providing a high level of detail. It closely follows the Zephyr C code, covering all the data structures and imperative statements present in the implementation.
We use the rely-guarantee proof system of  for the formal verification of functional correctness and invariant preservation in the model, revealing three bugs in the C code.

Compared to OSs, BPEL programs are CRSs with a flow reaction structure. BPEL aims to model the behaviour of processes via a language for the specification of both executable and abstract business processes. It extends the Web Services interaction model and enables it to support business transactions. BPEL has complex basic and structural activities, such as receive, reply, invoke, sequence, while, repeatuntil, flow (parallel). We have applied  to interpret the semantics of the BPEL language by translating BPEL into . To show the correctness of this translation, we prove a strong bisimulation between the source BPEL program and the translated  specification. In this way, formal verification of BPEL programs can be conducted in the  framework. The strong bisimulation implies the soundness and completeness of the formal verification of BPEL programs in .

§.§ Contributions

This work is entirely mechanized and proved in Isabelle/HOL; the sources are available at <https://lvpgroup.github.io/picorebook/>.
In summary, this article makes the following new contributions.

* We propose a novel event specification language and its rely-guarantee proof system for CRSs. To the best of our knowledge,  is the first rely-guarantee approach supporting complex reaction structures of CRSs.

*  is a parametric rely-guarantee framework for CRSs. By using rely-guarantee interfaces and adapters, it allows reusing existing languages and their rely-guarantee proof systems.
To the best of our knowledge,  is the first flexible and open rely-guarantee framework for 3rd-party languages.

* We have integrated two existing languages and their rely-guarantee proof systems into the  framework, and thus created two instances of . These instances can formally specify and verify CRSs at different abstraction levels.

* As a case study of concurrent OSs, we have applied  to the formal specification and mechanized proof of the concurrent buddy memory allocation of Zephyr RTOS. During the formal verification of functional correctness and invariant preservation, we reveal three bugs in the C code. To the best of our knowledge, this work is the first formal verification of a concurrent buddy memory allocation from a real-world operating system.

* As a case study of concurrent business processes, we have applied  to the formalization of the BPEL standard by an automated translator. We use a bisimulation relation to prove the correctness of this translation. To the best of our knowledge, this work presents the first verified translation of BPEL to a formal reasoning system.

We partially present contributions (1) - (3) in <cit.>, where we only supported modelling CRSs with a peer reaction structure. In this article, we have completely redesigned the event language and its proof system, supporting complex reaction structures. The semantics of the event language has also been extended by the modular definition of computations to considerably simplify the soundness proof of rely-guarantee rules. Also, the current design of  has a better parameter support in the creation of the events. The rely-guarantee interface of  has been also simplified and made clearer. Contribution (4) was partially presented in <cit.>. In this article, we use the new event language to revise the formal specification of Zephyr RTOS.

§.§ Organization

The rest of this article is organized as follows. We first introduce the rely-guarantee method and relevant Isabelle/HOL notation for this article in  <ref>.  <ref> presents the  rely-guarantee framework for CRSs.  <ref> presents the rely-guarantee interface and adapter.  <ref> shows how we integrate the two 3rd-party languages,  and , and their rely-guarantee proof systems.
Next, we present the two case studies in s <ref> and <ref> respectively.
We evaluate our work and compare the related work in  <ref>. Finally, we conclude this article in  <ref>.

§ PRELIMINARIES

In this section, we briefly introduce the rely-guarantee method as well as Isabelle/HOL notations used in languages integration and case studies.

§.§ Rely-guarantee Reasoning

In the rely-guarantee method <cit.>, executions of concurrent programs are considered as computations, i.e. traces of configurations which are a pair of a program and a state. The rely-guarantee method distinguishes environment steps $\rgenvtran$ from component steps $\rgptran$ in computations.
A rely-guarantee specification for a program is a quadruple $\rgconddefault$, where $\mathit{pre}$ is the precondition, $\mathit{rely}$ is the rely condition, $\mathit{guar}$ is the guarantee condition, and $\mathit{post}$ is the postcondition.  The designer of a concurrent program can assume that if

* the initial state satisfies the precondition pre, and

* any environment step satisfies the rely condition rely,

then the program makes the following commitments:

* any program step satisfies the guarantee condition guar, and

* if the program terminates, the final state satisfies the postcondition post.

In the case of total correctness, the program ensures the termination as well.
The validity of a rely-guarantee condition is illustrated as follows.

\begin{equation}
\label{eq:rg_validity}
\overbrace{(\symbprog_0,s_0)}^{s_0 \in \textbf{pre}} \cdots \overbrace{(\symbprog_i,s_i) \rgenvtran (\symbprog_{i+1},s_{i+1})}^{(s_i,s_{i+1}) \in \textbf{rely}}  \cdots \underbrace{(\symbprog_j,s_j) \rgptran (\symbprog_{j+1},s_{j+1})}_{(s_j,s_{j+1}) \in \textbf{guar}} \cdots \underbrace{(\symbprog_n,s_n)}_{s_n \in \textbf{post}}
\end{equation}

The assumption, commitment and the validity of a specification are defined as it follows, where $\symbcomp_i$ is the $i$th configuration in a computation $\symbcomp$, $\symbstate_{\symbcomp_i}$ is the state part of the configuration, and $\symbprog_{\symbcomp_i}$ is the program of the configuration. $\compfun(\symbprog, \symbstate)$ is the set of all computations of the $\symbprog$ starting from an initial state $\symbstate$.

\begin{equation*}%\fontsize{8pt}{0cm}
\centering
\begin{aligned}
& \assumefun(\mathit{pre}, \mathit{rely}) \equiv \{\symbcomp \mid \symbstate_{\symbcomp_0} \in \mathit{pre} \wedge (\forall i < \mathit{len}(\symbcomp) - 1. \ (\symbcomp_i \rgenvtran \symbcomp_{i+1}) \longrightarrow (\symbstate_{\symbcomp_i},\symbstate_{\symbcomp_{i+1}}) \in \mathit{rely})\} \\
& \commitfun(\mathit{guar}, \mathit{post}) \equiv \{\symbcomp \mid \ (\forall i < \mathit{len}(\symbcomp) - 1. \ (\symbcomp_i \rgptran \symbcomp_{i+1}) \longrightarrow (\symbstate_{\symbcomp_i},\symbstate_{\symbcomp_{i+1}}) \in \mathit{guar}) \\
& \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad
\wedge (\symbprog_{\mathit{last}(\symbcomp)} = \cmdfinal \longrightarrow \symbstate_{\symbcomp_n} \in \mathit{post})\} \\
& \RGSAT{\symbprog}{\rgconddefault} \equiv \forall \symbstate. \ \compfun(\symbprog, \symbstate) \cap \assumefun(\mathit{pre}, \mathit{rely}) \subseteq \commitfun(\mathit{guar}, \mathit{post})
\end{aligned}
\end{equation*}

A set of rules inductively define the derivable correctness formulas $\rgsat{\symbprog}{\rgconddefault}$.  The verification of a rely-guarantee specification on a concurrent program is thus carried out by inductively applying the rules for each language construct and discharging the proof obligations the rules generate. The proof rule for parallel composition is typically defined as

\begin{equation*}
\infer{\rgsat{\symbprog_1 \parallel \symbprog_2}{\rgconddefault}}
\begin{aligned}
\rgsat{\symbprog_1}{\rgcond{pre_1}{rely_1}{guar_1}{post_1}} \quad \rgsat{\symbprog_2}{\rgcond{pre_2}{rely_2}{guar_2}{post_2}} \quad pre \subseteq pre_1 \cap pre_2\\
rely \cup guar_2 \subseteq rely_1 \quad rely \cup guar_1 \subseteq rely_2 \quad guar_1 \cup guar_2 \subseteq guar \quad post_1 \cap post_2 \subseteq post
\end{aligned}
\end{equation*}

Since valid proofs depend on a sound proof system, the soundness of the inference rules with regards to the validity of a rely-guarantee specification is proved by

\[\rgsat{\symbprog}{\rgconddefault} \Longrightarrow \RGSAT{\symbprog}{\rgconddefault}\]

§.§ Isabelle/HOL Notations

This subsection covers the Isabelle/HOL notations used later and their semantics.
Isabelle/HOL is a generic and tactic-based theorem prover that uses higher order logic.

The keyword datatype is used to define an inductive data type.
For instance, the list in Isabelle is one of the essential data type in computing and is defined as

$$\textbf{datatype} \ 'a \ list = Nil \ (``[]") \ | \ Cons \ 'a \ ``\ 'a \ list \ " (\textbf{infixr} \ ``\#")$$

where $'a$ is the type parameter for the type of elements in the list, $[ ]$ is the empty list and $\#$ is the append operation.
The polymorphic option type is defined as
$$\textbf{datatype} \ 'a \ option = None \ | \ Some \ (the: \ 'a)$$

$Some\ (e :: 'a)$ represents defined elements, and $None$ those that are not defined. The value of a defined element is obtained using operator $the$, with $the\ (Some\ e) = e$.

Isabelle/HOL allows the definition of types as records. An example of a record type is
$$\textbf{record} \ point = xcoord::int \ \ ycoord::int$$
where an instance $p$ of type point is defined as $p = {\isasymlparr} xcoord = 10, ycoord = 10 {\isasymrparr}$.
Isabelle/HOL provides operations for field projection, update, and extension. For instance, $xcoord \ p$ and $ycoord \ p$ are the projections of the fields $xcoord$ and $ycoord$ in $p$; $p{\isasymlparr} xcoord := 20, ycoord := 20 {\isasymrparr}$ updates $p$; and $\textbf{record} \ cpoint = point + col :: color$ extends $p$ with an additional field $col$ of type $color$.
Tuples in Isabelle/HOL are defined as types of ($'a \times 'b$). They provide two functions to select the elements of the tuple: $fst :: ('a \times 'b) \Rightarrow 'a$ and $snd :: ('a \times 'b) \Rightarrow 'b$.

A total functionf $fun1$ is are defined as $fun1 :: 'a \Rightarrow 'b$, i.e. a mapping from type $'a$ to type $'b$.
Given a function $f$ of type $'a \Rightarrow 'b$, the update of an element $a::'a$ in the domain of $f$ to the value $b::'b$ is represented by $f(a := b)$. This returns a new function $f'$ in which $f'\ x = f\ x$ if $x \neq a$ and $f'\ a = b$.
A function of type $'a \rightharpoonup \ 'b$ models a partial function, which is equal to $'a \Rightarrow ('b \ option)$.
Nonrecursive definitions can be made with the definition command and the primrec function definition is used for primitive recursions.

Isabelle's deals with parametric theories by using locales <cit.>.  A locale can be seen as a formula schema

\[
\bigwedge x_1...x_n. \ \isasymlbrakk A_1; ...; A_m \isasymrbrakk \Longrightarrow C
\]

where the variables $x_1,...,x_n$ are called parameters and the premises $A_1, ..., A_m$ assumptions. A formula $C$ is a theorem in the locale if it is a conclusion. In its simplest form, a locale declaration consists of a sequence of context elements declaring parameters (keyword fixes) and assumptions (keyword assumes). Moreover, a locale can be imported and extended by new parameters and assumptions in a new locale (using “+” operator).

Locales can be interpreted in the contexts of theories and structured proofs. The interpretation is made by assigning concrete data to parameters, and the resulting instantiated declarations are propagated to the current theory or the current proof context. This is called locale interpretation.

To enhance readability, we will use standard mathematical notation where possible. We use Isabelle/HOL syntax to represent the integration of the languages as well as the case studies.

§ : THE RELY-GUARANTEE REASONING FRAMEWORK

This section presents the event language of  as well as its notion of computations, rely-guarantee proof system, the soundness of proof rules and invariant verification.

§.§ An Event Specification Language

We design a new specification language for CRSs by introducing the notion of “events”. The language decouples the triggering mechanism in system reactions from the execution behaviour of triggered events. The triggering mechanism specifies how and when the system reaction is triggered, and the execution behaviour defines how the system reaction is executed. The event language focuses on the triggering mechanism, and parametrizes the execution behaviour with the input parameters to the event that are provided when the event is triggered. The elemental component to specify a reaction triggering is the event. To incorporate complex reaction structures, we design a set of structural compositions of events in the language.

\[
\begin{aligned}
\textbf{Event System}: & & \\
\symbevtsys \ ::= &\ \event{\eventdef} 						& \text{(Basic Event)}\\
| &\ \atomevt{\eventdef} 						& \text{(Atomic Event)}\\
| &\ \anonevt{\symbprog}     					& \text{(Triggered Event)}\\
| &\ \evtseq{\symbevtsys_1}{\symbevtsys_2} 	& \text{(Sequence)}\\
| &\ \evtchoice{\symbevtsys_1}{\symbevtsys_2} & \text{(Choice)}\\
| &\ \evtjoin{\symbevtsys_1}{\symbevtsys_2} 	& \text{(Join)}\\
| &\ \evtrec{b}{\symbevtsys} 					& \text{(Iteration)} \\
\textbf{Parallel Event System}: & & \\
\symbpes\ ::= &\ {\parsysc} 			& \text{(Parallel Composition of Event Systems)}
\end{aligned}
\]

The Abstract Syntax of Event Language

The abstract syntax of the event language is defined as shown in  <ref>.
An event system $\symbevtsys$ is an event (basic, atomic and triggered), or a structural compositions of event systems.
A CRS is modelled as a parallel composition of event systems with shared states, denoted as $\symbpes$. It is a function from $\symbCore$ to event systems, where $\symbCore$ indicates the identifiers of event systems and is considered as the execution context of event systems.
This design is more general and can be applied to track executing events. For instance, we use $\symbCore$ to represent the core identifier in multicore systems.

§.§.§ Events

The syntax for events distinguishes basic, atomic and triggered events. Basic and atomic events are pending to be triggered in particular states.
A basic event is defined as $\event{\eventdef}$, where $l$ is the event label, $g$ is the event guard condition, and $\symbprog$ is the body of the event. ${\eventdef}$ parametrizes triplets $(l,g,P)$ with the input parameters of the event, representing the set of all possible instances of $(l,g,P)$ from the domain of the parameters. This set is automatically constructed from the domain of the event parameters in the concrete syntax of .
$\event{\eventdef}$ can be triggered when there is at least one element in the set of event instances for which the current state satisfies its guard. Then, the related body is executed, and it becomes a triggered event $\anonevt{\symbprog}$. The execution of $\anonevt{\symbprog}$ just simulates the execution of the program $\symbprog$. The execution of $\anonevt{\symbprog}$ interleaves with its parallel event systems. However, $\atomevt{\eventdef}$ is atomically executed in one single step without interleaving with the other parallel event systems.

§.§.§ Event Composition

We design four structural constructs for event composition: Sequence, Choice, Join and Iteration.
The sequence of two event systems models the sequential execution of them. The Choice of two event systems is represented by $\evtchoice{\symbevtsys_1}{\symbevtsys_2}$. It models non-determinism of events by choosing one of them to be executed, i.e. if $\symbevtsys_1$ (or $\symbevtsys_2$) is able to move one step forward and becomes $\symbevtsys'_1$ ($\symbevtsys'_2$), $\evtchoice{\symbevtsys_1}{\symbevtsys_2}$ evolves to $\symbevtsys'_1$ ($\symbevtsys'_2$). The Choice construct can represent the conditional structure (e.g. IF cond THEN P ELSE Q) using complementary guards for two basic events.
Different from Choice, the execution of the Join of two event systems $\evtjoin{\symbevtsys_1}{\symbevtsys_2}$ is concurrent and finishes when the two event systems finish. Thus, it is also called concurrent join.
In addition to the top-level parallel composition of event systems ($\symbpes$), we retain the parallel composition at the event level (Join). With the two levels of parallel composition, it becomes easy to specify CRSs with two levels of concurrency, such as concurrent OS kernels on multicore processors, where the kernel instance on each core is also concurrent due to its interruptable and preemptive execution.
The Iteration construct carries out interaction of events which can be repeated unboundedly. This construct is similar to while-loops in imperative languages.

§.§ Operational Semantics

<ref> shows the small-step operational semantics of the event language. Due to the multi-level structure of the event language, we classify the transition rules into three categories: program transitions, event systems and parallel event systems.

Since  is a parametric framework for underlying programs, the operational semantics of  is defined in terms of the semantics of the underlying program language and they are an input parameter in the locale modelling  in the Isabelle HOL mechanization. Hence, this section does not provide details on the semantics of programs.

§.§.§ Transition Rules

(l,g,P) ∈ev     ∈g

(l,g,P) ∈ev     s ∈g     t

Qt     Q ≠

Qt     Q =

_1'_1t      '_1 ≠

_1'_1t      '_1 =

∈b     ≠

Small-step Operational Semantics of the Event Language

The small-step transition relation of the underlying program language is denoted as $\ptran{P}{s}{Q}{t}$, where $P,Q$ are programs, $s,t$ are states and $\symbenv$ is used for some static configuration for programs (e.g. an environment for procedure declarations). The notation $\ptrans{P}{s}{Q}{t}$ is the reflexive transitive closure of $\ptran{P}{s}{Q}{t}$.
In , $\cmdfinal$ denotes program termination.
The transition rules for event systems have the form of $\estran{\symbevtsys}{s}{\etranlabel}{\symbevtsys'}{t}$, where $\etranlabel =  \actk{\symbact}{\symbcore}$ is the combination of a transition label $\symbact$ of event systems and the execution context $\symbcore$. It means that transition $\symbact$ is done by the event system $\symbcore$. $\symbact$ indicates the transition type of event systems and is defined as

\[\symbact = \etranlabelc \mid \evtent{l} \mid \aevtent{l} \]

The notation $\etranlabelc$ is a label constant representing anonymous transitions of triggered events (TriggeredEvt and TriggeredEvtFin), of expression evaluations (EvtIterT and EvtIterF) and of eliminating final triggered events $\fin$ (EvtJoinFin). $\cmdfinal$ is the notation to represent the termination of programs.
The other two types of labels indicate actions respectively triggering events and atomic events. $\actk{ }{\symbcore}$ means that the action occurs in event system $\symbcore$.
The transition rule for parallel event systems has a similar form of $\pestran{\symbpes}{s}{\actk{\symbact}{\symbcore}}{\symbpes'}{t}$.

Next, we discuss each transition rule of the semantics. The transition rule for triggered events is straightforward and defined directly by the transition rules of programs.
The BasicEvt rule specifies that a basic event occurs when one condition is satisfied by the current state. When a basic event is triggered in event system $\symbcore$, the execution context is changed to the event, and the body begins to be executed.
As shown by the AtomEvt rule, an atomic event behaves like a basic event, but it is atomically executed, i.e. it finishes its execution in a single step.
The execution of a triggered event $\anonevt{\symbprog}$ just simulates the program $\anonevt{\symbprog}$ (TriggeredEvt) and the execution context of the event system is set to None when its execution finishes (TriggeredEvtFin).
The EvtSeq and EvtSeqFin rules specify the behaviour of the sequential composition of two event systems.
The EvtChoice1 and EvtChoice2 rules show a nondeterministic choice between two event systems.
The EvtJoin1 and EvtJoin2 rules show the interleaving of the concurrent execution of two event systems in the interleaving manner.
The execution of $\evtjoin{\symbevtsys_1}{\symbevtsys_2}$ finishes as specified by the EvtParFin rule.
The EvtIterT and EvtIterF rules specify the execution of an event system in a loop manner. The body of an iteration cannot be specified as the termination since it is a semantical notation.
Finally, the Par rule describes behaviour of parallel event systems. The execution of $\symbpes$ is the interleaving of its event systems.
This design relaxes the atomicity of events in other approaches (e.g., Event-B <cit.>).

Environment transition rules (EnvTran_es and EnvTran_pes) have the form $\anyenvtran{\symbspec}{s}{\symbspec}{t}$ where $\symbspec$ is a specification and the subscript $_{\square}$ ($_e$ and $_{pe}$) indicates the transition objects. Intuitively, a transition made by the environment may change the state but not the specification and the execution context.

§.§ Computation

The concept of computation is intended to define the notion of validity using of the operational semantics in the  rely-guarantee proof system.

We define a computation as a sequence of component and environment transitions.

The most intuitively way of describing a computation is by directly using the operational semantics to construct sequence of computations as shown in Figure <ref>. That is, a computation is inductively constructed from an existing computation $(\symbevtsys_2, t)\#cs$ and a environment or component transition from $(\symbevtsys_1,s)$ to $(\symbevtsys_2,t)$. Note that this definition loses the structure of a computation. An alternative equivalent definition for computations takes its structure into account as we show in Figure <ref>. Although it is more elaborated, it can considerably simplify proofs, especially those involving iterative event systems.

In previous versions of  in <cit.>, we use the linear definition of computation and thus the proof of its soundness takes $\approx$ 8,000 lines. By the modular definition, the proof is reduced to $\approx$ 4,200 lines, even though we extend more general constructs for .

§.§.§ Linear Computation

We define the set of computations of all event systems with static information $\symbenv$ as $\compfun(\symbenv)$, which is a set of lists of configurations inductively defined as shown in  <ref>. The singleton list is always a computation (CptsOne). Two consecutive configurations are part of a computation if they are the initial and final configurations of an environment (CptsEnv) or action transition (CptsAct). The operator $\#$ in $e\# l$ represents the insertion of element $e$ in list $l$.

[(, )] ∈() -

(, )#(, t)#cs ∈()

(, t)#cs ∈()

(_1, )#(_2, t)#cs ∈()

_1s_2t     (_2, t)#cs ∈()

Linear Definition of Computation

We use $\compfun(\symbenv,\symbevtsys)$ to denote the set of computations of an event system $\symbevtsys$. The function $\compfun(\symbenv, \symbevtsys, \symbstate)$ denotes the computations of $\symbevtsys$ starting up from an initial state $\symbstate$ and execution context $x$. Computations for parallel event systems are defined in a similar way.

§.§.§ Modular Computation

We define the set of computations of event systems as the lists of configurations in an inductive manner formed by the rules shown in  <ref>. For the modular computation, we use the notation $\compfunm$ instead of $\compfun$.

[(, )] ∈() -

(, )#(, t)#cs ∈()
(, t)#cs ∈()

(, )#(Q, t)#cs ∈()

$\ptran{\symbprog}{\symbstate}{Q}{t} \quad Q \neq \cmdfinal$

$(\anonevt{Q}, t)\#cs \in \compfunm(\symbenv)$

(, )#(Q, t)#cs ∈()

$\ptran{\symbprog}{\symbstate}{Q}{t} \quad Q = \cmdfinal$

$(\anonevt{Q}, t)\#cs \in \compfunm(\symbenv)$

(ev,)#(,)#cs ∈()

$(l,g,P) \in \evtdef{ev} $

$\symbstate \in g \quad (\anonevt{\symbprog},\symbstate)\#cs \in \compfunm(\symbenv)$

(ev,)#(,t)#cs ∈()

$(l,g,P) \in \evtdef{ev} \quad \ptrans{\symbprog}{\symbstate}{\cmdfinal}{t} $

$s \in g \quad (\fin,t,x)\#cs \in \compfunm(\symbenv)$

(_1_2,) # ('_1_2,t) # cs ∈()

$(\evtseq{\symbevtsys'_1}{\symbevtsys_2},t) \# cs \in \compfunm(\symbenv)$

(_1_2,) # (_2,t) # cs ∈()

$(\symbevtsys_2,t) \# cs \in \compfunm(\symbenv) $

(_1_2,) # ('_1,t) # cs ∈()

$(\symbevtsys'_1,t) \# cs \in \compfunm(\symbenv)$

(_1_2,) # ('_2,t) # cs ∈()

$(\symbevtsys'_2,t,y) \# cs \in \compfunm(\symbenv)$

(_1_2,) # ('_1_2,t) # cs ∈()

$(\evtjoin{\symbevtsys'_1}{\symbevtsys_2},t) \# cs \in \compfunm(\symbenv)$

(_1_2,) # (_1'_2,t) # cs ∈()

$(\evtjoin{\symbevtsys_1}{\symbevtsys'_2},t) \# cs \in \compfunm(\symbenv)$

(,) # (,) # cs ∈()
(,) # cs ∈()

(b,) # (,) # cs ∈()
(,) # cs ∈()

(b,) # ( lift-seq-cpt (b)  ((,) # cs) ) ∈()
(,) # cs ∈()

(b,) # ( lift-seq-cpt (b)  ((,) # cs) ) @ (b,t) # cs' ∈()
(,) # cs ∈()
last ((,) # cs)(,t)
(b,t) # cs' ∈()

Modular Definition of Computation

The first two rules are the same as those in the linear definition. The CptsAct rule, however, is now replaced by fourteen rules which correspond to different kinds of component transitions.
The rules in the modular semantics for events and for sequence, choice, and join composition, directly follow the system event operational semantics for each construct as defined in  <ref>.

We explain the detail of the last two rules for iteration. They unfold the iteration into the sequential execution of the event system being iterated.
The CptsMIterTOne rule represents the computations with one iteration, and CptsMIterTMore those where the body has been iteratively executed for more than once. The $last$ function indicates the last element in a list and the “@” function concatenates two lists.

Here, we use an auxiliary function lift-seq-cpt as follows. Given a computation $c$ and an event system $Q$, the function returns the same computation where the specification of each configuration has been sequentially composed with $Q$. The $map$ function applies the transformation (a lambda function) to each element of a list.

\[
\textbf{lift-seq-cpt} \ c \ Q \equiv map \ (\lambda\ (\symbevtsys,\symbstate).\ (\evtseq{\symbevtsys}{Q}, \symbstate))\ c
\]

§.§.§ Equivalence of the Linear and Modular Computations

The following theorem shows the equivalence in  between the linear and modular definitions for computation.

The sets of linear and modular computations are equivalent, i.e. $\compfun(\symbenv) = \compfunm(\symbenv)$.

This theorem is intensively used when proving the soundness of the rely-guarantee proof rules in , especially the proof rule of iteration.
From theorem <ref>, it can be directly inferred that $\compfun(\symbenv,\symbevtsys) = \compfunm(\symbenv,\symbevtsys)$.

§.§ Rely-guarantee Proof System

For compositional reasoning, we propose a rely-guarantee proof system for .
We first introduce the rely-guarantee specification and its validity. Then, we present a set of proof rules and its soundness with regards to the notion of validity.

We consider the verification of two classes of properties in the rely-guarantee proof system of : functional correctness by pre and post conditions and safety by invariants.

§.§.§ Validity

A rely-guarantee specification in  is a quadruple $\rgconddefault$, where $pre$ is the precondition, $rely$ is the rely condition, $guar$ is the guarantee condition, and $post$ is the post condition. The assumption and commitment functions for event systems are denoted by $\assumefun$ and $\commitfun$ respectively. For each computation of an event system $\symbevtsys$, $\symbcomp \in \compfun(\symbenv,\symbevtsys)$, we use $\symbcomp_i$ to denote the configuration at index $i$. $\symbspec_{\symbcomp_i}$ and $\symbstate_{\symbcomp_i}$ represent the projection of each component in the tuple $\symbcomp_i =(\symbspec, \symbstate)$. The $last$ function indicates the last element in a list.

\begin{equation} %\fontsize{8pt}{0cm}
\label{eq:assume_commit}
\begin{aligned}
& \assumefun(\textbf{pre}, \textbf{rely}) \equiv \{\symbcomp \mid \symbstate_{\symbcomp_0} \in \textbf{pre} \wedge (\forall i < len(\symbcomp) - 1. \ (\symbspec_{\symbcomp_i} = \symbspec_{\symbcomp_{i+1}}) \longrightarrow (\symbstate_{\symbcomp_i},\symbstate_{\symbcomp_{i+1}}) \in \textbf{rely})\} \\
& \commitfun(\symbenv, \textbf{guar}, \textbf{post}) \equiv \{\symbcomp \mid \ (\forall i < len(\symbcomp) - 1. \ (\exists \etranlabel.\ \estranconf{\symbcomp_i}{\etranlabel}{\symbcomp_{i+1}}) \longrightarrow (\symbstate_{\symbcomp_i},\symbstate_{\symbcomp_{i+1}}) \in \textbf{guar}) \\
& \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad
\wedge (\symbspec_{last(\symbcomp)} = \fin \longrightarrow \symbstate_{last(\symbcomp)} \in \textbf{post})\}
\end{aligned}
\end{equation}

The validity of rely-guarantee specification for event systems is defined as

\[
\RGSATe{\symbevtsys}{\rgconddefaultb} \equiv \forall \symbstate. \ \compfun(\symbenv, \symbevtsys, \symbstate) \cap \assumefun(\textbf{pre}, \textbf{rely}) \subseteq \commitfun(\symbenv, \textbf{guar}, \textbf{post})
\]

Intuitively, validity represents that the set of computations $cpts$ starting at the configuration $(\symbevtsys, \symbstate)$, with $\symbstate \in \textbf{pre}$ and environment transitions in a computation $cpt \in cpts$ belonging to the rely relation $\textbf{rely}$, is a subset of the set of computations where component transitions belong to the guarantee relation $\textbf{guar}$ and if the event system terminates, then the final states belongs to $\textbf{post}$.
Validity for parallel event systems is defined similarly.

§.§.§ Proof Rules

Now we present the proof rules of  as shown in  <ref>, which give us a relational proof method for CRSs. We first define $\stablefun{f}{g} \equiv \forall x,y. \ x \in f \wedge (x, y) \in g \longrightarrow y \in f$. Thus, $\stablefun{pre}{rely}$ means that the precondition is stable when the rely condition holds. Rules may assume stability of the precondition with regards to the rely relation to ensure that the precondition holds during the environment transitions.
The identity set is denoted as , which is defined as $\{{p \mid \exists x .\ p = (x, x)}\}$. The universal set is denoted as .

We design three forms of proof rules according to the different specification levels: program, event systems, and parallel event systems. They are denoted by:

\begin{equation*} %\fontsize{8pt}{0cm}
\begin{aligned}
(1)\ & \rgsatp{\symbprog}{\rgconddefault} \\
(2)\ & \rgsate{\symbevtsys}{\rgconddefault} \\
(3)\ & \rgsatpe{\symbpes}{\rgconddefault}
\end{aligned}
\end{equation*}

The  framework reuses the proof rules for programs in 3rd-party languages rather than defining them.
We discuss the proof rules for event systems and parallel event systems in detail.

$\forall (l,g,P) \in \evtdef{ev}.\ \rgsatp{\symbprog}{\rgcond{pre \cap g}{rely}{guar}{post}}$

$\stablefun{pre}{rely} \quad \idset \subseteq guar$

$\forall (l,g,P) \in \evtdef{ev}. \forall V.\ \rgsatp{\symbprog}{\rgcond{pre \cap g \cap \{V\}}{\idset}{\univset}{\{s \mid (V,s) \in guar\} \cap post }}$

$\stablefun{pre}{rely} \quad \stablefun{post}{rely}$

$\rgsate{\symbevtsys_1}{\rgcond{pre}{rely}{guar}{mid}} $

_1_2pre_1 ∩pre_2relyguarpost_1 ∩post_2

(1) $\rgsate{\symbevtsys_1}{\rgcond{pre_1}{rely_1}{guar_1}{post_1}}$   (2) $\rgsate{\symbevtsys_2}{\rgcond{pre_2}{rely_2}{guar_2}{post_2}}$

(3) $guar_1 \cup guar_2 \subseteq guar$   (4) $rely \cup guar_2 \subseteq rely_1$   (5) $rely \cup guar_1 \subseteq rely_2$   (6) $\idset \subseteq guar$

inv ∩brelyguarinv
inv ∩ b ⊆post     ⊆guar     invrely     postrely

pre ⊆pre'     rely ⊆rely'     guar' ⊆guar     post' ⊆post

$\forall \symbcore. \ \rgsate{\symbpes(\symbcore)}{\rgcond{Pre(\symbcore)}{Rely(\symbcore)}{Guar(\symbcore)}{Post(\symbcore)}}$
$\forall \symbcore \ \symbcore'. \ \symbcore \neq \symbcore' \longrightarrow Guar(\symbcore) \subseteq Rely(\symbcore')$

$\forall \symbcore. \ pre \subseteq Pre(\symbcore)$   $\forall \symbcore. \ rely \subseteq Rely(\symbcore)$   $\forall \symbcore. \ Guar(\symbcore) \subseteq guar$   $(\bigcap \symbcore. \ Post(\symbcore)) \subseteq post$

Rely-guarantee Proof Rules of

Basic event
As we explained in section <ref>, an event  $\event{\eventdef}$ is composed of the set of all possible instances of $(l,g,P)$ from the parameters domain.
A basic event satisfies its rely-guarantee specification (rule RG-BasicEvt) if all parameter instantiation of the body $P\in \eventdef$ satisfies the specification, strengthening the precondition with the guard of the event. Since the occurrence of a basic event (see the BasicEvt transition rule in  <ref>) does not change the state, the guarantee relation must include the identity relation to accept stuttering transitions.

Atomic event
By the semantics of atomic events, a positive evaluation of its guard and the execution of its body is done atomically. Thus, the state transition caused by the complete execution of $\symbprog$ must satisfy the guarantee condition. This is presented in the pre and post conditions of $\symbprog$ in the assumptions of the RG-AtomEvt rule. We use a universally quantified variable $V$ to relate the state before and after the transformation.
Changes during the execution of $\symbprog$ may arbitrarily modify intermediate states, hence $\symbprog$ must guarantee any possible transition. Thus the guarantee condition is $\univset$.
Since $\symbprog$ is executed atomically, the environment cannot change the state, i.e. the rely condition is the identity relation $\idset$. To ensure that both the pre and post conditions are preserved after environment transitions, we request stability of $pre$ and $post$.

Triggered event
The RG-TrgEvt rule says that a triggered event $\anonevt{\symbprog}$ satisfies the rely-guarantee specification if the program $\symbprog$ satisfies the specification. This rule is directly derived from the semantics for triggered events in  <ref>, where triggered events modify the state according to how the program modifies the state. Note that this rule is not necessary in the proof system, since valid formulas on an event are tackled by  RG-BasicEvt, however we keep it for the sake of completeness.

Sequence of event systems
The rules for the sequential composition (rule RG-Seq) is standard.

Choice of event systems
Regarding the semantics of the Choice of event systems, $\evtchoice{\symbevtsys_1}{\symbevtsys_2}$ behaves as $\symbevtsys_1$ or $\symbevtsys_2$. Therefore, $\evtchoice{\symbevtsys_1}{\symbevtsys_2}$ satisfies the rely-guarantee specification when both $\symbevtsys_1$ and $\symbevtsys_2$ satisfy the specification.

Join of event systems
The concurrent join of two event systems satisfies a rely-guarantee specification if

* The two systems satisfy their specifications (Premise 1 and 2).

* since a component transition of the join is performed by one of its systems, the guarantee condition guar must be at least the union of the guarantee conditions of the two systems (Premise 3);

* An environment transition for one system corresponds to a component transition of another system, or of a transition from the overall environment. Hence, the strongest rely condition for $\symbevtsys_1$ is $rely \cup guar_2$ (Premise 4), and it is the same as for $\symbevtsys_2$ (Premise 5);

* Since the EvtJoinFin rule in  <ref> does not change the state, the guarantee relation must include the identity relation (Premise 6).

* Finally, the pre and post conditions for the join are the intersection of pre and post conditions of the two systems, respectively.

Iteration of event systems
In the RG-Iter rule the precondition plays the role of the invariant; it must hold before and after the execution of the body at every iteration.

Consequence rule
The rule of consequence allows us to strengthen the assumptions and weaken the commitments.

Parallel event systems
The RG-ParEvtSys rule presents the parallel composition of a set of event systems, which are described as a function $\symbpes: \symbCore \rightarrow \symbevtsys$. The premises of this rule are similar to RG-Join, extended to an arbitrary number of parallel event systems.

§.§.§ Soundness

Finally, the soundness theorem for a specification relates rely-guarantee specifications proven on the proof system with its validity.

if  $\rgsate{\symbevtsys}{\rgconddefault}$, then $\RGSATe{\symbevtsys}{\rgconddefault}$.

if  $\rgsatpe{\symbpes}{\rgconddefault}$, then $\RGSATpe{\symbpes}{\rgconddefault}$.

§.§ Invariant Verification

In many cases, we would like to show that CRSs preserve certain data invariants. Since CRSs may not be closed systems, i.e. their environment may change the system state that is represented by rely conditions of CRSs, the reachable states of CRSs are dependent on both the initial states and the environment. The preservation of an invariant on a CRS is defined as follows.

A CRS $\symbpes$ with static information $\symbenv$, starting up from a set of initial states $init$ under an environment $rely$, preserves an invariant $inv$ when its reachable states satisfy the predicate:

\[
\forall \symbcomp.\ \symbcomp \in \compfun(\symbenv, \symbpes) \cap \assumefun(init, rely) \longrightarrow (\forall i<len(\symbcomp).\ inv(s_{\symbcomp_i}))
\]

In this definition, $\symbcomp$ denotes an arbitrary computation of $\symbpes$ from a set of initial states $init$ and under an environment $rely$. It requires that all states in $\symbcomp$ satisfy the invariant $inv$.

To show that $inv$ is preserved by a system $\symbpes$, it suffices to show the invariant verification theorem as follows. This theorem indicates that (1) the system satisfies its rely-guarantee specification $\rgcond{init}{rely}{guar}{post}$, (2) $inv$ initially holds in the set of initial states, and (3) each component transition as well as each environment transition preserves $inv$. Later, by the proof system of , invariant verification is decomposed to the verification of individual events.

For formal specification $\symbpes$ and $\symbenv$, a state set $init$, a rely condition $rely$, and an invariant $inv$, if

* $\rgsatpe{\symbpes}{\rgcond{init}{rely}{guar}{post}}$.

* $init \subseteq \{s \mid inv(s)\}$.

* $\stablefun{\{s \mid inv(s)\}}{rely}$ and $\stablefun{\{s \mid inv(s)\}}{guar}$ are satisfied.

then $inv$ is preserved by $\symbpes$ w.r.t. $\symbenv$, $init$ and $rely$.

§ LANGUAGE INTEGRATION BY ADAPTER PATTERN

parametrizes the language and its rely-guarantee proof system at the program level using a rely-guarantee interface and thus allows to easily reuse existing rely-guarantee frameworks. This reusability is achieved by using an adapter design pattern <cit.>. This section first overviews the idea of language integration. We then present the rely-guarantee interface and its adapters for languages. Finally, we show how the  framework is implemented in Isabelle/HOL.

§.§ Integration Overview

The adapter pattern is a software design pattern that allows the interface of an existing class to be used as another interface <cit.> by defining a separate adapter class that converts the (incompatible) interface of a class (adaptee) into another interface (target) that clients require. It is often used to make existing classes work with others without modifying their source code.

To implement a flexible integration of languages used for the definition of the event bodies,  provides a rely-guarantee interface that program languages respect. The interface is an abstraction for common rely-guarantee components required by . These components are represented as a set of parameters and their assumptions. The language, semantics, proof rules and soundness proof of  in  <ref> are developed using this interface. The architecture of language integration into  is shown in  <ref>.

Languages Integration in

When integrating a 3rd-party language into , the language is the adaptee, and the rely-guarantee interface is the target. It is necessary to provide a rely-guarantee adapter to bridge the differences of rely-guarantee components between  and the language. The adapter implements the rely-guarantee interface by delegating functionality of the event language to the integrated language.
Following this adapter, a 3rd-party language and its rely-guarantee proof systems are integrated into  as a new instance. Since these languages may have been developed independently from , they are not necessarily completely consistent with the  interface.
This architecture makes it possible to integrate existing languages without modifying their specification, semantics, and rely-guarantee proof system.

§.§ Rely-guarantee Interface and Adapter

The rely-guarantee interface requires specifications and assumptions for four differentiated elements: language definition (syntax and semantics), rely-guarantee definitions (validity), rely-guarantee proof rules, and their soundness.
The detailed information is discussed as follows.

* interface types: they are data types used by the parameters. These are the types of the program, the program state and the static configuration for programs.

* interface parameters and types:
as a parametric framework,  does not define the syntax for the languages used in event bodies. However, it requires the representation for program termination, which is denoted as $\cmdfinal$ in  (Parameter 1 in  <ref>).
also needs the transition relation representing the program language semantics (Parameters 2). Moreover, the interface requires the components related to the validity of a rely-guarantee specification (Parameter 3) and the proof rules (Parameter 4).

* interface assumptions:
to reason about event behaviours,  assumes that

* The program $\cmdfinal$ cannot take a step to another state (Assumption 1 in  <ref>).

* if a program $\symbprog$ takes a component transition, $\symbprog$ is changed in the next configuration (Assumption 2).

* the definition of the validity is similar to those in , and are relaxed to be not necessarily equivalent (Assumption 3).

* the validity is usually defined by three functions, i.e. computation ($\compfun(\symbenv,\symbprog,\symbstate)$), assumption ($\assumefun_p(pre,rely)$) and commitment ($\commitfun_p(\symbenv, guar,post)$). The functions have the same form as of those in  <ref> (Page eq:assume_commit) by using the program transition relation (Parameter 2).  requires that the rely-guarantee proof rules in languages are sound (Assumption 4).

Parameters and Their Assumptions of

No.     Parameter     Notation of Parameter     Assumption of Parameter

(1)     Terminal statement     $\cmdfinal$     2*l(1) $\neg(\ptran{\cmdfinal}{s}{P}{t})$
(2) $\neg(\ptran{P}{s}{P}{t})$

(2)     Program transition     $\ptran{P}{s}{Q}{t}$

(3)     Validity     $\RGSATp{\symbprog}{\rgconddefault}$
l(3) $\RGSATp{\symbprog}{\rgconddefault}$
$\Longrightarrow \forall \symbstate.\ \compfun(\symbenv,\symbprog,\symbstate) \cap \assumefun_p(pre,rely)$
$\quad \quad \quad \quad \quad \subseteq \commitfun_p(\symbenv, guar,post)$

(4)     Proof rule     $\rgsatp{P}{\rgconddefault}$     l(4) $\rgsatp{P}{\rgconddefault}$
$\Longrightarrow \RGSATp{\symbprog}{\rgconddefault}$

The rely-guarantee adapter for a concrete language implements the rely-guarantee interface by delegating the functionality of the event language to the integrated language.
In the adapter, we first need to instantiate the interface types to be adapter types.
For each interface parameter, there is a corresponding definition (or function) in the adapter to instantiate the parameter.
Moreover, the adapter provides the necessary set of adapter conclusions (lemmas and theorems) to show that it satisfies the interface assumptions.

§.§ Isabelle/HOL Implementation

In the mechanized implementation of  in Isabelle/HOL, we design a set of hierarchical locales, where the final locale is shown in  <ref>.
The interface types are represented as ${\isacharprime}prog$ for the type of programs, ${\isacharprime}s$ for the type of program states, and ${\isacharprime}Env$ for the type of static configuration for programs represented by $\symbenv$.
The four interface parameters are represented as $fin{\isacharunderscore}com$, $ptran$, $prog{\isacharunderscore}validity$ and  $rghoare{\isacharunderscore}p$ respectively. The four interface assumptions are represented as $none{\isacharunderscore}no{\isacharunderscore}tran{\isacharprime}$, $ptran{\isacharunderscore}neq$, $prog{\isacharunderscore}validity{\isacharunderscore}def$ and $rgsound{\isacharunderscore}p$ respectively.

sprog pconf  prog  s

locale PiCore

fixes fincom  prog

fixes ptran  Env  sprog pconf  sprog pconf set

fixes progvalidity  Env  prog  s set  s  s set  s  s set  s set  bool

fixes rghoarep  Env  prog s set s  s set s  s set s set  bool

assumes nonenotran fincom sPt  ptran

assumes ptranneq P sPt  ptran

assumes progvaliditydef   P satp pre rely guar post

s0 cptsfrom ptran  Ps0  assume pre rely  commit ptran  fincom guar post

assumes rgsoundp   P satp pre rely guar post    P satp pre rely guar post

......  // we omit here the  implementation using parameters and assumptions.

Isabelle/HOL Implementation of  Rely-guarantee Interface

Finally, the interpretation of the  locale is shown as follows, where finI, ptranI, validityI and rghoareI are adapter parameters of a concrete language $I$ passed to the locale. The interpretation command in Isabelle will generate proof goals showing the satisfaction of assumptions.

\isacommand{interpretation} \ {\slang} \ finI \ ptranI \ validityI \ rghoareI

§ INTEGRATING CONCRETE LANGUAGES

Using the  framework and its Isabelle/HOL implementation, the remaining work to integrate a concrete language is to design its adapter.  We have created two  instances by interpreting the  locale using adapters for  and . This section presents the two adapters, together with an overview of the integrated language for each adapter.

§.§ : Integrating  Language

§.§.§  Overview

The  language and its rely-guarantee proof system are presented in detail in <cit.>.
The abstract syntax of  is defined as in  <ref> in terms of states, of type ${\isacharprime}s$; a set of fault types, of type ${\isacharprime}f$; a set of procedure names of type ${\isacharprime}p$, and a set of simulation events ${\isacharprime}e$.

In order to capture all aspects of abrupt termination, assertions, and function calls, the program state in  is modelled as a datatype $xstate$, which is composed of four different constructors to represent a regular execution, a failed assertion, an exceptional state and a state where a call to a non-defined function is made.
Type $({\isacharprime}s,{\isacharprime}p,{\isacharprime}f,{\isacharprime}e)\ config$ defines the configuration used in its transition semantics and $({\isacharprime}s,{\isacharprime}p,{\isacharprime}f,{\isacharprime}e)\ body$ denoted as an environment $\csimplprocenv$ defines the procedure declarations as a partial function from the set ${\isacharprime}p$ of procedure names to the body of the procedures. $({\isacharprime}s,{\isacharprime}p,{\isacharprime}f,{\isacharprime}e)\ confs$ defines the type of computations. To support reasoning about procedure invocations,  uses the notation $\csimplprocrg$ to maintain the rely-guarantee specification for procedures. The validity in  requires that each procedure in $\csimplprocrg$ satisfies its specification.

s p f e com
Skip  Throw  Basic  s  s  e option    Spec  s  s set   e option

Seq  s p f e com  s p f e com  Await  s bexp  e option   s p f e com

Cond  s bexp  s p f e com   s p f e com

While  s bexp  s p f e com  Call  p
DynCom  s  s p f e com

Guard  f  s bexp  s p f e com
Catch s p f e com  s p f e com

sf xstate  Normal s  Abrupt s  Fault f  Stuck

s p f e config  s p f ecom   sf xstate

s p f e body  p  s p f e com option

spfe confs  spfe body spfe config list

Syntax and State Definition of the  Language in Isabelle/HOL <cit.>

§.§.§ Rely-guarantee Adapter for

Instantiating the interface types in  is straightforward. The interface type of programs ${\isacharprime}prog$ is implemented as type ${\isacharparenleft}{\isacharprime}s{\isacharcomma}\ {\isacharprime}p{\isacharcomma}\ {\isacharprime}f{\isacharcomma}\ {\isacharprime}e{\isacharparenright}\ com$, and interface type of program state ${\isacharprime}s$ as type ${\isacharparenleft}{\isacharprime}s{\isacharcomma}{\isacharprime}f{\isacharparenright}\ xstate$.
The procedure declarations $\csimplprocenv$ and their rely-guarantee specification $\csimplprocrg$ are the static configuration of . Thus, we use type $\csimplprocenv \times \csimplprocrg$ to instantiate the environment ${\isacharprime}Env$ in .

The interface parameter of the terminal statement is instantiated as the $Skip$ command in .
The program transition in  is defined as $\csimpltran{P}{s}{Q}{t}$.
The interface parameter of program transition is instantiated as $(\Gamma,\Theta) \vdash_{cI} (P,s) \rightarrow (Q,t) \equiv \csimpltran{P}{s}{Q}{t}$ by delegating it to the  semantics.

Instantiating the interface parameter of the validity has to consider the computation, assumption and commitment functions. The validity function in  is shown in  <ref>. The rely-guarantee specification in  is in the form $\rgcond{pre}{rely}{guar}{(q,a)}$ with a set of Fault states $F$, where the postcondition $(q,a)$ is a pair of state sets. The set $q$ constrains the final state if the program terminates as Skip representing a normal state, whilst $a$ constrains abrupt terminations in an exception with the command Throw. The set $F$ constrains that the final state of the program should not be in Fault states in $F$.
For procedure invocations,  defines another validity function using the general one, which also requires that each procedure satisfies its rely-guarantee specification.

First, the computation function in  is defined by using the program transition and the environment transition. As discussed above, the program transition of  is adapted straightforwardly.
semantics for programs can transit from a Normal state to a different type. However, it does not allow transitions from a non Normal state to any other state.
Therefore, the environment transition in  is defined as follows.
To adapt the restricted environment transition, we first define the environment transition in the adapter as $(\Gamma,\Theta) \vdash_{cI} (P, s) \rightsquigarrow (Q,t) \equiv P = Q$, which allows any state transition and is compatible with that in the rely-guarantee interface. Then, we restrict the rely condition in the definition of proof rules in the adapter to bridge this difference, which will be discussed later. Based on the transition functions, the computation function $\compfun$ of the adapter is defined in the same form as in .

\[
\left\{
\begin{aligned}
& \csimplenvtran{P}{Normal\ s}{P}{t} \\
& (\forall t'.\ t \neq Normal\ t') \Longrightarrow \csimplenvtran{P}{t}{P}{t}
\end{aligned}
\right.
\]

Second, the validity of  only concerns the preconditions over Normal states. Thus, the assumption function of  as shown in  <ref> restricts the starting state of a computation to Normal.
For type consistency,  does not impose that restriction, but rather it is enforced by the adapter to bridge the difference. So in the adapter, we define the assumption function as the same as in . Then, we restrict the precondition in the definition of proof rules in the adapter, which will be discussed later.

assum pre,  rely  c sndsnd c0  Normal  pre  i Suc ilength snd c

fst ccsnd ci  $\rightsquigarrow$ snd cSuc i sndsnd ci sndsnd cSuc i   rely

comm guar qa F   c snd last snd c  Fault  F   i Suc ilength snd c

fst ccsnd ci   snd cSuc i  sndsnd ci sndsnd cSuc i  guar

final last snd c   fst last snd c  Skip  snd last snd c  Normal  q

fst last snd c  Throw  snd last snd c  Normal  a

F Pr sat pre rely guar qa  s cp  Pr s  assumpre rely  commguar qa F

F Pr sat pre rely guar qa

cpRGqa   F Call c sat p R G qa  F Pr sat pre rely guar qa

The Validity in the  Language in Isabelle/HOL <cit.>

Third, referring to semantics of the final state in the validity of , the commitment function in  is defined as shown in  <ref>.  does restrict the final statement to Skip, thus exceptions have to be handled at the program level. In the adapter, we define the same commitment function as in . Then, we restrict the postcondition in the definition of proof rules in the adapter, which will be discussed later.

Finally, the validity parameter of the  adapter is define as $({\isasymGamma},{\isasymTheta})\ {\isasymTurnstile}\isactrlsub I\ P\ sat\isactrlsub p\ {\isacharbrackleft}pre{\isacharcomma}\ rely{\isacharcomma}\ guar{\isacharcomma}\ q{\isacharbrackright}$, which has the same form as in the rely-guarantee interface.

Considering the interface parameter of the proof rule, based on the definition of proof rules  F P sat pre rely guar qa in , we adapt proof rules as follows. (1) The validity in  only concerns preconditions of Normal states, so we restrict the precondition $pre$ to Normal. (2) Programs of an event body cannot throw exceptions to the event level, so final states when reaching the final statement Skip are Normal. Thus, we restrict the postcondition $q$ to Normal. (3) Events assume the normal execution of their program body, and furthermore the program cannot fall into a Fault state. So we assume the Fault set $F$ to be empty. In addition, the program $P$ should satisfy its rely-guarantee specification in . The abrupt postcondition is set to False, to ensure that the CSimpl program never ends in an exceptional state. (4) The environment transition in  does not allow transitions from a non Normal state to a different 	state, we represent it in the rely condition $rely$. (5) Finally, the rely-guarantee specification for each procedure in $\Theta$ has to be satisfied.

(,) I P satp pre rely guar q
$\overbrace{\text{{\isacharparenleft}pre\ {\isasymsubseteq}\ Normal\ {\isacharbackquote}\ UNIV{\isacharparenright}}}^{(1)}$
$\overbrace{\text{{\isacharparenleft}q\ {\isasymsubseteq}\ Normal\ {\isacharbackquote}\ UNIV{\isacharparenright}}}^{(2)}$

$\overbrace{\text{{\isacharparenleft}{\isasymGamma}{\isacharcomma}{\isasymTheta}\ {\isasymturnstile}\isactrlbsub {\isacharslash}{\isacharbraceleft}{\isacharbraceright}\isactrlesub \ P\ sat\ {\isacharbrackleft}{\isacharbraceleft}s $\mid$ Normal\ s\ {\isasymin}\ pre{\isacharbraceright}{\isacharcomma}\ rely{\isacharcomma}\ guar{\isacharcomma}\ {\isacharbraceleft}s $\mid$ Normal\ s\ {\isasymin}\ q{\isacharbraceright}{\isacharcomma}\ \{\ \} {\isacharbrackright}{\isacharparenright}}}^{(3)}$

$\overbrace{\text{{\isacharparenleft}{\isasymforall}{\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}rely{\isachardot}\ s\ {\isasymnotin}\ Normal\ {\isacharbackquote}\ UNIV\ {\isasymlongrightarrow}\ s\ {\isacharequal}\ t{\isacharparenright}}}^{(4)}$

$\overbrace{\text{{\isacharparenleft}{\isasymforall}{\isacharparenleft}c{\isacharcomma}p{\isacharcomma}R{\isacharcomma}G{\isacharcomma}q{\isacharcomma}a{\isacharparenright}{\isasymin}\ {\isasymTheta}{\isachardot}\ {\isasymGamma}{\isacharcomma}{\isacharbraceleft}{\isacharbraceright}\ {\isasymturnstile}\isactrlbsub {\isacharslash}{\isacharbraceleft}{\isacharbraceright}\isactrlesub \ {\isacharparenleft}Call\ c{\isacharparenright}\ sat\ {\isacharbrackleft}p{\isacharcomma}\ R{\isacharcomma}\ G{\isacharcomma}\ q{\isacharcomma}a{\isacharbrackright}{\isacharparenright}}}^{(5)}$

As we discuss the adapter parameters of , it is straightforward to show that the first three interface assumptions ( <ref>) are satisfied in the adapter. To show the fourth assumption, it is enough to prove that

(,) I P satp pre rely guar q $\Longrightarrow$ (,) I P satp pre rely guar q

§.§ : Integrating  Language

§.§.§  Overview

is a simple imperative language with a rely-guarantee proof system <cit.> provided by the Hoare_Parallel library of Isabelle/HOL. We briefly overview the language since we will use it and its  instance for the case studies later.
The abstract and concrete syntax of  is shown as follows. Since there is no terminal statement in the abstract syntax, the configuration used in the semantics of  is defined as ${\isacharparenleft}{\isacharparenleft}{\isacharprime}s\ com{\isacharparenright}\ option{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}s$. The terminal statement is denoted as the Isabelle/HOL construct None. However, the proof rules of  denoted as $\rgsat{P}{\rgcond{pre}{rely}{guar}{post}}$ still use the program $P$ of type ${\isacharprime}s\ com$.

s com
Basic s  s

Seq s com s com

Await s bexp s com
AWAIT  THEN  END

Cond s bexp s com  s com
IF  THEN  ELSE FI

While s bexp s com
WHILE  DO  OD

s conf  s com option  s

§.§.§ Rely-guarantee Adapter for

In the  adapter, we use ${\isacharparenleft}{\isacharprime}s\ com{\isacharparenright}\ option$ to instantiate the interface type of programs ${\isacharprime}prog$. Since there is no static information $\symbenv$ in , we omit this information in the program transition and validity of the adapter.
We define the proof rules as $\rgsatpI{(Some \ P)}{\rgcond{pre}{rely}{guar}{post}}$ using the original  proof rules and thus reuse all of soundness proofs to prove the interface assumption (4) in  <ref> (Page tbl:interface).
Other definitions of rely-guarantee components in  respect to the  interface are straightforward, and we omit the details here. The interested reader can refer to the Isabelle/HOL sources.

§ FORMAL VERIFICATION OF CONCURRENT MEMORY MANAGEMENT

Aiming at the highest evaluation assurance level (EAL 7) evaluation of Common Criteria (CC) <cit.>, we develop a low-level design specification of the Zephyr concurrent memory management by using , the instance of  for the  language. The specification closely follows the Zephyr C code, and thus is able to do the code-to-spec review required by the EAL 7 evaluation, covering all the data structures and imperative statements present in the implementation.

The verification conducted in this case study is on Zephyr v1.8.0, released in 2017. The C code of the buddy memory management is $\approx$ 400 lines, not counting blank lines and comments. During the formal verification, we found 3 bugs in the C code of Zephyr: an incorrect block split, an incorrect return, and non-termination of a loop in the k_mem_pool_alloc service.
The first two bugs are critical and have been repaired in the latest release of Zephyr.

has support for concurrent OS kernels features like modelling shared-variable concurrency of multiple threads, interruptable execution of handlers, self-suspending threads, and rescheduling.
An OS kernel can be considered as a CRS of peer reaction structure. It makes an initialization and enters in an idle loop until it receives an interruption which is handled by an interrupt handler. After finishing the execution of the handler, the OS kernel returns to the idle loop waiting for new interruptions.
OS kernels may provide a large number of services to applications. The peer reaction construct in  can easily model the behaviour of OS kernels.

§.§ Concurrent Buddy Memory Management of Zephyr

In Zephyr, a memory pool is a kernel object that allows memory blocks to be dynamically allocated, from a designated memory region, and released back into the pool. Its definition in the C code is shown as follows.
A memory pool's buffer ($*buf$) is an $n\_max$-size array of blocks of $max\_sz$ bytes at level $0$, with no wasted space between them. The size of the buffer is thus $n\_max \times max\_sz$ bytes long. Zephyr tries to accomplish a memory request by splitting available blocks into smaller ones fitting as best as possible the requested size.
Each “level 0” block is a quad-block that can be split into four smaller “level 1” blocks of equal size. Likewise, each level 1 block is itself a quad-block that can be split again. At each level, the four smaller blocks become buddies or partners to each other. The block size at level $l$ is thus $max\_sz / 4 ^ l$.

struct k_mem_block_id
u32_t pool : 8;
u32_t level : 4;
u32_t block : 20;
struct k_mem_pool_lvl
u32_t *bits_p;
u32_t bits;
sys_dlist_t free_list;

struct k_mem_block
void *data;
struct k_mem_block_id id;
struct k_mem_pool
void *buf;
size_t max_sz;
u16_t n_max;
u8_t n_levels;
u8_t max_inline_level;
struct k_mem_pool_lvl *levels;
_wait_q_t wait_q;

The pool is initially configured with the parameters  $n\_max$ and $max\_sz$, together with a third parameter $min\_sz$. $min\_sz$ defines the minimum size for an allocated block and must be at least $4 \times X$ ($X > 0$) bytes long. Memory pool blocks are recursively split into quarters until blocks of the minimum size are obtained, at which point no further split can occur.
The depth at which $min\_sz$ blocks are allocated is $n\_levels$ and satisfies that $n\_max = min\_sz \times 4 ^ {n\_levels}$.

Every memory block is composed of a $level$; a $block$ index within the level, ranging from $0$ to $(n\_max \times 4 ^ {level}) - 1$; and the $data$ representing the block start address, which is equal to $buf + (max\_sz / 4 ^ {level}) \times block$. We use a tuple $(level, block)$ to uniquely represent a block within a pool $p$.

A memory pool keeps track of how its buffer space has been split using a linked list free_list with the start address of the free blocks in each level. To improve the performance of coalescing partner blocks, memory pools maintain a bitmap at each level to indicate the allocation status of each block in the level.  This structure is represented by a C union of an integer bits and an array bits_p. The implementation can allocate the bitmaps at levels smaller than $max\_inlinle\_levels$ using only an integer bits. However, the number of blocks in levels higher than $max\_inlinle\_levels$ make necessary to allocate the bitmap information using the array bits_map.
In such a design, the levels of bitmaps actually form a forest of complete quadtrees.
The bit $i$ in the bitmap of level $j$ is set to $1$ for the block $(i,j)$ iff it is a free block, i.e. it is in the free list at level $i$. Otherwise, the bitmap for such block is set to $0$.

static int pool_alloc(struct k_mem_pool *p,struct k_mem_block *block,size_t size)

..... //calcuate lsizes[], alloc_l and free_l
if (alloc_l < 0 || free_l < 0)
block->data = NULL;
return -ENOMEM;

blk = alloc_block(p, free_l, lsizes[free_l]);
if (!blk)  return -EAGAIN;
/* Iteratively break the smallest enclosing block... */
for (from_l = free_l; level_empty(p, alloc_l)        from_l < alloc_l;
blk = break_block(p, blk, from_l, lsizes);

block->id.level = alloc_l; //assign block level to the variable *block
......  //assign other block info to the variable *block
return 0;

int k_mem_pool_alloc(struct k_mem_pool *p, struct k_mem_block *block, size_t size, s32_t timeout)

...... // initialize local vars, calculate the end time for timeout.
while (1)
ret = pool_alloc(p, block, size);
if (ret == 0 || timeout == K_NO_WAIT ||
ret == -EAGAIN || (ret        ret != -ENOMEM))
return ret;

key = irq_lock();
_pend_current_thread(   p->wait_q, timeout);
...... //if timeout > 0, break the loop if time out

return -EAGAIN;

The C Source Code of Memory Allocation in Zephyr v1.8.0

Zephyr provides two kernel services k_mem_pool_alloc and k_mem_pool_free, for memory allocation and release respectively.
The main part of the C code of k_mem_pool_alloc is shown in  <ref>.
When an application requests for a memory block, Zephyr first computes $alloc\_l$ and $free\_l$. $alloc\_l$ is the level with the size of the smallest block that will satisfy the request, and $free\_l$, with $free\_l \leqslant alloc\_l$, is the lowest level where there are free memory blocks. Since the services are concurrent, when the service tries to allocate a free block blk from level $free\_l$ (Line 8), blocks at that level may be allocated or merged into a bigger block by other concurrent threads. In such case, the service will back out (Line 9) and tell the main function k_mem_pool_alloc to retry. If $blk$ is successfully locked for allocation, then it is broken down to level $alloc\_l$ (Lines 11 - 14).
The allocation service k_mem_pool_alloc supports a timeout parameter to allow threads waiting for that pool for a period of time when the call does not succeed. If the allocation fails (Line 24) and the timeout is not K_NO_WAIT, the thread is suspended (Line 30) in a linked list wait_q, and the context is switched to another thread (Line 31).

Interruptions are always enabled in both services with the exception of the code for the functions alloc_block and break_block, which invoke irq_lock and irq_unlock  to respectively enable and disable interruptions.
Similar to k_mem_pool_alloc, the execution of k_mem_pool_free is interruptable too.

§.§ Defining Structures and Properties of Buddy Memory Pools

As a specification at the design level, we use abstract data types to represent the complete structure of memory pools.
We use an abstract reference ref in Isabelle to define pointers to memory pools. Starting addresses of memory blocks, memory pools, and unsigned integers in the implementation are defined as natural numbers (nat). Linked lists used in the implementation for the elements levels and free_list, together with the bitmaps used in bits and bits_p, are defined as a list type.
C structs are modelled in Isabelle as records of the same name as the implementation and comprising the same data. There are two exceptions to this: (1) $k\_mem\_block\_id$ and $k\_mem\_block$ are merged in one single record, (2) the union in the struct $k\_mem\_pool\_lvl$ is replaced by a single list representing the bitmap, and thus max_inline_level is removed.

Structure of Memory Pools

The Zephyr implementation makes use of a bitmap to represent the state of a memory block. The bit $j$ of the bitmap for level a $i$ is set to $1$ iff the memory address of the memory block $(i,j)$ is in the free list at level $i$. A bit $j$ at a level $i$ is set to $0$ under the following conditions: (1) its corresponding memory block is allocated (ALLOCATED), (2) the memory block has been split (DIVIDED), (3) the memory block is being split in the allocation service (ALLOCATING) (Line 13 in  <ref>), (4) the memory block is being coalesced in the release service (FREEING), and (5) the memory block does not exist (NOEXIST). Instead of only using a binary representation, our formal specification models the bitmap using a datatype BlockState that is composed of these cases together with FREE. The reason for this decision is to simplify proving that the bitmap shape is well-formed. In particular, this representation makes it less complex to verify the case in which the descendant of a free block is a non-free block. This is the case where the last free block has not been split, and therefore lower levels do not exist.
We illustrate the structure of a memory pool in  <ref>. The top of the figure shows the real memory of the first block at level $0$.

The structural properties clarify the constraints on and consistency of quadtrees, free block lists, the memory pool configuration, and waiting threads. All of them are thought of as invariants on the kernel state and have been formally verified on the formal specification in Isabelle/HOL.

Well-shaped bitmaps.
We say that the logical memory block $j$ at a level $i$ physically exists iff the bitmap $j$ for the level $i$ is ALLOCATED, FREE, ALLOCATING, or FREEING, represented by the predicate $is\_memblock$. We do not consider blocks marked as DIVIDED as physical blocks since it is only a logical block containing other blocks.
Threads may split and coalesce memory blocks. A valid forest is defined by the following rules: (1) the parent bit of an existing memory block is DIVIDED and its child bits are NOEXIST, denoted by the predicate $noexist\_bits$ that checks for a given bitmap $b$ and a position $j$ that nodes $b!j$ to $b!(j+3)$ are set as NOEXIST; (2) the parent bit of a DIVIDED block is also DIVIDED; and (3) the child bits of a NOEXIST bit are also NOEXIST and its parent can not be a DIVIDED block. The property is defined as the predicate invbitmap($s$), where $s$ is the state.

There are two additional properties on bitmaps. First, the address space of any memory pool can not be empty, i.e., the bits at level 0 have to be different from NOEXIST. Second, the allocation algorithm may split a memory block into smaller ones, but not those blocks at the lowest level (i.e. level $n\_levels - 1$); therefore the bits at the lowest level cannot not be DIVIDED. The first property is defined as invbitmap0($s$) and the second as invbitmapn($s$).

Consistency of the memory configuration.
The configuration of a memory pool is set when it is initialized. Since the minimum block size is aligned to 4 bytes, there must exist an $n > 0$ such that the maximum size of a pool is equal to $4 \times n \times 4 ^ {n\_levels}$, relating the number of levels of a level 0 block with its maximum size. Moreover, the number of blocks at level 0 and the number of levels have to be greater than zero, since the memory pool cannot be empty. The number of levels is equal to the length of the  pool $levels$ list. Finally, the length of the bitmap at level $i$ should be $n\_max \times 4 ^ i$. This property is defined as invmempoolinfo($s$).

Memory partition property.
Memory blocks partition the pool they belong to, in this context, there are two critical properties that the allocation and release of blocks must preserve: the absence of any overlapping blocks and the absence of memory leaks. For a memory block of index $j$ at level $i$, its address space is the interval $[j \times (max\_sz / 4 ^ i), (j + 1) \times (max\_sz / 4 ^ i))$. For any relative memory address $addr$ in the memory domain of a memory pool, and hence $addr < n\_max * max\_sz$, there is one and only one memory block whose address space contains $addr$. Here, we use relative address for $addr$.  The property is defined as mempart(s).

From the invariants of the bitmap, we derive the general property for the memory partition.

For any kernel state $s$, If the memory pools in $s$ are consistent in their configuration, and their bitmaps are well-shaped, the memory pools satisfy the partition property in $s$:

\[
\textbf{inv\_mempool\_info}(s) \wedge \textbf{inv\_bitmap}(s) \wedge \textbf{inv\_bitmap0}(s) \wedge \textbf{inv\_bitmapn}(s) \Longrightarrow \textbf{mem\_part}(s)
\]

Together with the memory partition property, pools must also satisfy the following:

No partner fragmentation.
The memory release algorithm in Zephyr coalesces free partner memory blocks into blocks as large as possible for all the descendants from the root level, without including it. Thus, a memory pool does not contain four FREE partner bits.

Validity of free block lists.
The free list at one level keeps the starting address of free memory blocks. The memory management ensures that the addresses in the list are valid, i.e., they are different from each other and aligned to the block size, which at a level $i$ is given by ($max\_sz / 4 ^ i$).
Moreover, a memory block is in the free list iff the corresponding bit of the bitmap is FREE.

Non-overlapping of memory pools.
The memory spaces of the set of pools defined in a system must be disjoint, so the memory addresses of a pool do not belong to the memory space of any other pool.

Other properties.
The state of a suspended thread in wait_q has to be consistent with the threads waiting for a memory pool. Threads can only be blocked once, and those threads waiting for available memory blocks have to be in a BLOCKED state.
During allocation and free of a memory block, blocks of the tree may temporally be manipulated during the coalescing and division process. Only one thread can manipulate a give bloack at a time, and the state bit of a block being temporally manipulated has to be FREEING or ALLOCATING.

§.§ Formalizing Zephyr Memory Management

§.§.§ Event-based Execution Model of Zephyr

An Execution Model of Zephyr Memory Management

As shown in  <ref> (a), if we do not consider its initialization, an OS kernel can be seen as a reactive system that is in an idle loop until it receives an interruption (e.g. syscalls, timer interrupts) which is handled by an interruption handler.
Whilst interrupt handlers execution is atomic in sequential kernels, it can be interrupted in concurrent kernels <cit.> allowing services invoked by threads to be interrupted and resumed later.
In the execution model of Zephyr, we consider a scheduler $\mathcal{S}$ and a set of threads $t_1, ..., t_n$. In this model, the execution of the scheduler is atomic since kernel services can not interrupt it. But kernel services can be interrupted via the scheduler, i.e., the execution of a memory service invoked by a thread $t_i$ may be interrupted by the kernel scheduler to execute a thread $t_j$. <ref> (b) illustrates the Zephyr execution model, where solid lines represent execution steps of the threads/kernel services and dotted lines mean the suspension of the thread/code. For instance, the execution of k_mempool_free in thread $t_1$ is interrupted by the scheduler, and the context is switched to thread $t_2$ which invokes k_mempool_alloc. During the execution of $t_2$, the kernel service may suspend the thread and switch to another thread $t_n$ by calling rescheduling. Later, the execution is switched back to $t_1$ and continues the execution of k_mempool_free in a different state from when it was interrupted.

Each user thread $t_i$ invokes the allocation and release services; thus the event system for $t_i$ is

\begin{equation*}
\begin{aligned}
esys_{t_i} \equiv & \evtrec{\mathbf{True}}{((\stmtevthead{mem\_pool\_free}{blk}{t_i})} \\
& \quad \quad \quad\ \ \symbchoice (\stmtevthead{mem\_pool\_alloc}{p,sz,tmout}{t_i}))
\end{aligned}
\end{equation*}

which is the iteration of alloc or free events, where the input parameters for these events correspond with the arguments of the service implementation in the C code.
Events are parametrized by a thread identifier $t_i$ used to control access to the execution context of the thread invoking it.
Together with threads, we model the event service for the scheduler $esys_{sched}$ consisting of a unique event sched whose argument is a thread $t$ to be scheduled when it is in the READY state.
The formal specification of the memory management is thus defined as follows, which is much simpler than the specification obtained from a non-event oriented language.

\[
Kernel\_Spec \equiv \lambda \symbcore. \ \textbf{case} \ \symbcore \ \textbf{of} \ (\isasymT \ t_i)\ \isasymRightarrow\ esys_{t_i} \ \isacharbar \ \textbf{sched} \ \isasymRightarrow\ esys_{sched}
\]

The execution of a service executed by a thread can be stopped by the scheduler to be resumed later. This behaviour is modelled by using a global variable $cur$ that indicates the thread being currently has been scheduled and is being executed, and conditioning the execution of parametrized events in $t$ only when $t$ is scheduled. This is achieved by using the expression

\[ \stmtirq{t}{p} \equiv \stmtawait{cur = t}{p}\]

so an event invoked by a thread $t$ only progresses when $t$ is scheduled. This scheme allows using rely-guarantee for concurrent execution of threads on mono-core architectures, where only the scheduled thread is able to modify the memory.

§.§.§ Specification of Memory Management Services

The C code of Zephyr uses the recursive function free_block to coalesce free partner blocks and the break statement to stop the execution of a loop statements, which are not supported by the  language in . The formal specification overcomes this by transforming the recursion into a loop controlled by the recursion condition, and using a control variable to exit loops with breaks when the condition to execute the loop break is satisfied.
The memory management services use the atomic body irq_lock(); P; irq_unlock(); to keep interruption handlers reentrant by disabling interruptions.
We simplify this behaviour in the specification using an ATOM statement, avoiding that the service is interrupted at that point. The rest of the formal specification closely follows the implementation, where variables are modified using higher order functions changing the state as the code does it. The reason for using Isabelle/HOL functions is that  does not provide a semantic for expressions, using instead state transformer relying on high order functions to change the state.

1  WHILE freeblockr t DO  2    t   lsz  lsz t  lsizes t  lvl t  3    t   blk  blk t  blockptr mempoolinfo pool b lsz t bn t  4    t   ATOM  5      mempoolinfo  setbitfree mempoolinfo pool b lvl t bn t  6      freeingnode  freeingnode t  None  7      IF lvl t  0  partnerbits mempoolinfo pool b lvl t bn t THEN  8        FOR i  it  0 i t  4 i  it  i t  1 DO  9          bb  bb t  bn t div 4  4  i t10          mempoolinfo  setbitnoexist mempoolinfo pool b lvl t bb t11          blockpt  blockpt t  blockptr mempoolinfo pool b lsz t bb t12          IF bn t  bb t  blockfits mempoolinfo pool b blockpt t lsz t THEN13            mempoolinfo  mempoolinfo pool b  14                removefreelist mempoolinfo pool b lvl t blockpt t15          FI16        ROF17        lvl  lvl t  lvl t  118        bn  bn t  bn t div 419        mempoolinfo  setbitfreeing mempoolinfo pool b lvl t bn t20        freeingnode  freeingnode t  Some pool  pool b level  lvl t 21                      block  bn t
data  blockptr mempoolinfo pool b 22                         ALIGN4 maxsz mempoolinfo pool b div 4  lvl t
bn t 23      ELSE24        IF blockfits mempoolinfo pool b blk t lsz t THEN25          mempoolinfo  mempoolinfo pool b  26            appendfreelist mempoolinfo pool b lvl t blk t 27        FI28        freeblockr  freeblockr t  False29      FI30    END31  OD

The  Specification of free_block

<ref> illustrates the  specification of the free_block function invoked by k_mem_pool_free when releasing a memory block.
We refer readers to  <ref> for the main part of the C code of the k_mem_pool_free service and  <ref> for the complete specification of the service.

The code accesses  the following variables: $lsz$, $lsize$, and $lvl$ to keep information about the current level; $blk$, $bn$, and $bb$ to represent the address and number of the block currently being accessed; $freeing\_node$ to represent the node being freeing; and $i$ to iterate blocks. Additionally, the model includes the component $free\_block\_r$ to model the recursion condition. To simplify the representation, the model uses predicates and functions to access and modify the state. Due to space constraints, we are unable to provide a detailed explanation of these functions. However, the name of the functions can help the reader to better understand their functionality.

In the C code,  free_block is a recursive function with two conditions: (1) the block being released belongs to a level higher than zero, since blocks at level zero cannot be merged; and (2) the partners bits of the block being released are FREE, so they can be merged into a bigger block. We represent (1) with the predicate ${\isasymacute}lvl\ t\ {\isachargreater}\ {\isadigit{0}}$ and (2) with the predicate $partner\_bit\_free$. The formal specification follows the same structure translating the recursive function into a loop that is controlled by a variable mimicking the recursion.

The formal specification for  free_block first releases an allocated memory block $bn$ setting it to FREEING. Then, the loop statement sets free_block to FREE (Line 5), and also checks that the iteration/recursive condition holds in Line 7. If the condition holds, the partner bits are set  to NOEXIST, and remove their addresses from the free list for this level (Lines 12 - 14). Then, it sets the parent block bit to FREEING (Lines 17 - 22), and updates the variables controlling the current block and level numbers, before going back to the beginning of the loop again. If the iteration condition is not true, it sets the bit to FREE and add the block to the free list (Lines 24 - 28) and sets the loop condition to false to end the procedure.
This function is illustrated in  <ref>. A thread releases the block $172$, and since its partner blocks (block $173 - 175$) are free, Zephyr coalesces the four blocks and sets their parent block $43$ as FREEING. The coalescence continues iteratively if the partners of block $43$ are all free.

§.§ Correctness and Rely-guarantee Proof

Using the compositional reasoning of , correctness of Zephyr memory management can be specified and verified with the rely-guarantee specification of each event.
A pair pre-post-condition for a kernel service specifies its functional correctnes.
Invariant preservation, memory configuration, and separation of local variables are specified in the guarantee condition of each service.
The guarantee condition for both memory services is defined as:

Mempoolallocguar t

$\overbrace{cur\ s\ {\isasymnoteq}\ Some\ t\ {\isasymlongrightarrow}\ gvars{\isacharunderscore}nochange\ s\ r\ {\isasymand}\ lvars{\isacharunderscore}nochange\ t\ s\ r}^{(3.1)}$

$\overbrace{cur\ s\ {\isacharequal}\ Some\ t\ {\isasymlongrightarrow}\ inv\ s\ {\isasymlongrightarrow}\ inv\ r}^{(3.2)}$

$\overbrace{{\isasymforall}t{\isacharprime}{\isachardot}\ t{\isacharprime}\ {\isasymnoteq}\ t\ {\isasymlongrightarrow}\ lvars{\isacharunderscore}nochange\ t{\isacharprime}\ s\ r}^{(4)}$

This relation states that the alloc and free services may not change the state (1), e.g., a blocked await or selecting branch on a conditional statement. If it changes the state then: (2) the static configuration of memory pools in the model do not change; (3.1) if the scheduled thread is not the thread invoking the event then variables for that thread do not change, since it is blocked in an Await; (3.2) if it is, then the relation preserves the memory invariant, and consequently each step of the event needs to preserve the invariant $inv$; (4) a thread does not change the local variables of other threads.

Using the  proof rules, we verify that all the events reserve the invariant. Additionally, we prove that when starting in a valid memory configuration given by the invariant, then the service returns a valid memory block with size bigger or equal than the requested capacity, when the returned value is not an error code. The following postcondition specifies the property:

Mempoolallocpre t  s inv s  allocatingnode s t  None  freeingnode s t  None

Mempoolallocpost t p sz timeout  s inv s  allocatingnode s t  None  freeingnode s t  None       timeout  FOREVER       ret s t  ESIZEERR  mempoolallocret s t  None       ret s t  OK  mblk mempoolallocret s t  Some mblk  mblkvalid s p sz mblk       timeout  NOWAIT       ret s t  ENOMEM  ret s t  ESIZEERR  mempoolallocret s t  None        ret s t  OK  mblk mempoolallocret s t  Some mblk  mblkvalid s p sz mblk       timeout  0       ret s t  ETIMEOUT  ret s t  ESIZEERR  mempoolallocret s t  None        ret s t  OK  mblk mempoolallocret s t  Some mblk  mblkvalid s p sz mblk

If a thread requests a memory block in mode FOREVER, it may successfully allocate a valid memory block, or fail (ESIZEERR) if the requested size is larger than the size of the memory pool. If the thread is requesting a memory pool in mode NOWAIT, it may also get the result of ENOMEM if there are no available blocks. But if the thread is requesting the service in mode TIMEOUT, it will get the result of ETIMEOUT if there are no available blocks in timeout milliseconds.

In , verification of a rely-guarantee specification proving a property is carried out by inductively applying the proof rules for each system event and discharging the proof obligations the rules generate. Typically, these proof obligations require to prove stability of the pre and postcondition to check that changes of the environment preserve them, and to show that a statement modifying a state from the precondition gets a state belonging to the postcondition.
A detailed proof sketch of the k_mempool_free service is shown in  <ref>.

To prove loop termination, loop invariants are parametrized with a logical variable $\alpha$. It suffices to show total correctness of a loop statement by the following proposition where $loopinv(\alpha)$ is the parametrize invariant, in which the logical variable is used to find a convergent relation to show that the number of iterations of the loop is finite.

\[ %\fontsize{8pt}{0cm}
\begin{aligned}
&\rgsatpI{(Some \ P)}{\rgcond{loopinv(\alpha) \cap \{s.\ \alpha > 0\}}{R}{G}{\exists \beta < \alpha. \ loopinv(\beta)}} \\
& \wedge\  loopinv(\alpha) \cap \{s.\ \alpha > 0\} \subseteq \{s.\ b\} \ \wedge \ loopinv(0) \subseteq \{s.\ \neg b\} \\
& \wedge \ \forall s \in loopinv(\alpha).\ (s,t) \in R \longrightarrow \exists \beta \leqslant \alpha. \ t \in loopinv(\beta)
\end{aligned}
\]

For instance, to prove termination of the loop statement in free_block shown in  <ref>, we define the loop invariant with the logical variable $\alpha$ as follows.

mpfreeloopinv t b   s. inv s  level b  length lsizes s t   iilength lsizes s t lsizes s t  ii  maxsz mempoolinfo s pool b div 4  ii   bn s t  length bits levels mempoolinfo s pool blvl s t   bn s t  block b div 4  level b  lvl s t  lvl s t  level b

freeblockr s t   blk freeingnode s t  Some blk  pool blk  pool b                               level blk  lvl s t  block blk  bn s t

allocmemblkdatavalid s pool b the freeingnode s t

freeblockr s t  freeingnode s t  None   ...

s.   if freeingnode s t  None then lvl s t  1 else 0

$freeing\_node$ and $lvt$ are local variables respectively storing the node being free and the level that the node belongs to.
In the body of the loop, if $lvl\ t\ {\isachargreater}\ {\isadigit{0}}$ and $partner\_bit$ is true, then $lvl = lvl - 1$ at the end of the body. Otherwise, $freeing\_node \ t= None$. So at the end of the loop body, $\alpha$ decreases or $\alpha = 0$. If $\alpha = 0$, we have $freeing\_node\ t = None$, and thus the negation of the loop condition  $\neg free\_block\_r \ t$, concluding termination of free_block.

§ VERIFIED TRANSLATION FROM BPEL TO

In the case study of Zephyr concurrent memory management, we have shown the simplicity of the formal specification of  for concurrent OS kernels as well as the power of  for compositional reasoning of CRSs with complex structures and algorithms.
This section presents another class of CRSs, i.e. concurrent business processes in BPEL language <cit.>, which has more complex event patterns. This kind of CRSs has a flow reaction structure.
Due to the wide application of business process programming, especially in safety/security critical systems, it is essential to ensure correctness and safety/security of business processes in order to avoid errors that may cause critical losses to the involved organizations.

In this case study, we create an abstract syntax for BPEL and implement a formally verified translation from BPEL into , rather than use the  to model the BPEL programs directly. This approach alleviates the efforts of manually modeling BPEL programs by automatic translation and provides high confidence with correctness proof. By the correct translation, the functional correctness and safety/security of BPEL programs can be compositionally verified in .

The correctness of the translation or compilation is usually defined as a simulation relation between the source and target languages, <cit.>. Thus, we define a strong bisimulation relation for the correctness of the translation from BPEL to .  is designed having reaction structures in mind, and it is expressive enough to simulate each small step of BPEL processes.

In this section, we first introduce the BPEL language in brief. Then, we present an abstract syntax and its operational semantics of a core subset of BPEL in Isabelle/HOL. Next, we discuss the translation of BPEL into  and its correctness proof.

§.§ Background of BPEL

Service-oriented computing represents a paradigm for building distributed computing applications over the Internet, where services are the basic blocks and applications are constructed by interoperations among services. From a business perspective, services composition drastically reduces the cost and risks of building new business applications in the sense that existing business logics are represented as Web services and could be reused <cit.>. Service compositions are programmed as executable business processes in languages like BPEL <cit.>, which is an imperative, XML-based language.
In BPEL, activities are nested within concurrency, compensation and event handling constructs that cause an overwhelming number of execution paths.

In  <ref>, we illustrate the structure of business processes in BPEL with a simple example adopted from the BPEL standard. The labels in blue color show the type of each activity.
Solid arrows in black color represent sequencing. Solid arrows in red color represent control links used for synchronization across concurrent activities.
Activities in BPEL perform the process logic. Basic activities are those describing elemental steps of the process behaviour, such as invoke, receive, reply, assign, wait. The wait activity specifies a delay for a certain period of time or until a certain deadline is reached.
Structured activities encode control-flow logic, and therefore can contain other basic and/or structured activities recursively, such as sequence, if, while, repeatUntil, forEach, pick, flow. The pick activity waits for the occurrence of exactly one event from a set of events, then executes the activity associated with that event. The flow activity provides concurrency and synchronization using links.

An Example of BPEL <cit.>

§.§ Formalizing the BPEL Language in Isabelle/HOL

We design an abstract syntax of a core subset of the BPEL language as shown in  <ref>.
The invoke activity is used to call a Web Service offered by service providers, which is specified by the service's partner link ptlink, port type pttype and operation op. The invocation returns normally, and the state is updated by the invocation result, which is specified as a mapping spec of states. It also may return a fault message identified by a QName.
The catch construct attached to the invoke activity provides a way to define a set of custom fault handling activities, where each of them is defined to intercept a specific kind of fault. A default handler catchAll clause can be added to catch any fault not caught by a more specific fault handler.
Whenever a catchAll fault handler is missing, it must be implicitly created. Thus, we assume there is a catchAll handler for each invoke activity.

slc FlowEle  targets  slc State  bool  l list option

sources  l  slc State  bool list option

slc Activity      Invoke  feslc FlowEle ptlinkNCName pttypeQName opNCName

specslc State  slc State

catchesQName  slc Activity list catchallslc Activity

Receive  feslc FlowEle ptlinkNCName pttypeQName opNCName

specslc State  slc State

Reply  feslc FlowEle ptlinkNCName pttypeQName opNCName

Assign  feslc FlowEle   slc State  slc State

Wait  feslc FlowEle Time

Empty  feslc FlowEle

Seq   slc Activity   slc Activity

If   condslc State set   slc Activity   slc Activity

While   condslc State set   slc Activity

Flow   slc Activity   slc Activity

Pick   slc EventHandler   slc EventHandler

and slc EventHandler

OnMessage  ptlinkNCName pttypeQName opNCName

specslc State  slc State   slc Activity

OnAlarm  Time   slc Activity

repeatUtil c P $\equiv$ Seq  P  (While c P)

forEach m n P $\equiv$
if m = n then P

else if m > n  then

else Seq  P (forEach (m + 1) n P)

Syntax of BPEL in Isabelle/HOL

A business process provides services to its partners through inbound message activities (e.g. receive and pick) and corresponding reply activities.
A receive activity specifies a partner link ptlink to receive messages, the port type pttype and operation op that it expects the partner to invoke. A receive activity is blocked until it receives a message and the state is updated by assigning the message to a variable.
The reply activity is used to send a response to a request previously accepted through an inbound message activity such as a receive activity. This activity only queries the current state for sending messages; however, the state is not changed.

The assign activity can be used to copy data from one variable to another, as well as to construct and insert new data using expressions. A state mapping specifies this activity. The wait activity specifies a delay until a certain deadline is reached. The empty activity specifies an activity that does nothing, for example when a fault needs to be caught and suppressed. Another use of empty is to provide a synchronization point in a flow structure.

The if, seq and while activities are standard, and repeatUntil is similar to do { ... } while(b) statement.
The forEach activity has two execution modes. In sequential mode, when its parallel attribute is false, the forEach activity will execute its contained activity exactly $N+1$ times where $N = endv - startv$. Otherwise, the activity is a parallel forEach. The enclosed activity must be concurrently executed $N+1$ times. Essentially, it is the same as a flow activity with $N+1$ copies of the forEach's enclosed activity as children. Thus, we could only consider sequential forEach activities for formal verification.

The pick activity waits for the occurrence of exactly one event from a set of events, then executes the activity associated with that event. After an event has been selected, the other events are no longer accepted by that pick. The activity is comprised of a set of event handlers, each containing an event-activity pair in two forms: (1) The onMessage is similar to a receive activity, in that it waits for the receipt of an inbound message. (2) The onAlarm corresponds to a timer-based alarm.

A flow activity completes when all of the activities enclosed by the flow have completed.
The synchronization of concurrent activities is specified by a flow element attached to basic activities.
An activity can declare itself to be the source of one or more links by including one or more source elements (sources).
Each source element can specify an optional transition condition as a guard for the specified link. After executing the activity, the source's specified link is flagged as fired, if the transition condition of a source is evaluated to true.
Similarly, an activity can declare itself to be the target of one or more links by including one or more target elements (targets). Targets, as a whole, can specify an optional join condition, which is a boolean expression. If the condition is true, the activity must be blocked until all links specified in targets are fired. If no join condition is specified, the condition is the disjunction of the link status of all incoming links of this activity.
Finally, we add  to denote the termination of BPEL execution.

Typical transition rules of BPEL are shown in  <ref>. The invoked service nondeterministically decides the occurrence of faults when a BPEL process invoking a Web services, so we choose one fault handler to be executed (InvokeFault). Other rules refer to the explanation of each activity above.

Invoke fls ptl ptt opn spc cts ctast
targets_sat (targets fls) s
r = spc s
t = fire_sources (sources fls) r

Invoke fls ptl ptt opn spc cts ctasevht

$\text{targets\_sat}\ (targets\ fls)\ s$   $t = \text{fire\_sources}\ (sources\ fls)\ s$
$evh \in set\ (map\ snd\ cts) \cup \{cta\}$

Pick P  QsQ't

Flow P QsFlow P O't

Flow  ss

OnMessage ptl ptt opn spc AsAt
t = spc s

OnAlarm time AsAs
time > tick s

Operational Semantics of BPEL

§.§ Translating BPEL into

We have developed a translator for the formal verification of BPEL programs using the  framework. In order to show that  is expressive to model concurrent business processes in BPEL, we use the event compositions to represent complex activities, rather than the complex statements in integrated languages such as . We only use the Basic statement in the  language ( <ref>) to change the state.
For the formal verification, we use the same state definition in the translated  specification as in the BPEL program.
BPEL composes Web services in the orchestration manner <cit.>, which always represents control from one party's perspective.
Formal verification of BPEL can only concern one BPEL program, rather than a set of composed programs, which would be a Web services choreography.
Moreover, a BPEL program composing a set of external services has embedded concurrent internal sub-processes. Therefore, we use event systems to represent BPEL processes but not parallel event systems. In this way, the events translated from BPEL activities do not have the parameter “$\textbf{OF}\ t$” to indicate the execution context.

We implement a compile function to translate a BPEL process into a  specification.
We first introduce the translation of the invoke activity as shown in  <ref>. Other translation rules are shown in  <ref>, which will be discussed later.

For each basic activity, the translated events are guarded by a condition

\[
{\isasymacute}{\isacharparenleft}{\isasymlambda}s{\isachardot}\ targets{\isacharunderscore}sat\ {\isacharparenleft}targets\ fls{\isacharparenright}\ s{\isacharparenright}
\]

which constrains the state that all targeted links of the activity are fired. Meanwhile, in the body of the translated events, the links sourced by the activity are fired by a statement

\[
Basic\ {\isacharparenleft}{\isasymlambda}s{\isachardot}\ fire{\isacharunderscore}sources\ {\isacharparenleft}sources\ fls{\isacharparenright}\ s{\isacharparenright}
\]

where $Basic\ spc$ represents an atomic state transformation, for example, an assignment, a multiple assignments, or the $SKIP$ command ($SKIP \equiv Basic\ Id$).

For the invoke activity, we use the $\textbf{Event}_{suc}$ and $\textbf{Event}_{fail}$ events to simulate the cases of normal and faulty invocation respectively. Since the execution of a invoke activity is one step in BPEL semantics, we use atomic events (EVENTA) to model it. In the normal case, the event updates the state by the invocation result and flags its source links. When the invocation returns a fault, it is nondeterministically resolved by special handlers and the default handler.
For the list of handlers in an invocation, we use the operator to compose the events in a list by the choice construct. Then, we use the $\oplus$ and operators to simulate the nondeterministism among successful invocation, failed invocations caught by the default and custom fault handlers. The $\textbf{Event}_{suc}$ event represents the successful invocation in . The sequence $\evtseq{ \textbf{Event\isactrlsub {fail}} }{ \textbf{compile}(cta) }$ represents a failed invocation and the default handler  ($cta$) deals with the fault. The “map (($\evtseq{\textbf{Event\isactrlsub {fail}}}{}$) $\circ$ compile) (map snd cts)” expression constructs a list of event sequence, each of which is $\evtseq{ \textbf{Event\isactrlsub {fail}} }{ \textbf{compile}(ct) }$ corresponding to each $(name,ct) \in cts$.
The partner link, port type and operation name are used to construct the event name.

\left\{
\begin{aligned}
& \lchoice{[]} = \fin \\
& \lchoice{[a]} = a \\
& \lchoice{(a \ \# \ b \ \# \ xs)} = \evtchoice{a}{(\lchoice{(b \ \# \ xs)})}
\end{aligned}
\right.

EVENTA Invokeptlpttopn

WHEN s targetssat targets fls s

Basic spc

Basic s firesources sources fls s

EVENTA Invokeptlpttopn

WHEN s targetssat targets fls s

Basic s firesources sources fls s

compile(Invoke  fls ptl ptt opn spc cts cta)

Eventsucc $\oplus$

(($\evtseq{ \textbf{Event\isactrlsub {fail}} }{ \textbf{compile}(cta) }$) # (map (($\evtseq{\textbf{Event\isactrlsub {fail}}}{}$) $\circ$ compile) (map snd cts)  ))

Translation of Invoke Activity

The compile function

BPEL Activity     Translated  Specification

Receive fls ptl ptt opn spc

EVENTA  Receiveptlpttopn WHEN  s targetssat targets fls s THEN  Basic spc Basic s firesources sources fls s END

Reply fls ptl ptt opn

EVENTA  Replyptlpttopn WHEN  s targetssat targets fls s THEN  Basic s firesources sources fls s END

Assign fls spc

EVENTA  Assign WHEN  s targetssat targets fls s THEN  Basic spc Basic s firesources sources fls s END

Wait fls t

EVENTA Wait WHEN t <  tick  s targetssat targets fls s THEN Basic s firesources sources fls s END

Empty fls

EVENTA  Empty WHEN  s targetssat targets fls s THEN  Basic s firesources sources fls s END

Seq  $A_1$ $A_2$

$\evtseq{(compile\ A_1)}{(compile\ A_2)}$

If c $A_1$ $A_2$

EVENTA If WHEN s sc THEN SKIP END

$\rhd$ compile A1

EVENTA Else WHEN s sc THEN SKIP END

$\rhd$ compile A2

While  c A

$\evtrec{c}{(compile\ A)}$

Pick  $A_1$ $A_2$

$\evtchoice{compile\ A_1}{compile\ A_2}$

Flow  $A_1$ $A_2$

$\evtjoin{compile\ A_1}{compile\ A_2}$

OnMessage ptl ptt opn spc at

EVENTA OnMessageptlpttopn

WHEN True THEN Basic spc END

$\rhd$  compile at

OnAlarm t at

EVENTA OnAlarm WHEN t > tick THEN SKIP END

$\rhd$  compile at

The translated  specification of receive, reply, assign and empty activities are similar to the invoke's.
A wait activity has an additional guard condition $t < tick$, i.e. the time point $t$ has passed.
The termination ActFin is translated to $\fin$.

An if activity is translated to the choice composition of two event systems, each of which has an atomic event with disjoint guard conditions. The translation of seq, while, pick and flow activities is straightforward, as well as event handlers OnMessage and OnAlarm.

Finally, due to different event names and bodies of translated events for BPEL activities, the translation we design is an injection shown as the following lemma.

if $\textbf{compile}(b_1) = \textbf{compile}(b_2)$ then $b_1 = b_2$.

§.§ Correctness Proof of the Translation

To show the correctness of the translation, we first give the intuition behind the semantic equivalence between a BPEL program and a  Specification.

A computation $c_{\symbevtsys}$ of an event system $\symbevtsys$ is equivalent to a computation $c_B$ of a BPEL program $B$, denoted as $\traceeq{c_B}{c_{\symbevtsys}}$, that is defined as follows.

\[
\left\{
\begin{aligned}
& \traceeq{Nil}{Nil} = True \\
& \traceeq{(B,s)\# tr1}{(\symbevtsys,t)\# tr2} = (compile(B) = \symbevtsys \wedge s = t \wedge \traceeq{tr1}{tr2}) \\
& \mathbf{otherwise} ... = False
\end{aligned}
\right.
\]

Computations of BPEL programs are defined similarly to the linear definition in Subsection <ref>, thus we use $\compfun(B,s)$ to denote the set of computations of a BPEL program $B$ from an initial state $s$. Then the equivalence of a  specification and a BPEL program is defined by the equivalence of their state traces as follows.

A  specification $\symbevtsys$ and a BPEL program $B$ is equivalent from an initial state $\symbstate$ under a configuration $\symbenv$, denoted as $\picorebpeleq{(B,s)}{(\symbevtsys,t)}$, if

* $\forall tr \in \compfun(B,s).\ \exists tr' \in \tilde{\compfun}(\symbenv,\symbevtsys,t).\ \traceeq{tr}{tr'}$.

* $\forall tr' \in \tilde{\compfun}(\symbenv,\symbevtsys,t).\ \exists tr \in \compfun(B,s).\ \traceeq{tr}{tr'}$.

The equivalence above is defined directly over state traces of programs, which is intuitive but not compositional.
To decompose the correct proof of the translation into each execution step of BPEL activities, we use a bisimulation relation considering each step of in a BPEL and  trace to represent the equivalence of a BPEL program and its translated  specification. Moreover, the bisimulation we defined is sound and complete w.r.t. the equivalence of state traces.

The bisimulation relation is coinductively defined as follows. Since BPEL and  have the same state definition, the state relation in the bisimulation is the equivalent relation “=”.

A BPEL program $B$ and a  specification $\symbevtsys$ are bisimilar from the same starting state $s$ under a configuration $\symbenv$, denoted as $\bisim{B}{s}{\symbevtsys}{s}$, when the following are true.

* for arbitrary $B'$ and $t$, if $\bpeltran{B}{s}{B'}{t}$, then there exists $\symbevtsys'$ such that $\exists \etranlabel.\ \estrannx{\symbevtsys}{s}{\etranlabel}{\symbevtsys'}{t}$ and $\bisim{B'}{t}{\symbevtsys'}{t}$.

* for arbitrary $\symbevtsys'$ and $t$, if $\exists \etranlabel.\ \estrannx{\symbevtsys}{s}{\etranlabel}{\symbevtsys'}{t}$, then there exists $B'$ such at $\bpeltran{B}{s}{B'}{t}$ and $\bisim{B'}{t}{\symbevtsys'}{t}$.

* $\symbevtsys = \textbf{compile}(B)$.

The bisimulation is sound and complete w.r.t. the state trace equivalence between BPEL and . The soundness and completeness of the bisimulation are shown as the following theorem, where  <ref> is a necessary condition for the completeness proof.

$\picorebpeleq{(B,s)}{(\symbevtsys,s)}$ iff $\bisim{B}{s}{\symbevtsys}{s}$.

The following two cases prove the theorem:

* soundness: it is sufficient to show that if $\bisim{B}{s}{\symbevtsys}{s}$, then

* for an arbitrary computation $tr \in \compfun(B,s)$, there exist $\symbcomp \in \tilde{\compfun}(\symbenv,\symbevtsys,s)$ such that $\traceeq{tr}{\symbcomp}$.

* for an arbitrary computation $\symbcomp \in \tilde{\compfun}(\symbenv,\symbevtsys,s)$, there exist $tr \in \compfun(B,s)$ such that $\traceeq{tr}{\symbcomp}$.

The two propositions could be proved by induction of the list $tr$ and $\symbcomp$ respectively.

* completeness: by coinduction of the bisimulation, we only need to prove the following three propositions under the assumption $\picorebpeleq{(B,s)}{(\symbevtsys,s)}$:

* if $\bpeltran{B}{s}{B'}{s'}$, there exists $\symbevtsys'$ such that $\exists \etranlabel.\ \estrannx{\symbevtsys}{s}{\etranlabel}{\symbevtsys'}{s'}$ and $\picorebpeleq{(B',s')}{(\symbevtsys',s')}$. We prove it by $\symbevtsys' = compile(B')$.

* from $\bpeltran{B}{s}{B'}{s'}$ we have that $[(B,s),(B',s')] \in \compfun(B,s)$. With the assumption we have $[(\symbevtsys,s),(\symbevtsys',s')] \in \tilde{\compfun}(\symbenv,\symbevtsys,s)$. Thus, $\exists \etranlabel.\ \estrannx{\symbevtsys}{s}{\etranlabel}{\symbevtsys'}{s'}$.

* to prove $\picorebpeleq{(B',s')}{(\symbevtsys',s')}$, we need to show that

for arbitrary $tr \in \compfun(B',s')$, there exists $\symbcomp \in \tilde{\compfun}(\symbenv,\symbevtsys',s')$ such that $\traceeq{tr}{\symbcomp}$. With $\bpeltran{B}{s}{B'}{s'}$, we have that $(B,s)\#tr \in \compfun(B,s)$. With the assumption $\picorebpeleq{(B,s)}{(\symbevtsys,s)}$, we obtain a computation $\symbcomp' \in \tilde{\compfun}(\symbenv,\symbevtsys,s)$ and $\traceeq{(B,s)\#tr}{\symbcomp'}$. Then it is proved by $\symbcomp = tl\ \symbcomp'$, where $\symbcomp$ is the tail of the list $\symbcomp'$.

* for arbitrary $\symbcomp \in \tilde{\compfun}(\symbenv,\symbevtsys',s')$, there exists $tr \in \compfun(B',s')$ such that $\traceeq{tr}{\symbcomp}$. It could be proved by a reversed way using the injection of the translation ( <ref>).

* if $\exists \etranlabel.\ \estrannx{\symbevtsys}{s}{\etranlabel}{\symbevtsys'}{s'}$, there exist $B'$ such that $\bpeltran{B}{s}{B'}{s'}$ and $\picorebpeleq{(B',s')}{(\symbevtsys',s')}$. It could be similarly proved as above by $\symbevtsys' = compile(B')$.

* $\symbevtsys = compile(B)$. Its straightforward from the assumption and  <ref>.

Finally, we have proved the theorem of correct translation from BPEL to  as follows.

$\forall B\ s.\ \bisim{B}{s}{compile(B)}{s}$

By coinduction of the bisimulation, it is sufficient to prove the following propositions:

* if $\bpeltran{B}{s}{B'}{s'}$ then $\exists \etranlabel.\ \estrannx{compile(B)}{s}{\etranlabel}{compile(B')}{s'}$. It could be proved by induction of $B$ and then the preservation on each type of BPEL activity and its compiled  specification, among which the proof of the invoke activity is the most complex. It is proved by the cases of transitions rules of invoke:

* InvokeSuc in  <ref>: the Eventsucc in $\textbf{compile}(\textbf{Invoke} \ fls\ ptl\ ptt\ opn\ spc\ cts\ cta)$ in  <ref> simulates the successful invocation. Furthermore, we have
$$\exists \etranlabel.\ \estrannx{\textbf{Event\isactrlsub {succ}}}{s}{\etranlabel}{\fin}{s'}$$
$$\textbf{compile}(\bpelfin) = \fin$$

* InvokeFault in  <ref>: we further split the case to two cases, i.e. the fault is caught by the default handler and by special handlers. The first case is simulated by $\evtseq{ \textbf{Event\isactrlsub {fail}} }{ \textbf{compile}(cta) }$ in $\textbf{compile}(\textbf{Invoke} \ fls\ ptl\ ptt\ opn\ spc\ cts\ cta)$ in  <ref>. We have
$$\bpeltran{\textbf{Invoke}\ fls\ ptl\ ptt\ opn\ spc\ cts\ cta}{s}{cta}{s'}$$
$$\exists \etranlabel.\ \estrannx{\evtseq{ \textbf{Event\isactrlsub {fail}} }{ \textbf{compile}(cta) }}{s}{\etranlabel}{\textbf{compile}(cta)}{s'}$$

A similar way proves the second case.

* if $\estrannx{compile(B)}{s}{\etranlabel}{Q}{s'}$, there exist $B'$ such that $\bpeltran{B}{s}{B'}{s'}$ and $Q = compile(B')$. It could be proved in a similar approach as the first case.

§ EVALUATION AND DISCUSSION

§.§ Evaluation

We use Isabelle/HOL as the specification and verification system. All derivations of our proofs have passed through the Isabelle proof kernel.
<ref> shows the statistics for the effort and size of the proofs in the Isabelle/HOL theorem prover. In total, the models and mechanized verification consists of $\approx$ 28,400 lines of specification and proofs (LOSP), and the total effort is $\approx$ 24 person-months (PM). The specification and proof of  are reusable for the verification of other systems.