# Quasi-localization and Wannier Obstruction in Partially Flat Bands

Jin-Hong Park  Research Center for Novel Epitaxial Quantum Architectures,
Department of Physics, Seoul National University, Seoul, 08826, Korea  Jun-Won
Rhim<EMAIL_ADDRESS>Research Center for Novel Epitaxial Quantum
Architectures, Department of Physics, Seoul National University, Seoul, 08826,
Korea  Department of Physics, Ajou University, Suwon 16499, Korea

###### Abstract

The localized nature of a flat band is understood by the existence of a
compact localized eigenstate. However, the localization properties of a
partially flat band, ubiquitous in surface modes of topological semimetals,
have been unknown. We show that the partially flat band is characterized by a
non-normalizable compact localized state(NCLS). The partially flat band
develops only in a momentum range, where normalizable Bloch wave functions can
be obtained by the linear combination of the NCLSs. Outside this momentum
region, a ghost flat band, unseen from the band structure, is introduced for
the consistent counting argument with the full set of NCLSs. Then, we
demonstrate that the Wannier function corresponding to the partially flat band
exhibits an algebraic($\sim 1/r^{1+\epsilon}$ in 1D and $\sim
1/r^{3/2+\epsilon}$ in 2D) decay behavior, where $\epsilon$ is a positive
number. Namely, one can have the Wannier obstruction even in a topologically
trivial band if it is partially flat. Finally, we develop a construction
scheme of a tight-binding model of the topological semimetal by designing an
NCLS.

Introduction. Flat bands have received significant attention because they are
considered an ideal playground to study many-body physics [1, 2, 3, 4, 5, 6,
7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23] and geometric
properties of the Bloch wave function beyond topological aspects [24, 25, 26,
27, 28, 29, 30, 31, 32, 33]. While it has long been believed that the flat
band can only be realized in artificial systems [34, 35, 36, 37, 38, 39, 40],
there has recently been a surge of research on synthesizing flat band
materials [41, 42, 43, 44, 45, 46] after discovering the unconventional
superconductivity originating from the flat band in the twisted bilayer
graphene [47]. As a result, flat band materials are now regarded as intriguing
quantum materials with promising implications, attracting interest from both
fundamental and application-oriented perspectives.

The localization of charge carriers in a flat band, essential for
understanding many-body phenomena in the system, has an intriguing origin.
Suppose a flat band is perfectly dispersionless over the whole Brillouin zone,
denoted by a fully flat band(FFB). The localization nature of the FFB is
understood by the existence of a special eigenmode called a compact localized
state(CLS) [48, 49, 50]. The amplitude of the CLS is nonzero only inside a
finite region while completely vanishing outside of it. The CLS can be
stabilized due to the destructive interference provided by the flat band
system’s specific lattice and hopping structures. This explains how the
electrons can be localized in the flat band systems, although electrons are
itinerant via the hopping processes. Moreover, it was shown that when the flat
band’s Bloch eigenfunction possesses a singularity due to a band-crossing, one
cannot find a set of independent CLS spanning the flat band. In this case,
several extended states, called the non-contractible loop states(NLSs), should
be added to the set to achieve completeness [49, 48]. NLSs exhibit exotic
real-space topology probed in photonic lattices [37]. From designing CLSs and
NLSs, one can also easily construct flat band tight-binding models [51].

Besides the FFB, one can also observe partially flat bands(PFBs) frequently on
the edge or surface of topological semimetals, such as graphene and nodal line
semimetals [52, 53, 54, 55, 56, 57, 58]. In the zigzag graphene
nanoribbon(ZGNR), we have PFBs between two Dirac points. In fact, they are
nearly flat bands with momentum dependence $\sim(k-\pi)^{Q}$ around the zone
boundary, where $Q$ is the number of dimmer lines proportional to the ribbon
width. In the semi-infinite limit($Q\rightarrow\infty$), the exact PFB is
realized. The PFBs of the ZGNR attracted tremendous attention due to their
instability toward the half-metallic ground state [59]. Another well-known
example is the drum-head surface states of nodal-line semimetals [55, 56, 57,
58], which are expected to lead to the high-temperature superconductivity
[60].

Figure 1: (a) The band structure of a semi-infinite zigzag graphene
nanoribbon. At zero energy, the PFB and GFB are plotted by the red solid and
gray dashed lines, respectively. (b) The semi-infinite zigzag graphene
nanoribbon has an edge on the left-hand side. The NCLS is drawn by a gray
region. The amplitudes of the NCLS are denoted by the colored circles, whose
size stands for the magnitude of the amplitude, while the color represents the
sign. We have different NCLSs depending on the position of the vertex
indicated by the red star symbol. (c) A linear combination of the NCLSs,
resulting in a Bloch wave function, whose amplitudes are plotted in (d).

This letter answers the question of how to understand the localization nature
of PFBs. In the case of the FFB, one can always find $N$(the number of unit
cells in the system) CLSs spanning the flat band completely if the flat band
has no singularity [49]. This property characterizes the localization nature
of the FFB [61, 50, 49]. The same idea may not be applied to the PFB because
it has only $fN$ degenerate Bloch states, where $f$ is a fractional
number($0<f<1$) representing the ratio between the flat region and the
Brillouin zone. However, $N$ number of different CLSs must exist if at least
one CLS is found, by moving the center of the CLS to different unit cells.
This macroscopic mismatch between the number of Bloch wave functions and CLSs
implies that the conventional CLS cannot exist in the PFB.

We demonstrate that the PFB is characterized by an unconventional type of CLS
called a non-normalizable compact localized state(NCLS). With a normalizable
regular localized eigenstate, one can find $N$ independent such states by
translated copies of them. Then, their Bloch summations with different crystal
momenta give $N$ independent Bloch states, which correspond to an FFB, not a
PFB. The PFBs are usually found in semi-infinite systems, where the
normalizability condition can be broken. The NCLS shows the compactly
localized feature along the translationally invariant direction. However, its
amplitude can grow away from the boundary, resulting in a non-normalizable
state. Although it does not make sense to use the non-normalizable states
conventionally, we note that their Bloch sums can be normalizable depending on
the crystal momentum. The PFB appears in the momentum range with normalizable
Bloch sums of NCLSs, while we propose that there is a ghost flat band(GFB)
outside this range because the corresponding Bloch states cannot be
normalized. The unphysical, non-normalizable states cannot be observed in a
spectroscopy. However, introducing the GFB can resolve the frustrated counting
argument because we have the same number of Bloch states(from both the PFB and
GFB) and the NCLSs. We also investigate the localization properties of the
Wannier functions of the PFB. The exponential decay of the Wannier function of
an isolated analytic band explains the localization nature of insulators [62,
63]. This Wannierization is obstructed in topological bands due to the
singular properties of the corresponding Bloch wave function [64]. We show
that the Wannier obstruction can also occur in a topologically trivial band if
it is a PFB because the Bloch wave functions in the GFB do not participate in
the construction of the Wannier functions. In the PFB, the Wannier function
exhibits $~{}1/r^{1+\epsilon}$ and $~{}1/r^{3/2+\epsilon}$ decays with a
positive number $\epsilon$ in 1D and 2D, respectively, instead of the
exponential one. Finally, We develop a systematic scheme for constructing a
tight-binding Hamiltonian hosting a PFB by designing an NCLS. Since the PFBs
are usually the surface modes of topological semimetals, this scheme can be
used to obtain topological semimetal models.

Non-normalizable compact localized states. We discuss the generic localization
nature of a PFB by considering a specific example, the PFB of a semi-infinite
graphene with a zigzag edge, illustrated in Fig. 1(a). As denoted in Fig.
1(b), positions of A and B sites are represented by
$\mathbf{R}_{A}(m,n)=m\mathbf{a}_{1}+n\mathbf{a}_{2}$ and
$\mathbf{R}_{B}(m,n)=m\mathbf{a}_{1}+n\mathbf{a}_{2}+\mathbf{b}$,
respectively, where $\mathbf{a}_{1}=a(\sqrt{3}/2,-1/2)$,
$\mathbf{a}_{2}=a(0,1)$, and $\mathbf{b}=(a/\sqrt{3})(1/2,\sqrt{3}/2)$. Here,
$m\geq 0$ is the dimmer line index, and $a$ is the lattice constant. Here,
only the nearest neighbor hopping processes are included. We look for a CLS
localized along the translationally invariant direction, namely $y$-axis in
Fig. 1(b). One can find a zero energy eigenstate, illustrated in Fig. 1(b),
whose amplitudes at $A$ sites are given by

$\displaystyle\phi^{A}_{n^{*}}(m.n)=\begin{cases}(-1)^{m}{}_{m}\mathrm{C}_{n-n^{*}},&n^{*}\leq
n\leq n^{*}+m\\\ 0,&\mathrm{otherwise}\end{cases},$ (1)

where $n^{*}\mathbf{a}_{2}$ is the position of the left-end vertex of this
state, as indicated by an arrow in Fig. 1(b). The amplitudes at B sites,
denoted by $\phi^{B}_{n^{*}}(m.n)$, are zero. In total, the eigenstate is
written as
$|\phi_{n^{*}}\rangle=\sum_{m,n}[\phi^{A}_{n^{*}}(m,n)a^{\dagger}_{m,n}+\phi^{B}_{n^{*}}(m,n)b^{\dagger}_{m,n}]|0\rangle$,
where $a^{\dagger}_{m,n}$($b^{\dagger}_{m,n}$) creates an electron at A(B)
site with position $\mathbf{R}_{A}(m,n)$($\mathbf{R}_{B}(m,n)$). The compactly
localized feature of this state is due to the destructive interference between
$\phi^{A}_{n^{*}}(m,n^{*})$($\phi^{A}_{n^{*}}(m,n^{*}+m)$) and
$\phi^{A}_{n^{*}}(m+1,n^{*})$($\phi^{A}_{n^{*}}(m+1,n^{*}+m)$) at the
neighboring B site after the hopping processes. However, this is a non-
normalizable state since the amplitudes grow as the dimmer line index $m$
increases. This is the NCLS described in the introduction. There are $N$
degenerate NCLSs at zero energy depending on the vertex position $n^{*}$,
where $N$ is the number of unit cells along the $y$-axis. Since the left-end
vertices of the $N$ NCLSs with different $n^{*}$’s do not overlap, the $N$
NCLSs are independent of each other even within the periodic boundary
condition along $y$-axis.

Figure 2: (a) The lattice and hopping structures of the 3D nodal line
semimetal model. At each site, two orbitals, denoted by A and B, reside. Lines
with red, blue, and yellow colors represent hopping processes. Solid and
dashed lines indicate $+$ and $-$ signs of the hopping amplitudes. (b) The
band structure for $k_{z}=0$. The nodal ring is denoted by the red closed
curve. (c) A schematic view of the NCLS of the nodal line semimetal in the
semi-infinite system. (d) A linear combination of NCLSs in (c) with different
apex positions, resulting in a Bloch wave function.

We show that a normalizable Bloch eigenstate can be obtained from a linear
combination of the NCLSs, as illustrated in Fig. 1(c). We build an extended
eigenstate satisfying the Bloch theorem given by

$\displaystyle|\psi_{k}\rangle=\sum_{n^{*}}e^{in^{*}k}|\phi_{n^{*}}\rangle,$
(2)

whose amplitude reads

$\displaystyle\psi^{A}_{k}(m,n)=e^{ink}(1+e^{-ik})^{m},$ (3)

for the A sites at $\mathbf{R}_{A}(m,n)$ while $\psi^{B}_{k}(m,n)=0$, as
plotted in Fig. 1(d). The eigenenergy corresponding to this mode is zero
because that of $|\phi_{n^{*}}\rangle$ is zero. Most importantly, the obtained
Bloch eigenstate shows exponential decay along $\mathbf{a}_{2}$ direction if
$k\in I_{L}=(-\pi,-2\pi/3)$ or $k\in I_{R}=(2\pi/3,\pi)$. Here, the Brillouin
zone is set to be $-\pi<k\leq\pi$. Namely, $|\psi_{k}\rangle$ is a
normalizable one-dimensional Bloch wave function for momenta belonging to
$I_{L}$ or $I_{R}$. Outside these two intervals, on the other hand, the
constructed Bloch states should be discarded and invisible in spectroscopy
because they cannot be normalized. Therefore, we have zero energy flat band in
$I_{L}$ and $I_{R}$, which realizes the PFB. This PFB is not connected to
other bands and is terminated in the middle of the Brillouin zone. Meanwhile,
one can consider the zero energy states corresponding to the non-normalizable
$|\psi_{k}\rangle$ outside $I_{L}$ and $I_{R}$ as a ghost flat band(GFB). We
have in total $N$ number of states in the PFB and GFB, which is consistent
with the $N$ number of independent NCLSs $|\phi_{n^{*}}\rangle$.

In general, we conjecture that a PFB is obtained in a semi-infinite system by
discarding the ghost part of an FFB. A semi-infinite system is a good
playground to have such a ghost band for the following reasons. Considering
only hermitian tight-binding Hamiltonians, which can be block-diagonalizable
into the finite-size Bloch Hamiltonians, the bulk’s band dispersion should be
analytic in momentum because every matrix element of the Bloch Hamiltonian of
such a model is analytic in momentum space. However, the PFB cannot be an
analytic function of momentum because an integer $n$ exists such that the
$n$-th left- and right-hand derivative of the band becomes discontinuous at
the end-point of the PFB. Therefore, the flat band should always be FFB in
such a conventional Hamiltonian. One of the ways to violate the properties of
the conventional Hamiltonians is to make the size of the Bloch Hamiltonian
infinite, which is impossible in reality in principle. The semi-infinite
systems are the examples, and the non-normalizable states can emerge in such
systems, as shown in the example above.

We apply our general conclusions to a 3D topological nodal-line semimetal. We
consider the minimal tight-binding Hamiltonian on a cubic lattice given by
$H_{\mathrm{NL}}=\sin k_{z}\sigma_{y}+(2-\cos k_{x}-\cos k_{y}-\cos
k_{z})\sigma_{z}$, where $\sigma_{\alpha}$ is a Pauli matrix representing the
orbital degree of freedom for each site. The hopping structure is illustrated
in Fig. 2(a). Lattice sites are represented by
$\mathbf{R}(\mathbf{n})=n_{x}\mathbf{a}_{x}+n_{y}\mathbf{a}_{y}+n_{z}\mathbf{a}_{z}$,
where $\mathbf{a}_{\alpha}$ is a unit vector along $\alpha$-direction. This
model hosts a nodal ring described by $1=\cos k_{x}+\cos k_{y}$ at zero
energy, as plotted in Fig. 2(b). When the system is terminated along
$z$-direction, we have a drumhead flat surface mode inside the nodal ring. We
consider a semi-infinite system obtained by removing sites with a negative
$n_{z}$ in the cubic lattice. The quasi-localized feature of this drumhead PFB
is explained by a zero energy NCLS illustrated in Fig. 2(c), whose apex is
located at
$\mathbf{R}(\mathbf{n}^{*})=n^{*}_{x}\mathbf{a}_{x}+n^{*}_{y}\mathbf{a}_{y}$.
The amplitude of the NCLS, denoted by $|\phi_{\mathbf{n}^{*}}\rangle$, is
given by

$\displaystyle\phi_{\mathbf{n}^{*},\sigma}(\mathbf{n})=\sigma\Big{[}2-\sum_{\beta}\left(e^{ik_{\beta}}+e^{-ik_{\beta}}\right)/2\Big{]}^{n_{z}}\Big{|}_{\Delta
n_{x},\Delta n_{y}},$ (4)

where $\sigma=\pm$ represents two orbitals, $\beta=x$ and $y$, and the
subscript $\Delta n_{\beta}=n_{\beta}-n_{\beta}^{*}$ means that we pick up the
coefficient of the exponential factor $e^{i\Delta n_{x}k_{x}+i\Delta
n_{y}k_{y}}$. Since the above formula is a finite polynomial of the
exponential factors, $\phi_{\mathbf{n}^{*},\sigma}(\mathbf{n})$ is nonzero
only inside a finite region for a given $n_{z}$, which implies the compact
localization. Then, by a linear combination of the NCLSs(Fig. 2(d)), we obtain
Bloch eigenfunction,
$|\psi_{\mathbf{k}}\rangle=\sum_{\mathbf{n}^{*}}e^{i\mathbf{n}^{*}\cdot\mathbf{k}}|\phi_{\mathbf{n}^{*}}\rangle$,
whose amplitudes are evaluated as

$\displaystyle\psi_{\mathbf{k},\sigma}(\mathbf{n})=e^{i(n_{x}k_{x}+n_{y}k_{y})}(2-\cos
k_{x}-\cos k_{y})^{n_{z}},$ (5)

where $\mathbf{k}=(k_{x},k_{y})$. The Bloch wave function exhibits exponential
decay and can be normalized in a momentum range $-1<2-\cos k_{x}-\cos
k_{y}<1$, precisely the same as the drum-head surface mode’s region above.
Outside the nodal ring, the constructed Bloch wave function increases
exponentially as a function of $n_{z}$ and cannot be normalized, which leads
to the GFB.

Wannier obstruction. The localization nature of an insulator is explained by
exponentially decaying Wannier functions [63]. According to the Paley-Wiener
theorem, such states are guaranteed to exist if the Bloch wavefunctions are
analytic over the whole Brillouin zone [65]. Bloch wavefunctions are always
analytic in 1D, and one can find exponentially localized Wannier functions in
a 1D isolated band. On the other hand, in 2D, a topologically nontrivial band
cannot have such a Wannierization due to singularities of the corresponding
Bloch eigenfunction in momentum space. Here, we investigate the Wannier
function properties of a PFB, where one cannot apply the Paley-Wiener theorem
because the Fourier transform of the Bloch wave function is ill-defined due to
the absence of the wave function outside the PFB regions in the Brillouin
zone.

Let us begin with the 1D PFB of a semi-infinite system. A general form of the
Bloch wave function of the PFB is given by

$\displaystyle|\psi_{k}\rangle=\lim_{Q\rightarrow\infty}\frac{1}{\sqrt{N}}\sum_{m=1}^{Q}\sum_{\sigma_{m}=1}^{P_{n}}v^{(Q)}_{m,\sigma_{m}}(k)e^{ikn}c^{\dagger}_{m,n,\sigma_{m}}|0\rangle,$
(6)

where $n$ is the unit cell index along the translationally invariant
direction, $m$ is the sublattice index, and $\sigma_{m}$ represents the
orbital in the $m$-th sublattice. Here, $m$ increases as we go away from the
semi-infinite system’s boundary($m=0$). The semi-infinity is described by the
limit process $Q\rightarrow\infty$. We assume that there are $P_{m}$ orbitals
in the $m$-th sublattice. Finally, $v^{(Q)}_{m,\sigma_{m}}(k)$ is the
component corresponding to the $\sigma_{m}$-th orbital in the $m$-th
sublattice of the PFB’s eigenvector ${\bf v}^{(Q)}(k)$ of the Bloch
Hamiltonian. Here, ${\bf v}^{(Q)}(k)$ is obtained by holding the components of
the unnormalized Bloch wave function constructed from the NCLSs, such as (3),
up to the $Q$-th sublattice and normalizing it. For example, for the semi-
infinite graphene, we have
$v^{(Q)}_{m}(k)=\psi^{A}_{k}(m,0)/(\sum_{m^{\prime}=0}^{Q}|\psi^{A}_{k}(m^{\prime},0)|^{2})^{1/2}$.
Note that, before reflecting the semi-infinity($Q\rightarrow\infty$) of the
system, $v^{(Q)}_{m,\sigma_{m}}(k)$ is analytic over the whole Brillouin zone,
even out of the PFB region. As a result, the Fourier transform of
$v^{(Q)}_{m,\sigma_{m}}(k)$ exponentially decays far from the Wannier center
according to the Paley-Wienener theorem and we have
$v^{(Q)}_{m,\sigma_{m}}(k)=(1/\sqrt{N})\sum_{n}e^{ikn}\varphi^{(Q)}_{m,\sigma_{m}}(n)$,
where $\varphi^{(Q)}_{m,\sigma_{m}}(n)\sim e^{-b|n|}$ for
$|n|\rightarrow\infty$ with a positive coefficient $b$. Now, we obtain the
Wannier function for the PFB by using this form of $v^{(Q)}_{m,\sigma_{m}}(k)$
in the semi-infinite limit($Q\rightarrow\infty$). In this limit,
$v^{(Q)}_{m,\sigma_{m}}(k)$ is ill-defined for momenta corresponding to the
EFB. Therefore, performing the integral over the momentum range corresponding
to the PFB is natural to construct a Wannier function from
$v^{(Q)}_{m,\sigma_{m}}(k)$. Then, the Wannier function amplitude for the
$\sigma_{m}$-th orbital is given by
$W_{m,\sigma_{m}}(n-n_{0})=(1/N)\lim_{Q\rightarrow\infty}\sum_{k\in
I_{\mathrm{PFB}}}v^{(Q)}_{m,\sigma_{m}}(k)e^{ik(n-n_{0})}$, where
$I_{\mathrm{PFB}}$ is a set of momenta supporting the PFB, and $n_{0}$ is the
Wannier function’s center. In general, $I_{\mathrm{PFB}}$ is divided into many
separate intervals, where the $l$-th one is $[k_{l,i},k_{l,f}]$. Denoting
$\Delta n=n-n_{0}$,
$v_{m,\sigma_{m}}(k)=\lim_{Q\rightarrow\infty}v^{(Q)}_{m,\sigma_{m}}(k)$, and
$\varphi_{m,\sigma_{m}}(k)=\lim_{Q\rightarrow\infty}\varphi^{(Q)}_{m,\sigma_{m}}(k)$,
the Wannier function of the PFB is given by

$\displaystyle W_{m,\sigma_{m}}(\Delta n)=\frac{1}{2\pi
i}\sum_{l,\alpha}s_{\alpha}\frac{e^{ik_{l}\Delta n}}{\Delta
n}F_{l,m,\sigma_{m}}(\Delta n),$ (7)

where

$\displaystyle F_{l,m,\sigma_{m}}(\Delta
n)=\frac{1}{\sqrt{N}}\sum_{n^{\prime}}\varphi_{m,\sigma_{m}}(n^{\prime})\frac{e^{ik_{l,\alpha}}}{n^{\prime}/\Delta
n+1},$ (8)

and $s_{\alpha}=-1$ or $1$ for $\alpha=i$ or $f$, respectively. Since we are
interested in the behavior of $W(\Delta n)$ in the limit $|\Delta
n|\rightarrow\infty$, let us consider a function
$\tilde{F}_{l,m,\sigma_{m}}(x)=F_{l,m,\sigma_{m}}(1/x)$, where $x=1/\Delta n$.
One can show that $\tilde{F}_{l,m,\sigma_{m}}(0)=0$ because the eigenvector
component $v_{m,\sigma_{m}}(k)$ should be zero at $k_{l,i}$ and $k_{l,f}$,
boundaries of the PFB to be continuously connected to the eigenvector
component of the EFB, which is zero in the limit $Q\rightarrow\infty$. To
figure out the functional form of $\tilde{F}_{l,m,\sigma_{m}}(x)$ near
$\alpha=0$, we consider an arbitrary order of derivatives of it at $\alpha=0$.
We evaluate $\partial_{x}^{p}\tilde{F}_{l,m,\sigma_{m}}(x)|_{x=0}$ and denote
the smallest $p$, where the derivative becomes nonzero, by $p^{*}$. If
$|\partial_{x}^{p}\tilde{F}_{l,m,\sigma_{m}}(x)|_{x=0}|<\infty$ for $p\geq
p^{*}$, one can deduce that $\tilde{F}_{l,m,\sigma_{m}}(x)\sim x^{p^{*}}$.
This implies that $W_{m,\sigma_{m}}\sim 1/r^{1+p^{*}}$ from (7). On the other
hand, $\partial_{x}^{p^{*}}\tilde{F}_{l,m,\sigma_{m}}(x)|_{x=0}$ can be
divergent too. In this case, one can infer that
$\tilde{F}_{l,m,\sigma_{m}}(x)$ is an irrational function of the form
$x^{\epsilon}$, where $p^{*}-1<\epsilon<p^{*}$ because
$\tilde{F}_{l,m,\sigma_{m}}(x)$ vanishes at $x=0$. In this case, we have
$W_{m,\sigma_{m}}\sim 1/r^{1+\epsilon}$. In total, the Wannier function decays
algebraically as $\sim 1/r^{1+\epsilon}$, where $p^{*}-1<\nu\leq p^{*}$. Note
that the Wannier functions with different $n_{0}$ of the PFB are not
orthogonal to each other in general because not all the Bloch wave functions
in the Brillouin zone participate in constructing the Wannier functions. As a
result, while there can be $N$ different Wannier functions with distinct
$n_{0}$ values, only $N\sum_{l}(k_{l,f}-k_{l,i})/2\pi$ number of them are
independent of each other. Similar conclusions to the 1D Wannierization above
can be applied to the two-dimensional PFBs. Specifically, we show that the
Wannier function corresponding to the 2D PFB exhibits $1/r^{3/2+\epsilon}$
decay far from its center, where $\epsilon$ is a positive number. Detailed
derivations are included in Supplementary information.

Figure 3: (a) and (b) plot the Wannier function amplitudes of the semi-
infinite zigzag graphene nanoribbon and nodal line semimetal, respectively.
$m$ and $m_{z}$ represent the dimer lines and layers away from the edge and
surface of these two systems. $n$ is an index of the unit cell along a
translationally invariant direction. In the insets, we show that the local
maxima of the Wannier functions decay algebraically. (c) A band dispersion of
a finite-width zigzag graphene nanoribbon. The red and blue bands in the
middle correspond to the edge states. (d) The Wannier function for the red
band in (c) for various values of $m$.

Let us consider semi-infinite graphene as an example. Using (3), we have the
normalized eigenvector component of the PFB, evaluated as
$v_{m}(k)=\lim_{Q\rightarrow\infty}v^{(Q)}_{m}(k)=[1-4\cos^{2}(k/2)]^{1/2}(1+e^{-ik})^{m}$,
where the orbital index $\sigma_{m}$ is dropped because we have only one
orbital per sublattice. The momentum range for the PFB is given by
$I_{\mathrm{PFB}}=[2\pi/3,4\pi/3]$. Outside the PFB region, $v_{m}(k)=0$. The
Wannier function is obtained by
$W_{m}(n-n_{0})=(1/2\pi)\int_{2\pi/3}^{4\pi/3}dk~{}v_{m}(k)e^{ik(n-n_{0})}$
for the $m$-th dimer line. When $n_{0}=0$, the Wannier function amplitudes for
several values of $m$ are plotted in Fig. 3(a). We note that $W_{m}(n)\sim
1/n^{3/2}$ for large $n$ as shown in the inset of Fig. 3(a). This is
consistent with that $\partial_{k}v_{m}(k)$ diverges at $k=2\pi/3$ and
$4\pi/3$. This implies that the Wannier function of the semi-infinite graphene
with a zigzag edge decays algebraically($\sim 1/r^{3/2}$) along the
translationally invariant direction. In the case of the semi-infinite nodal
line semimetal described by $H_{\mathrm{NL}}$ above, the normalized
eigenvector’s component of the PFB corresponding to the $n_{z}$-th layer from
the surface is given by
$v_{m_{z}}(\mathbf{k})=\lim_{Q\rightarrow\infty}v_{m_{z}}^{(Q)}(\mathbf{k})=[(\cos
k_{x}+\cos k_{y}-1)(3-\cos k_{x}-\cos k_{y})]^{1/2}(2-\cos k_{x}-\cos
k_{y})^{n_{z}}$ inside the nodal ring. Outside the nodal ring,
$\lim_{Q\rightarrow\infty}v_{m_{z}}^{(Q)}(\mathbf{k})=0$. By using it, we
obtain the Wannier function for the PFB, and observe another algebraic decay
proportional to $1/r^{2}$ along various directions on the surface, as plotted
in Fig. 3(b). This is consistent with the generic $1/r^{3/2+\epsilon}$ decay
of the 2D PFB Wannier function shown above.

Construction of topological semimetal models. By reversely using the fact that
the eigenvector’s components of the PFB are in the form of the polynomial of
exponential factors, one can find a topological semimetal model. Let us
describe the construction scheme by considering an example, a 2D semi-infinite
rectangular lattice consisting of two sublattices denoted by $A$ and $B$ and
translationally invariant along $x$ direction. We arrange the PFB’s
eigenvector component as
$\mathbf{v}(k)=(v_{1A}(k),v_{1B}(k),\cdots,v_{mA}(k),v_{mB}(k),\cdots)^{\mathrm{T}}$,
where $m$ is the dimerline index from the edge. We consider
$v_{mA}(k)=(-1-ae^{ik}-ae^{-ik})^{m-1}$ and $v_{mB}(k)=0$ as a zero energy
PFB’s eigenvector. One can note that this choice of the eigenvector
corresponds to a NCLS, which has nonzero amplitudes only in a finite region
for each given $m$. An example of the Hamiltonian matrix of the semi-infinite
system satisfying $H_{\mathrm{SI}}\mathbf{v}(k)=0$ is given by

$\displaystyle H_{\mathrm{SI}}=\begin{pmatrix}0&h^{*}_{k}&0&0&\cdots\\\
h_{k}&0&1&0&\cdots\\\ 0&1&0&h^{*}_{k}&\cdots\\\ 0&0&h_{k}&0&\cdots\\\
\vdots&\vdots&\vdots&\vdots&\ddots\end{pmatrix},$ (9)

where $h_{\mathbf{k}}=1+ae^{ik}+ae^{-ik}$. $\mathbf{v}(k)$ is normalizable for
$\pi/2<k<3\pi/2$ when $a<1$ and $\pi/2<k<\cos^{-1}(-1/a)$ or
$2\pi-\cos^{-1}(-1/a)<k<3\pi/2$ when $a\geq 1$. Since the boundaries of this
momentum interval correspond to the band-crossing points, the corresponding
bulk Hamiltonian $H_{\mathrm{bulk}}=(1+2a\cos k_{x}+\cos k_{y})\sigma_{x}+\sin
k_{y}\sigma_{y}$, where $\sigma_{\alpha}$ is the Pauli matrix, leads to a
topological semimetal with four Dirac nodes.

Discussion. By considering semi-infinite systems, we have shown that the PFB
appears in a momentum range, where the corresponding Bloch summations of the
NCLSs are normalizable. As a result, when we construct Wannier functions, the
integration range of the Bloch wave functions in the momentum space is smaller
than the entire Brillouin zone, leading to the algebraically decaying
behavior. Therefore, we have demonstrated that the Wannier obstruction can
happen even in a topologically trivial band.

While we have only considered semi-infinite systems, one might wonder,
regarding realistic systems, whether the Wannier obstruction can be applied to
finite systems or not. Here, the term finite system implies that the system’s
size is finite along the directions with broken translational symmetry.
Graphene nanoribbons with finite width are examples. In such finite systems,
where one can construct regular finite-size Bloch Hamiltonians, the GFB cannot
exist, and each edge band should be smoothly connected to one of the bulk
bands. Therefore, the conventional Wannierization with exponentially localized
wave packets should be achieved in these systems. However, we show that the
algebraic decaying behavior dominates the Wannier function near its center as
the system size increases. This is because the edge modes are unaffected by
the system size, while the bulk mode’s amplitudes diminish as the size grows.
As a result, the Wannier function decays exponentially only extremely far from
its center, where the bulk wave function’s amplitude becomes comparable to
that of the Wannier function. As an example, we consider a finite-size zigzag
graphene nanoribbon. Its band structure is drawn in Fig. 3(c) for the ribbon
width $Q=$, where the red and blue bands host nearly flat bands, corresponding
to the edge modes, near the zone boundary. By applying a small perturbation,
the red and blue bands are detached so that one can construct the Wannier
function for them properly. Then, the red band’s Wannier function is plotted
in Fig. 3(d) for various dimer lines, which exhibit the expected algebraic
decay.

## References

  * Mielke [1993] A. Mielke, Ferromagnetism in the hubbard model and hund’s rule, Physics Letters A 174, 443 (1993).
  * Tasaki [1998] H. Tasaki, From nagaoka’s ferromagnetism to flat-band ferromagnetism and beyond: an introduction to ferromagnetism in the hubbard model, Progress of theoretical physics 99, 489 (1998).
  * Hase  _et al._ [2018] I. Hase, T. Yanagisawa, Y. Aiura, and K. Kawashima, Possibility of flat-band ferromagnetism in hole-doped pyrochlore oxides sn 2 nb 2 o 7 and sn 2 ta 2 o 7, Physical review letters 120, 196401 (2018).
  * Sharpe  _et al._ [2019] A. L. Sharpe, E. J. Fox, A. W. Barnard, J. Finney, K. Watanabe, T. Taniguchi, M. Kastner, and D. Goldhaber-Gordon, Emergent ferromagnetism near three-quarters filling in twisted bilayer graphene, Science 365, 605 (2019).
  * Saito  _et al._ [2021] Y. Saito, J. Ge, L. Rademaker, K. Watanabe, T. Taniguchi, D. A. Abanin, and A. F. Young, Hofstadter subband ferromagnetism and symmetry-broken chern insulators in twisted bilayer graphene, Nature Physics 17, 478 (2021).
  * Aoki [2020] H. Aoki, Theoretical possibilities for flat band superconductivity, Journal of Superconductivity and Novel Magnetism 33, 2341 (2020).
  * Volovik [1994] G. Volovik, The fermi condensate near the saddle point and in the vortex core, JETP Letters 59, 830 (1994).
  * Volovik [2018] G. E. Volovik, Graphite, graphene, and the flat band superconductivity, JETP Letters 107, 516 (2018).
  * Balents  _et al._ [2020] L. Balents, C. R. Dean, D. K. Efetov, and A. F. Young, Superconductivity and strong correlations in moiré flat bands, Nature Physics 16, 725 (2020).
  * Yudin  _et al._ [2014] D. Yudin, D. Hirschmeier, H. Hafermann, O. Eriksson, A. I. Lichtenstein, and M. I. Katsnelson, Fermi condensation near van hove singularities within the hubbard model on the triangular lattice, Physical Review Letters 112, 070403 (2014).
  * Liu  _et al._ [2021] X. Liu, C.-L. Chiu, J. Y. Lee, G. Farahi, K. Watanabe, T. Taniguchi, A. Vishwanath, and A. Yazdani, Spectroscopy of a tunable moiré system with a correlated and topological flat band, Nature communications 12, 1 (2021).
  * Peri  _et al._ [2021] V. Peri, Z.-D. Song, B. A. Bernevig, and S. D. Huber, Fragile topology and flat-band superconductivity in the strong-coupling regime, Physical review letters 126, 027002 (2021).
  * Wu  _et al._ [2007] C. Wu, D. Bergman, L. Balents, and S. D. Sarma, Flat bands and wigner crystallization in the honeycomb optical lattice, Physical review letters 99, 070401 (2007).
  * Chen  _et al._ [2018] Y. Chen, S. Xu, Y. Xie, C. Zhong, C. Wu, and S. Zhang, Ferromagnetism and wigner crystallization in kagome graphene and related structures, Physical Review B 98, 035135 (2018).
  * Jaworowski  _et al._ [2018] B. Jaworowski, A. D. Güçlü, P. Kaczmarkiewicz, M. Kupczyński, P. Potasz, and A. Wójs, Wigner crystallization in topological flat bands, New Journal of Physics 20, 063023 (2018).
  * Wang and Ran [2011] F. Wang and Y. Ran, Nearly flat band with chern number c= 2 on the dice lattice, Physical Review B 84, 241103 (2011).
  * Tang  _et al._ [2011] E. Tang, J.-W. Mei, and X.-G. Wen, High-temperature fractional quantum hall states, Physical review letters 106, 236802 (2011).
  * Sun  _et al._ [2011] K. Sun, Z. Gu, H. Katsura, and S. D. Sarma, Nearly flatbands with nontrivial topology, Physical review letters 106, 236803 (2011).
  * Neupert  _et al._ [2011] T. Neupert, L. Santos, C. Chamon, and C. Mudry, Fractional quantum hall states at zero magnetic field, Physical review letters 106, 236804 (2011).
  * Sheng  _et al._ [2011] D. Sheng, Z.-C. Gu, K. Sun, and L. Sheng, Fractional quantum hall effect in the absence of landau levels, Nature communications 2, 1 (2011).
  * Regnault and Bernevig [2011] N. Regnault and B. A. Bernevig, Fractional chern insulator, Physical Review X 1, 021014 (2011).
  * Liu  _et al._ [2012] Z. Liu, E. J. Bergholtz, H. Fan, and A. M. Läuchli, Fractional chern insulators in topological flat bands with higher chern number, Physical review letters 109, 186805 (2012).
  * Bergholtz and Liu [2013] E. J. Bergholtz and Z. Liu, Topological flat band models and fractional chern insulators, International Journal of Modern Physics B 27, 1330017 (2013).
  * Rhim  _et al._ [2020] J.-W. Rhim, K. Kim, and B.-J. Yang, Quantum distance and anomalous landau levels of flat bands, Nature 584, 59 (2020).
  * Hwang  _et al._ [2021a] Y. Hwang, J.-W. Rhim, and B.-J. Yang, Geometric characterization of anomalous landau levels of isolated flat bands, Nature communications 12, 6433 (2021a).
  * Hwang  _et al._ [2021b] Y. Hwang, J. Jung, J.-W. Rhim, and B.-J. Yang, Wave-function geometry of band crossing points in two dimensions, Physical Review B 103, L241102 (2021b).
  * Hwang  _et al._ [2021c] Y. Hwang, J.-W. Rhim, and B.-J. Yang, Flat bands with band crossings enforced by symmetry representation, Physical Review B 104, L081104 (2021c).
  * Peotta and Törmä [2015] S. Peotta and P. Törmä, Superfluidity in topologically nontrivial flat bands, Nature communications 6, 8944 (2015).
  * Mera and Mitscherling [2022] B. Mera and J. Mitscherling, Nontrivial quantum geometry of degenerate flat bands, Physical Review B 106, 165133 (2022).
  * Oh  _et al._ [2022] C.-g. Oh, D. Cho, S. Y. Park, and J.-W. Rhim, Bulk-interface correspondence from quantum distance in flat band systems, Communications Physics 5, 320 (2022).
  * Yu  _et al._ [2023] J. Yu, C. J. Ciccarino, R. Bianco, I. Errea, P. Narang, and B. A. Bernevig, Nontrivial quantum geometry and the strength of electron-phonon coupling, arXiv preprint arXiv:2305.02340 (2023).
  * Tian  _et al._ [2023] H. Tian, X. Gao, Y. Zhang, S. Che, T. Xu, P. Cheung, K. Watanabe, T. Taniguchi, M. Randeria, F. Zhang, _et al._ , Evidence for dirac flat band superconductivity enabled by quantum geometry, Nature 614, 440 (2023).
  * Jung  _et al._ [2023] J. Jung, H. Lim, and B.-J. Yang, Quantum geometry and landau levels of quadratic band crossing points, arXiv preprint arXiv:2307.12528 (2023).
  * Guzmán-Silva  _et al._ [2014] D. Guzmán-Silva, C. Mejía-Cortés, M. Bandres, M. Rechtsman, S. Weimann, S. Nolte, M. Segev, A. Szameit, and R. Vicencio, Experimental observation of bulk and edge transport in photonic lieb lattices, New Journal of Physics 16, 063061 (2014).
  * Vicencio  _et al._ [2015] R. A. Vicencio, C. Cantillano, L. Morales-Inostroza, B. Real, C. Mejía-Cortés, S. Weimann, A. Szameit, and M. I. Molina, Observation of localized states in lieb photonic lattices, Physical review letters 114, 245503 (2015).
  * Mukherjee  _et al._ [2015] S. Mukherjee, A. Spracklen, D. Choudhury, N. Goldman, P. Öhberg, E. Andersson, and R. R. Thomson, Observation of a localized flat-band state in a photonic lieb lattice, Physical review letters 114, 245504 (2015).
  * Ma  _et al._ [2020] J. Ma, J.-W. Rhim, L. Tang, S. Xia, H. Wang, X. Zheng, S. Xia, D. Song, Y. Hu, Y. Li, _et al._ , Direct observation of flatband loop states arising from nontrivial real-space topology, Physical Review Letters 124, 183901 (2020).
  * Milićević  _et al._ [2019] M. Milićević, G. Montambaux, T. Ozawa, O. Jamadi, B. Real, I. Sagnes, A. Lemaître, L. Le Gratiet, A. Harouri, J. Bloch, _et al._ , Type-iii and tilted dirac cones emerging from flat bands in photonic orbital graphene, Physical Review X 9, 031010 (2019).
  * Taie  _et al._ [2015] S. Taie, H. Ozawa, T. Ichinose, T. Nishio, S. Nakajima, and Y. Takahashi, Coherent driving and freezing of bosonic matter wave in an optical lieb lattice, Science Advances 1, e1500854 (2015).
  * Drost  _et al._ [2017] R. Drost, T. Ojanen, A. Harju, and P. Liljeroth, Topological states in engineered atomic lattices, Nature Physics 13, 668 (2017).
  * Kang  _et al._ [2020a] M. Kang, S. Fang, L. Ye, H. C. Po, J. Denlinger, C. Jozwiak, A. Bostwick, E. Rotenberg, E. Kaxiras, J. G. Checkelsky, _et al._ , Topological flat bands in frustrated kagome lattice cosn, Nature communications 11, 4004 (2020a).
  * Liu  _et al._ [2020] Z. Liu, M. Li, Q. Wang, G. Wang, C. Wen, K. Jiang, X. Lu, S. Yan, Y. Huang, D. Shen, _et al._ , Orbital-selective dirac fermions and extremely flat bands in frustrated kagome-lattice metal cosn, Nature communications 11, 4002 (2020).
  * Yin  _et al._ [2019] J.-X. Yin, S. S. Zhang, G. Chang, Q. Wang, S. S. Tsirkin, Z. Guguchia, B. Lian, H. Zhou, K. Jiang, I. Belopolski, _et al._ , Negative flat band magnetism in a spin–orbit-coupled correlated kagome magnet, Nature Physics 15, 443 (2019).
  * Kang  _et al._ [2020b] M. Kang, L. Ye, S. Fang, J.-S. You, A. Levitan, M. Han, J. I. Facio, C. Jozwiak, A. Bostwick, E. Rotenberg, _et al._ , Dirac fermions and flat bands in the ideal kagome metal fesn, Nature materials 19, 163 (2020b).
  * Lin  _et al._ [2018] Z. Lin, J.-H. Choi, Q. Zhang, W. Qin, S. Yi, P. Wang, L. Li, Y. Wang, H. Zhang, Z. Sun, _et al._ , Flatbands and emergent ferromagnetic ordering in fe 3 sn 2 kagome lattices, Physical review letters 121, 096401 (2018).
  * Di Sante  _et al._ [2023] D. Di Sante, C. Bigi, P. Eck, S. Enzner, A. Consiglio, G. Pokharel, P. Carrara, P. Orgiani, V. Polewczyk, J. Fujii, _et al._ , Flat band separation and robust spin berry curvature in bilayer kagome metals, Nature Physics , 1 (2023).
  * Cao  _et al._ [2018] Y. Cao, V. Fatemi, S. Fang, K. Watanabe, T. Taniguchi, E. Kaxiras, and P. Jarillo-Herrero, Unconventional superconductivity in magic-angle graphene superlattices, Nature 556, 43 (2018).
  * Rhim and Yang [2021] J.-W. Rhim and B.-J. Yang, Singular flat bands, Advances in Physics: X 6, 1901606 (2021).
  * Rhim and Yang [2019] J.-W. Rhim and B.-J. Yang, Classification of flat bands according to the band-crossing singularity of bloch wave functions, Physical Review B 99, 045107 (2019).
  * Leykam  _et al._ [2018] D. Leykam, A. Andreanov, and S. Flach, Artificial flat band systems: from lattice models to experiments, Advances in Physics: X 3, 1473052 (2018).
  * Kim  _et al._ [2023] H. Kim, C.-g. Oh, and J.-W. Rhim, General construction scheme for geometrically nontrivial flat band models, arXiv preprint arXiv:2305.00448 (2023).
  * Fujita  _et al._ [1996] M. Fujita, K. Wakabayashi, K. Nakada, and K. Kusakabe, Peculiar localized state at zigzag graphite edge, Journal of the Physical Society of Japan 65, 1920 (1996).
  * Rhim and Moon [2008] J.-W. Rhim and K. Moon, Edge states of zigzag bilayer graphite nanoribbons, Journal of Physics: Condensed Matter 20, 365202 (2008).
  * Jaskólski  _et al._ [2011] W. Jaskólski, A. Ayuela, M. Pelc, H. Santos, and L. Chico, Edge states and flat bands in graphene nanoribbons with arbitrary geometries, Physical Review B 83, 235424 (2011).
  * Burkov  _et al._ [2011] A. Burkov, M. Hook, and L. Balents, Topological nodal semimetals, Physical Review B 84, 235126 (2011).
  * Deng  _et al._ [2019] W. Deng, J. Lu, F. Li, X. Huang, M. Yan, J. Ma, and Z. Liu, Nodal rings and drumhead surface states in phononic crystals, Nature communications 10, 1769 (2019).
  * Kim  _et al._ [2015] Y. Kim, B. J. Wieder, C. Kane, and A. M. Rappe, Dirac line nodes in inversion-symmetric crystals, Physical review letters 115, 036806 (2015).
  * Bzdusek  _et al._ [2016] T. Bzdusek, Q. Wu, A. Rüegg, M. Sigrist, and A. A. Soluyanov, Nodal-chain metals, Nature 538, 75 (2016).
  * Son  _et al._ [2006] Y.-W. Son, M. L. Cohen, and S. G. Louie, Half-metallic graphene nanoribbons, Nature 444, 347 (2006).
  * Heikkilä  _et al._ [2011] T. T. Heikkilä, N. B. Kopnin, and G. E. Volovik, Flat bands in topological media, JETP letters 94, 233 (2011).
  * Bergman  _et al._ [2008] D. L. Bergman, C. Wu, and L. Balents, Band touching from real-space topology in frustrated hopping models, Physical Review B 78, 125104 (2008).
  * Kohn [1959] W. Kohn, Analytic properties of bloch waves and wannier functions, Physical Review 115, 809 (1959).
  * Brouder  _et al._ [2007] C. Brouder, G. Panati, M. Calandra, C. Mourougane, and N. Marzari, Exponential localization of wannier functions in insulators, Physical review letters 98, 046402 (2007).
  * Po  _et al._ [2018] H. C. Po, H. Watanabe, and A. Vishwanath, Fragile topology and wannier obstructions, Physical review letters 121, 126402 (2018).
  * Des Cloizeaux [1964] J. Des Cloizeaux, Analytical properties of n-dimensional energy bands and wannier functions, Physical Review 135, A698 (1964).


# Dezyne: Paving the Way to
Practical Formal Software Engineering

Rutger van Beusekom Verum Software Tools B.V., The Netherlands Bert de Jonge
Verum Software Tools B.V., The Netherlands Paul Hoogendijk Verum Software
Tools B.V., The Netherlands Jan Nieuwenhuizen Verum Software Tools B.V., The
Netherlands
<EMAIL_ADDRESS>
###### Abstract

Designing software that controls industrial equipment is challenging,
especially due to its inherent concurrent nature. Testing this kind of event
driven control software is difficult and, due to the large number of possible
execution scenarios only a low dynamic test coverage is achieved in practice.
This in turn is undesirable due to the high cost of software failure for this
type of equipment.

In this paper we describe the Dezyne language and tooling; Dezyne is a
programming language aimed at software engineers designing large industrial
control software. We discuss its underlying two layered and compositional
approach that enables reaping the benefits of Formal Methods, hereby strongly
supporting guiding principles of software engineering. The core of Dezyne uses
the mCRL2 language and model-checker (Jan Friso Groote et al.) to verify the
correctness and completeness of all possible execution scenarios.

The IDE of Dezyne is based on the Language Server Protocol allowing a smooth
integration with e.g., Visual Studio Code, and Emacs, extended with several
automatically generated interactive graphical views. We report on the
introduction of Dezyne and its predecessor at several large high-tech
equipment manufacturers resulting in a decrease of software developing time
and a major decrease of reported field defects.

##  1 Introduction

Designing software that controls industrial equipment is challenging. The
complexity of such equipment is ever growing and so is the demand on its
software. The software must control and monitor many processes in parallel.
Designing the regular control flow of the processing steps is already complex,
but many exceptional conditions may occur which disrupt the regular control
flow and must be handled appropriately.

Testing event driven control software is difficult. Testing time on hardware
is expensive so often software simulators on various levels of (hardware)
details are created to mitigate these costs. However, the ultimate test is
still the execution on the real hardware; errors found during the final
testing are very costly and time consuming to fix. Writing test cases for
(parts of) the software is difficult since, as explained earlier, many
different execution scenarios have to be considered which depend on different
timing conditions. As a result, only a small percentage of the possible
execution scenarios is effectively tested in practice.

This kind of high-tech equipment is extremely expensive, for instance the
Extreme Ultraviolet (EUV) lithography machine of ASML costs around $120
million dollar. Manufacturers of such kind of equipment are required to
deliver a high uptime of their machines. In some cases, the manufacturers are
penalized when a machine does not reach the agreed availability. As a result,
down time of these machines as the result of software failure must be avoided
at all cost.

##  2 Formal Methods

As stated in the previous section, designing and testing control software of
industrial high-tech equipment in a traditional fashion has serious short
comings, while on the other hand the cost-of-non-quality is extremely high.

Formal Methods have been around for many decades and have been shown to
deliver reliable and safe software. However, Formal Methods come with their
own challenges when applied to industrially sized systems and processes. The
tools and their associated languages require Formal Methods specialists.
Furthermore, a translation must be made from the (informal) requirements to
some description written in a Formal Methods Language. Typically, it is
challenging to validate that the intended requirements are correctly captured
or are that the requirements are appropriate in the first place.

The artifacts of the formalization process are typically used by Formal
Methods toolsets in proving the consistency of the requirements and any of the
derived refinements of the specifications. However, ultimately we need to
obtain running code on the hardware for which the specified properties
provably hold.

The total state space of any industrial size machine controlling application
is vast and cannot be handled by any Formal Methods tool in its entirety. A
practical way to handle this is to take a compositional approach: at a certain
level one should be able to abstract away from details which are not relevant
for the next level. This way the state-explosion problem can be avoided.

##  3 Dezyne

Verum has developed Dezyne [2]. Dezyne is a programming language aimed at
software engineers designing large industrial control software. The language
is designed to have a very low barrier to entry for regular software
engineers. The Dezyne language consists of two declarative language
constructs: the so-called “guarded” statement and the “on” statement for
specifying the states and trigger events of a state machine, respectively.
Furthermore, the Dezyne language has de facto standard imperative language
constructs as present in regular languages like C or Java: variable
declaration, assignment, function declaration, function call, and control flow
constructs like if-then-else.

###  3.1 The Component Model of Dezyne

Dezyne has the notion of three models: interfaces, components, and systems.

An interface model contains the definition of a set of events. In Dezyne
events are implemented as function calls. Each event declaration has a
direction, “in” or “out”, and a type signature. The type signature of an event
specifies the data parameters carried by an event, and the type of the return
value of an event. The allowed return types are: “void”, “boolean”,
enumeration types, and integer-range types. The types of the data parameters
can be any arbitrary type. This is an example of event declarations of an
interface:

⬇

interface IDevice {

in void turnon();

in void turnoff();

}

An interface also has a behaviour section. The behaviour of an interface
prescribes the order in which events are expected to occur. A behaviour can
specify additional state variables for keeping track of the state of the
interface. Using the simulator of the Dezyne tooling, the user can produce
sequence diagrams depicting allowed sequences of events for that interface.

An interface plays the role of a contract between components: it specifies how
a client component via its requires port should interact with the underlying
component providing the required functionality via its provides port. This is
an example of a simple interface that consists of two events “turnon” and
“turnoff”. The behaviour of the interface specifies that the events should be
used alternatingly:

⬇

interface IDevice {

in void turnon();

in void turnoff();

behaviour {

enum State {On, Off};

State s = State.Off;

[s.Off] {

on turnon: s = State.On;

on turnoff: illegal;

}

[s.On] {

on turnon: illegal;

on turnoff: s = State.Off;

}

}

}

Note that the statement “`on turnoff: illegal;`” defines that the event
“turnoff” is not allowed in that state.

A component model and a system model start by declaring their provides ports
and requires ports. A port is a instance of an interface.

A component model also specifies a behaviour, i.e. the actual implementation
of the component. The behaviour describes how a component implements each of
the events of its provides ports hereby possibly using some of its requires
ports. A behaviour can specify additional variables to keep track of the state
of the interaction between the component and its ports. In this way the user
specifies a finite state-machine describing the implementation of the
component. This is an example of a component model:

⬇

component Fork {

provides IDevice p;

requires IDevice r0;

requires IDevice r1;

behaviour {

enum State {On, Off};

State s = State.Off;

[s.Off] {

on p.turnon(): {r0.turnon(); r1.turnon(); s = State.On;}

}

[s.On] {

on p.turnoff(): {r0.turnoff(); r1.turnoff(); s = State.Off;}

}

}

}

Next to the provides and requires ports, a system model lists component
instances and the bindings between the ports of the component instances and
the external ports of the system. These bindings determine the routing, i.e.
call graph, of the events of the external ports of the systems and the
component instances. This is an example of a system model:

⬇

component System {

provides IControl cntrl;

system {

ProcessController controller;

Load loader;

Processor processor;

Unload unloader;

cntrl <=> controller.cntrl;

controller.load <=> loader.load;

controller.process <=> processor.process;

controller.unload <=> unloader.unload;

}

}

The Dezyne tools can generate a diagram from the system model as show in
figure 1.

Figure 1: Dezyne system diagram

Section 6 explains in more detail how these diagrams are generated. Note that
each connection in the diagram corresponds to a binding statement `<=>` in the
system model text.

###  3.2 Verifying Dezyne Models

The Dezyne language is statically checked on the use of syntax, types and an
extensive list of well-formedness properties111Among others: binding pairs of
provides and requires; non circular binding of ports; allowed component
triggers are “in” events of provides ports and “out” events of requires ports.

During the verification phase the Dezyne verification engine checks interface
and component models. The verification engine translates the Dezyne model to
an mCRL2 description [6, 3, 2]. Next, the mCRL2 tool set is used to convert
the mCRL2 description to an LTS (labeled transition system). An LTS is a graph
where nodes relate to states of the Dezyne model and each edge is labeled with
an event instance. The graph describes the total state space of the model and
all possible execution scenarios that cover this state space.

Both an interface and a component model are verified for the absence of
deadlocks and livelocks, and whether all integer assignments are in range by
inspecting the generated LTS. Additionally a component model is verified to
correctly interact with its requires ports as specified by their interfaces.
For this, the LTS is checked for the absence of the “illegal” label, where the
presence would indicate that either the component performed an action on one
of its requires port which was disallowed by the corresponding interface
behaviour, or that a requires port performed an event on the component which
was disallowed by the component behaviour.

Finally, the compliance of a component with all of its provides ports is
verified by means of the _ltscompare_ tool of mCRL2 using the Failures
Refinement preorder relation known from CSP [7, 14, 9]. It is used to verify
that the LTS of the component after hiding all internal, i.e. those events not
observable by the clients using the provides ports, is a refinement of the LTS
of the provides ports, i.e. for component C with provides port of type I and
requires port type J it verifies that:

$(C\|J)\\!\upharpoonright\\!\alpha(I)\,\sqsupseteq_{F}\,I$ (1)

where $\sqsupseteq_{F}$ denotes the Failures Refinement relation of CSP,
$\alpha(I)$ denotes the alphabet of process $I$, $\|$ denotes the parallel
composition synchronising on the common alphabet, and $\upharpoonright$
denotes the projection operator, i.e. the complement of the hiding operator,
i.e. $P\\!\upharpoonright\\!A=P\setminus\overline{A}$.

If an error is found a counter example is produced. This is a trace of events
leading up to the state where the inconsistency emerges.

Next in the Dezyne verification pipeline, the trace is fed to the Dezyne
simulator together with the original Dezyne models. The Dezyne simulator
reconstructs the relevant state and location information such that the user
can relate the counter example back to the Dezyne model text. The Dezyne
simulator outputs an encoding of a sequence diagram. This encoding also allows
navigating the source code location of each event occurrence in the sequence
diagram. This sequence diagram is fed to a graphical engine implemented in
JavaScript using a graphics library for rendering the sequence diagram. The
Dezyne simulator also outputs all possible valid next events. In the sequence
diagram these events are shown as buttons on the corresponding life lines.
Figure 2 depicts an example of a sequence diagram.

Figure 2: Generated Sequence Diagram with buttons for selecting next possible
event.

###  3.3 Two Level Approach

As described in the previous section, when verifying a Dezyne model a user
does not need to have a knowledge about Formal Methods or the mCRL2 language:
under the hood the Dezyne models are translated to mCRL2 models which are
verified using the mCRL2 tooling and a LTS analysis tool. If a problem is
found, the counter example trace is fed to the Dezyne simulator that generates
an interactive sequence diagram for the user. The user can use this diagram to
interactively find the root cause. The sequence diagram shows what the
component is doing from the start of the system up to the reported violation.
If the user has diagnosed the problem and has fixed the Dezyne models, they
can rerun the Dezyne verification engine and see whether the issue has
disappeared, and if not, iterate the steps mentioned above until the issue has
been fixed. After which, possibly another issue is found by the verification
engine and the attention is shifted to resolve this issue until no more issues
remain.

###  3.4 Generating Verified and Reliable Code

When the Dezyne models are verified and are correct, the models are used for
generating production quality machine code. Currently the Dezyne tooling has
code generators for the languages C++, C#, JavaScript and GNU Guile Scheme.

The operational semantics of the Dezyne models as specified by the modeling in
mCRL2 [2] and the implementation of Dezyne simulator is designed to capture
the intended execution behaviour of the corresponding generated machine code.
For Dezyne it is essential that the three embodiments of the semantics of
Dezyne are equivalent. Given that equivalence, it follows that if no problems
are found during verification, we know that all the verified properties also
hold for the generated machine code.

The equivalence between the semantics used during verification and the
simulation is asserted by means of _ltscompare_ -ing the trace equivalence of
the underlying LTSses for a large set of test models. Thus, for each model M
of this test set we check:

$LTS_{V}(M)\,\equiv_{T}\,LTS_{S}(M)$ (2)

where $LTS_{V}$ denotes the LTS produced by the mCRL2 tooling as used during
verification and $LTS_{S}$ denotes the LTS produced using the simulator by
calculating the transitive closure of the single step function of the
simulator, and $\equiv_{T}$ denotes the Trace Equivalence relation of CSP,
i.e. $L_{0}\equiv_{T}L_{1}$ iff $traces(L_{0})=traces(L_{1})$.

The equivalence of $LTS_{V}(M)$ with the generated code for component M is
verified in the following way. For $LTS_{V}(M)$ a trace graph cover is
calculated, i.e. a set of traces such that all edges of $LTS_{V}(M)$ occur in
the trace set. Next to the generated code for component M, a simulation stub
is also generated. The generated stub processes the textual representation of
a trace: for an inward going event the corresponding implementation of the
event is called. All outward events are logged and matched with the events of
the trace being processed. For all traces of the LTS graph cover, the
generated code plus stub is executed. If all traces of $LTS_{V}(M)$ are
correctly handled by the generated machine code for component M, we conclude
that

$traces(LTS_{V}(M))\,\subseteq\,traces(CODE_{L}(M))$ (3)

where $CODE_{L}(M)$ denotes the generated code and stub in language L for
model M, and $traces$ on code denotes the set of traces the execution of the
code would accept as described above.

Since $LTS_{V}(M)$ is complete, i.e. for all stable states, all events are
present, it follows that $CODE_{L}(M)$ is also complete, and since the
generated code is deterministic, i.e. for a given input event, only one
response is generated, we know that the generated code cannot exhibit more
behaviour as tested by the generated traces. In other words, it is that case
that:

$traces(LTS_{V}(M))\,\subseteq\,traces(CODE_{L}(M))\,\,\,\,\,\Rightarrow\,\,\,\,\,traces(LTS_{V}(M))\,=\,traces(CODE_{L}(M))$
(4)

Hence, we verify using _ltscompare_ and the running of all generated traces
that

$LTS_{V}(M)\,\equiv_{T}\,LTS_{S}(M)\,\equiv_{T}\,CODE_{L}(M)$ (5)

for all of the model M of the test set, for a given language L.

The above mentioned test set covers all aspects of the Dezyne language and
expected feature interactions. This test capability is also available for our
users to allow them to verify the equivalence (5) of their own (proprietary)
set of models. As a result, the user can assure that if no problems are found
during verification, all the verified properties hold for the generated
machine code for their specific models in their environment, i.e. target
compiler and platform.

##  4 Component Based Providing a Compositional Approach

As described above, a compositional approach to avoid the state explosion
problem is highly desirable to be able to verify large complex system designs.
Dezyne is a component based method: a component specifies its provides and
requires ports where ports are instances of interfaces. A Dezyne interface has
a contract, i.e. its behaviour, specifying the contract between two
components. The interfaces of the provides ports of a component are the
abstraction of said component. When designing a Dezyne component, a user does
not need to know which implementation is going to provide an interface; it is
sufficient to know the interface.

This provides a natural way of decomposing a larger system into smaller
manageable parts. When presented with the challenge to devise certain
functionality, one may approach this task by distinguishing the separate
responsibilities of that functionality which be separately assigned to one or
more components. The responsibility of a single component starts with its
provides ports and ends with its requires ports. When designing a component
one can, through verification, justly assume that the underlying components
implements the interfaces of its provides ports faithfully.

The approach of interfaces as an abstraction of components not only allows the
engineer to divide and conquer a problem by considering each responsibility of
a component one at the time, but also is a solution to verify complete systems
compositionally. This is due to an important property of the Failures
Refinement relation of CSP, which allows verifying each individual component
to be correct and therefore knowing that the overall system is also correct.
It is the case that when two components refine their provides port interfaces
then the compound of two components will also refine the top level provides
port since the Failures Refinement relation is transitive and the hiding
operator is congruent. We have, for component C with provides port of type I
and requires port of type J, and component D with provides port of type J and
requires port of type K, that:

$(C\|J)\\!\upharpoonright\\!\alpha(I)\,\sqsupseteq_{F}\,I\,\,\,\wedge\,\,\,(D\|K)\\!\upharpoonright\\!\alpha(J)\,\sqsupseteq_{F}\,J\,\,\,\,\,\Rightarrow\,\,\,\,\,(C\|D\|K)\\!\upharpoonright\\!\alpha(I)\,\sqsupseteq_{F}\,I$
(6)

Hence, for Dezyne, if we have proven that all components are correct, we have
proven that the complete system is correct.

##  5 Guiding Principles of Software Engineering

The development of the Dezyne methodology and language design are guided by
the fundamental software engineering principles as mentioned in e.g. [5].
These engineering principles are: rigor and formality, separation of concerns,
modularity, abstraction, anticipation of change, generality and
incrementality. We strive to have a methodology and language in supporting the
user as much as possible in practicing these engineering principles. Next we
discuss each of the principles in more detail and how they are reflected in
Dezyne in supporting the user.

#### Rigor and formality

Following this principle will add precision to and increases confidence in the
outcome of the creative process of constructing software by expressing
requirements and ideas succinctly using a well understood notation which
expresses intent and specifically allows communicating information.

As mentioned before, the Dezyne language has a rigorously and formally defined
operational semantics having three different but equivalent embodiments: the
modeling in mCRL2, the Dezyne simulator, and the behaviour of the generated
machine code.

For the user defining a Dezyne interface describing the interaction between
two components forces the user to clearly specify the expected interaction for
all possible scenarios thus also for exceptional cases. The verification
engine will find for a Dezyne component whether there are missing cases or
whether there are states where events are not handled as they are intended.

#### Separation of concerns

The principle of separation of concerns is a form of divide and conquer of the
work itself as well as dealing with the complexity of problems in general. By
explicitly distinguishing one aspect from another, we can avoid having to deal
with the compounded problem.

As mentioned before Dezyne is component based and guides the user in finding a
proper decomposition of the problem, i.e. describing different aspects in
behaviours independently in separate interfaces, component, and system models.

#### Modularity

Modularity is a structural and behavioural separation of concerns by
encapsulation222Information hiding, abstraction and (de)composition.

Interfaces represent and encapsulate the entire interactional conversation
between peer components. Components encapsulate all of the coordination across
its ports. Systems encapsulate component instances and their inter-
connections.

#### Incrementality

The principle of incrementality allows for stepwise refining solutions to
challenges, thereby avoiding the problems associated with a big bang approach.

Verification and code generation can be used throughout the life cycle of
every model. Also models can be extended aspect by aspect and hereby support
an agile software development approach.

#### Abstraction

Abstraction allows us to distinguish between key issues and side issues. The
key issues must be tackled early in the development process and will allow to
postpone dealing with the details at the last responsible moment.

Dezyne interfaces are abstractions of component interactions and hide
component implementation details and as mentioned before are key in having a
compositional approach.

#### Generality

Awareness of generality allow us to move from a point solution to a general
solution, which in turn caters for avoiding (future) work by using the general
solution.

In Dezyne interfaces represent the client’s perspective on the implementation.
Taking the different point solutions under consideration, this allows deriving
a general interface by capturing the commonality in the interaction of
different clients.

#### Anticipation of change

Change is inevitable, therefore we must both keep track of all of the
artifacts of the creative process, as well as maintain the consistency across
the refinement steps. We must also maintain their malleability.

In Dezyne the language and the verification create the freedom to evolve any
aspect while maintaining the consistency during the entire development
lifecycle. If a change breaks the consistency the verification engine will
report this and the user can take appropriate action.

##  6 Dezyne IDE Based on LSP

The core of the Dezyne tooling consists of the verification engine, simulator
and code generators which are implemented using GNU Guile Scheme. In order to
support a multitude of different IDEs we have implemented a language server
implementing the Language Server Protocol (LSP). LSP allows clients to remain
language-agnostic and share a single language-specific server implementation.
Currently the Dezyne LSP server provides code completion and code navigation.
The LSP server shares the parsing part with the core Dezyne tooling and as
such only a single language front-end has to be maintained. When the Dezyne
language is extended, it becomes immediately available for all IDEs by means
of the LSP server.

Currently there are LSP client implementations of both Visual Studio Code (3)
and GNU Emacs available. Due to the nature of LSP supporting the LSP clients
of other IDEs should involve little work, if any.

LSP is text oriented and currently does not provide any graphical support. To
integrate the interactive Dezyne diagrams, there is a daemon process running
on the machine of the user which among other things implements a webserver.
For all the Dezyne views a webbrowser is started that connects to this local
webserver. The editor also connects to this webserver: when the user clicks on
an element in the graphical view that contains source code location, a message
is sent from the webpage to the editor that contains a command for letting the
editor jump to the corresponding location in the Dezyne model. Note that large
parts of the daemon and JavaScript as part of a webpage rendered by the
webbrowser is produced using Dezyne.

Dezyne currently has a state diagram view, a system view depicting the
composition of a system model out of its subcomponent, and as mentioned before
the sequence diagram for the interaction with the simulator. The user can
either start the simulator directly, or the simulator is started when the
verification engine finds a problem and generates a counter example. The next
possible events are also depicted in the sequence diagram and if the user
selects a next event, this request is send from the webpage to the daemon, and
the daemon reruns the simulator with the current trace of events extended with
the requested event.

Figure 3: Visual Studio Code with Dezyne LSP and extended with a interactive
graphical view.

##  7 Application of Dezyne in Industry

Dezyne and its predecessor ASD have been intensively used by several Verum
customers for more than a decade. Verum customers are mainly high tech
equipment manufacturers; their binding factor is that the cost-of-non-quality
is high in the market they operate. Philips Healthcare is one of the first
customers and has the longest experience in using Verum products. For there
initial projects the impact of using this kind of low-entry Formal Methods
based tooling has been investigated [8, 13, 12, 11] and reported that the use
of the tool eliminated design errors earlier in the design process and
resulted in reduced development time and an ten fold reduction in reported
errors.

ASML is one of the leading manufacturers of semiconductor chip-making
equipment, and has been using our tooling in different projects for different
machines for some years now [10, 4, 15]. They also reported a similar decrease
in field defects and decrease in development time.

The most striking difference between ASD and Dezyne is that ASD has its own
proprietary Microsoft Excel resembling editor and is as such not language
based. This has had all kind of implications for incorporating ASD into
existing software development toolchains. For example, version management
tooling is predominantly text based. This alone was experienced as a
substantial obstacle in the acceptance of ASD. The feedback from users and the
noted shortcomings have served as primary input to design the Dezyne language
and its tooling.

Dezyne is being used by other customers which names we cannot disclose,
operating in the field of semiconductor equipment industry, electronic
analytical instruments, and egg grading, packing and processing machines.

##  8 Conclusions and Future Directions

Dezyne and its predecessor are being used at several high-tech equipment
manufacturing multinationals. So far several millions lines of generated code
are running in production around the world.

Software engineers without a formal methods background are productive and
comfortable due to the familiar concepts Dezyne is built on. Furthermore the
Dezyne language is designed to promote guiding principles of software
engineering. In order to avoid the state explosion problem it is especially
important to divide and conquer complexity in manageable sub-components, by
introducing internal Dezyne interfaces that capture the responsibilities of
these sub-components. The Dezyne verification engine guides the user in
achieving an intuitive understanding of the complexity of the problem at hand
and provides the user with input as to which parts of the system are
candidates to be broken up.

The introduction of Dezyne and its predecessor has resulted in a decrease in
software development time, a vast reduction in integration time, and a major
decrease of reported field defects. This shows that Formal Methods can bring a
lot of added value to industrial software engineers, provided that the method
hides the underlying complexities, can be used compositionally, generates
production quality and verified machine code, is properly packaged in a
familiar IDEs and graphical interactive views, and promotes the application of
proper software engineering principles.

Currently, the Dezyne simulator is restricted to a single component since this
is used to debug the counter examples found by the verification engine. We are
extending the simulator to bring multiple components in scope and even
complete systems. This will further support the user in validating their
systems, i.e. to check that the intended use cases and user stories are
present in the behaviour of system.

We aim to extend the verification engine to prove properties on several
components combined. The challenge here is to find a proper balance between
the expressiveness of the language defining these properties and the clarity
of the expressed properties such that a users can assess whether the formal
properties capture the intended informal requirements.

## References

  * [1]
  * [2] Rutger van Beusekom, Jan Friso Groote, Paul F. Hoogendijk, Robert Howe, Wieger Wesselink, Rob Wieringa & Tim A. C. Willemse (2017): _Formalising the Dezyne Modelling Language in mCRL2_.  In Laure Petrucci, Cristina Seceleanu & Ana Cavalcanti, editors: Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20, 2017, Proceedings, Lecture Notes in Computer Science 10471, Springer, pp. 217–233, 10.1007/978-3-319-67113-0_14.
  * [3] Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs & Tim A. C. Willemse (2019): _The mCRL2 Toolset for Analysing Concurrent Systems_.  In Tomáš Vojnar & Lijun Zhang, editors: Tools and Algorithms for the Construction and Analysis of Systems, Springer International Publishing, Cham, pp. 21–39, 10.1007/978-3-642-34281-3_26.
  * [4] Gemma Church (2017): _Have you ever wanted to press ‘delete’ on half a million lines of legacy code?_ Available at https://medium.com/@ASMLcompany/have-you-ever-wanted-to-press-delete-on-half-a-million-lines-of-legacy-code-96a76fdbc076.
  * [5] Carlo Ghezzi, Mehdi Jazayeri & Dino Mandrioli (2003): _Fundamentals of Software Engineering, 2nd Edition_.  Pearson.
  * [6] J.F. Groote & M.R. Mousavi (2014): _Modeling and analysis of communicating systems_.  MIT Press, 10.7551/mitpress/9946.001.0001.
  * [7] C.A.R. Hoare (1985): _Communicating Sequential Processes_.  Prentice-Hall International Series in Computer Science, Prentice Hall.  Available at http://www.usingcsp.com/cspbook.pdf.
  * [8] Jozef Hooman, Robert Huis in ’t Veld & Mathijs Schuts (2011): _Experiences with a Compositional Model Checker in the Healthcare Domain_.  In Zhiming Liu & Alan Wassyng, editors: Foundations of Health Informatics Engineering and Systems \- First International Symposium, FHIES 2011, Johannesburg, South Africa, August 29-30, 2011. Revised Selected Papers, Lecture Notes in Computer Science 7151, Springer, pp. 93–110, 10.1007/978-3-642-32355-3_6.
  * [9] Maurice Laveaux, Jan Friso Groote & Tim Willemse (2019): _Correct and efficient antichain algorithms for refinement checking_.  In Nobuko Yoshida & Jorge A. Pérez, editors: Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings, Lecture Notes in Computer Science, Springer, Germany, pp. 185–203, 10.1007/978-3-030-21759-4_11.
  * [10] A.A.H. Osaiweran, J. Marincic & J.F. Groote (2017): _Assessing the quality of tabular state machines through metrics._ In: Proceedings - 2017 IEEE International Conference on Software Quality, Reliability and Security, QRS 2017, IEEE Press, pp. 426–433, 10.1109/QRS.2017.52.  2017 IEEE International Conference on Software Quality, Reliability and Security (QRS) ; Conference date: 25-07-2017 Through 29-07-2017.
  * [11] A.A.H. Osaiweran, M.T.W. Schuts, J.J.M. Hooman, J.F. Groote & B.J. Rijnsoever, van (2016): _Evaluating the effect of a lightweight formal technique in industry_.  International Journal on Software Tools for Technology Transfer 18(1), pp. 93–108, 10.1007/s10009-015-0374-1.
  * [12] Ammar Osaiweran, Mathijs Schuts & Jozef Hooman (2014): _Experiences with incorporating formal techniques into industrial practice_.  Empir. Softw. Eng. 19(4), pp. 1169–1194, 10.1007/s10664-013-9251-2.
  * [13] Ammar Osaiweran, Mathijs Schuts, Jozef Hooman & Jacco H. Wesselius (2013): _Incorporating Formal Techniques into Industrial Practice: an Experience Report_.  Electron. Notes Theor. Comput. Sci. 295, pp. 49–63, 10.1016/j.entcs.2013.04.005.
  * [14] A. W. Roscoe (1997): _The Theory and Practice of Concurrency_.  Prentice Hall PTR, USA.
  * [15] R. Wester & J. Koster (2015): _The Software behind Moore’s Law_.  IEEE Software 32(02), pp. 37–40, 10.1109/MS.2015.53.