language=java, keywordstyle=, basicstyle=, mathescape=true, escapechar=|,
commentstyle=, frame=single

# SAT-Based Extraction of Behavioural Models for Java Libraries with
Collections

Larisa Safina<EMAIL_ADDRESS>INRIAFrance and  Simon Bliudze
<EMAIL_ADDRESS>INRIAFrance

(2022)

###### Abstract.

Behavioural models are a valuable tool for software verification, testing,
monitoring, publishing etc. However, they are rarely provided by the software
developers and have to be extracted either from the source or from the
compiled code. In the context of Java programs, a number of approaches exist
for building behavioural models. Most of these approaches rely on the analysis
of the compiled bytecode. Instead, we are looking to extract behavioural
models—in the form of Finite State Machines (FSMs)—from the Java source code
to ensure that the obtained FSMs can be easily understood by the software
developers and, if necessary, updated or integrated into the original source
code, e.g. in the form of annotations. Modern software systems are huge, rely
on external libraries and interact with their environment. Hence, extracting
useful behavioural models requires abstraction. In this paper, we present an
initial approach to this problem by focusing on the extraction of FSMs
modelling library APIs. We focus on the analysis of Java code involving the
use of collections. To this end, we encode the operational semantics of
collection operations using patterns of Boolean predicates. These patterns are
instantiated based on the analysis of the source code of API implementation
methods to form an encoding of the possible FSM transitions. A SAT solver is
then used to determine the enabledness conditions (guards) of these
transitions.

API, breaking changes, behavioral models, FSM, Java

††copyright: acmcopyright††journalyear: 2022

##  1\. Introduction

Behavioral models are a valuable tool for supporting the process of building
the correct software, that could be beneficial during all phases of the
development lifecycle: design and implementation (Montesi, 2015; Voinea et
al., 2020; Bravetti and Zavattaro, 2019), testing and verification (Corbett,
2000; Bartolo Burlò et al., 2020), coordination and monitoring (Gabbrielli et
al., 2019; Mavridou et al., 2017), deployment (Bravetti et al., 2020) etc.

One of the particular problem behavioral models could help to address is
maintaining the API correctness. APIs provide a great way of scoping,
encapsulating and presenting library functions (Bloch, 2006). Reusing
components with the help of APIs helps to reduce the cost of software systems
development and to increase their quality (Espinha et al., 2015; Brito et al.,
2017, 2018). However, API development is not free of problems. When designed
badly, API offers inefficient or even incorrect code requiring writing
additional code to deal with it, which leads directly to the increased
development cost (Henning, 2007). When documented badly and without clear
explanation of the correct sequence of method usage, API can demonstrate
exceptional behaviours (Ancona et al., 2018). External APIs, being a black
box, can contain error-prone dependencies and make systems prone to breaking
changes that have to be addressed in the client code. A new version of an
external interface evolving independently can break backward compatibility and
may cause runtime failures of client systems. According to studies, breaking
changes are being present in the significant amount of all new releases (70%
(Raemaekers et al., 2017), 75% (Dietrich et al., 2014), and 80% (Dig et al.,
2006)). One can argue that building a dynamic model of libraries to help the
developer understand the behaviour of methods operating on collections
contradicts the fundamental principle of information hiding: a developer
relying on knowledge of the API implementation would produce code even more
prone to the breaking changes we want to address. We believe, however, that if
a signature of an API method provides a developer with the insufficient
information, she will need to make her assumptions in any case whether they
are supported by the extracted model or not. But comparing the two models of
two different releases can show a developer if any breaking changes were
introduced.

There exist various approaches based on behavioral models to deal with such
problems possessing different levels of formality (from graphical
representation (Cook et al., 2017) to employing behavioral types (Ancona et
al., 2016)) and ways of being produced and presented. In general, these models
are expected to be expressive, rigourous, intuitive, well-structured and
possess the adequate level of abstraction (be sufficiently detailed and
precise) (Harel and Gery, 1997). Such models could complement the code
(Rumbaugh et al., 2004), be extracted from it (Dig et al., 2006; Parízek and
Lhoták, 2012), from its binaries (Raemaekers et al., 2017), from some
intermediate representation or from other models (Cruz-Filipe et al., 2017;
Dardha et al., 2017), from the execution traces (Lorenzoli et al., 2008) or be
created to synthesize the code from them (Harel and Gery, 1997).

We are interested in building behavioral models that have a tight connection
with API implementation source code to provide feedback to developers on the
behavior of the program. In this paper, we propose an approach to semi-
automatic extraction of behavioral models for APIs written in Java in the form
of Finite State Machines (FSMs), focusing on the code operating on
collections.

The paper is structured as follows. In Section 2, we introduce a simple
running example. In Section 3, we present our approach to model extraction. In
Section 4, we discuss our assumptions and future work directions. Section 5
concludes the paper.

##  2\. Running Example

Let’s imagine the API created for the users of a pharmaceutical company. In
particular it allows users to create reservations for the set of medications
and to manipulate this collections: add or remove elements. Each medication
can have two identifiers where the second is the one provided by a third-party
vendor. When a detail to be added or removed both ids are checked (see the
code snippet bellow)

⬇

class ExampleImpl implements ExampleAPI {

private Set<String> idSet;

public ExampleImpl() {

1: idSet = new HashSet<>();

}

public void add(String id){

1: idSet.add(id); // See |{\color{dkgreen}\secn{encoding}}| for the line

} // numbers in the left margin

public void removeId(String idMain, String idOpt) {

1: idSet.remove(idMain);

if (idMain != idOpt) {

2: idSet.remove(idOpt);

} else {

3: }

}

}

Figure 1. Running example source code

During the last code review it was decided to migrate idSet collection from
the HashSet to the TreeSet to present the order of the elements. However, this
led to the unexpected exception, when some user tried to remove a medicine
having only one id (remove("LK32EJ2", null)). This exception is not visible at
the compilation but can be catched by the static code analysers, and it is
clearly visible if we compare the behavioral models generated for the two
versions of the code (see Figures 2 and 3).

Figure 2. Behavioural model for the $\mathtt{HashSet}$ implementation Figure
3. Behavioural model for the $\mathtt{TreeSet}$ implementation

These models show the result of calling the API methods add and remove. We
model the states with the predicates we used to create this abstraction. The
transitions are labeled with the API method names, some of them have the
guards (values in square brackets) which are the conditions based on the
methods variables evaluated dynamically, that have to be satisfied in order to
fire the transition.

##  3\. Model extraction approach

###  3.1. Simplifying assumptions

We based our work on Java Collection Framework JDK 17—the most recent version
at the time of writing (jav, 2021)—and considered its General Purpose
Implementations (GPI). We studied each GPI to capture its behaviour and to
define its operational semantics taking into account differences in the
implementation of methods for various interfaces. For the sake of brevity, we
discuss only $\mathtt{Set}$ collections.

We focus on the contribution of collections to the object state. Thus, the
defining property of sets, i.e. the absence of duplicates, is irrelevant.
Other properties that can be taken into account are  (1) whether the
collection is ordered and  (2) whether it permits null values.  Here, we focus
on the latter.

Furthermore, since the operation of enlarging the collection is called
implicitly, we disregard the initial capacity and the load factor of the
collection. Similarly, since element retrieval is not based on their position
in the collection, we do not have to keep track of the insertion order. In
particular, these assumptions allow us to process $\mathtt{HashSet}$ and
$\mathtt{LinkedHashSet}$ in the same manner. For $\mathtt{TreeSet}$, we have
extra rules for adding and removing $\mathtt{null}$ elements.

In addition, we make the following assumptions that simplify the presentation.
We summarise them here—further details are provided in Section 3.2. We will
discuss the validity of these assumptions in Section 4. We assume that:

  1. (1)

all conditions used in branching statements ($\mathtt{if}$, $\mathtt{while}$
etc.) are Boolean expressions referring exclusively to comparisons of values
and the $\mathtt{contains()}$ and $\mathtt{isEmpty()}$ operations on
collections

  2. (2)

the source code is formatted in such a manner that there is at most one
operator per line, all branching statements have all their openning and
closing braces and the closing braces are placed on separate lines from any
other operators (cf. the example in Figure 1)

  3. (3)

there are only two types—collections and values—and any value can be stored in
any collection

  4. (4)

all loops terminate.

We plan to gradually resolve these simplifications up to the limits modern
model checking and other static analysis techniques will permit.

###  3.2. Boolean encoding of method behaviour

Our approach relies on the predicate abstraction idea from (Graf and Saïdi,
1997). For each method in the API under consideration, we proceed as follows.

Given a method, we consider a _context_ comprising a set of collection symbols
$C$ and a set of value symbols $V$. The symbols in $V$ can be literal
constants (e.g. $\mathtt{``Hello!"}$, $\mathtt{null}$), variables, method
parameters etc. For two symbols $v_{1},v_{2}\in V$ (idem for $c_{1},c_{2}\in
C$), we write $v_{1}\equiv v_{2}$ if they are the same symbol; $v_{1}=v_{2}$
denotes the predicate stating that their values are equal.

The definition of the context is a parameter of the approach, determining, in
particular, the degree of refinement of the resulting model. Context values
are used to form the following predicates:

  * •

$\mathit{eq}_{v_{1},v_{2}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(v_{1}=v_{2})$,
for $v_{1},v_{2}\in V$ ($v_{1}\not\equiv v_{2}$)

  * •

$\mathit{eq}_{c_{1},c_{2}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(c_{1}=c_{2})$,
for $c_{1},c_{2}\in C$ ($c_{1}\not\equiv c_{2}$)

  * •

$\mathit{cnt}_{c,v}$ holds for $v\in V$ and $c\in C$ if $v$ is contained in
$c$

  * •

$\mathit{empty}_{c}$ holds for $c\in C$ if $c$ is empty

  * •

$\mathit{e}$ holds if an exception has been thrown

We postulate the following axioms,

  1. (1)

$\mathit{ax}_{\ref{ax:same:value}}(c,v_{1},v_{2})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(\mathit{eq}_{v_{1},v_{2}}\implies\mathit{cnt}_{c,v_{1}}=\mathit{cnt}_{c,v_{2}})$

  2. (2)

$\mathit{ax}_{\ref{ax:same:collection}}(c_{1},c_{2},v)\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(\mathit{eq}_{c_{1},c_{2}}\implies\mathit{cnt}_{c_{1},v}=\mathit{cnt}_{c_{2},v})$

  3. (3)

$\mathit{ax}_{\ref{ax:empty}}(c,v)\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(\mathit{empty}_{c}\implies\lnot\mathit{cnt}_{c,v})$

Let $P$ be the set of all the predicates above and
$P^{\prime}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\\{p^{\prime}\,|\,p\in
P\\}$. Assume that all operators of the method are numbered sequentially from
1 to $n$, with the numbering of branching operators corresponding to their
closing braces (cf. Figure 1). For each predicate $p\in P$ and each
$i\in[0,n]$, we define a Boolean variable $p^{i}$ corresponding to the
valuation of $p$ after the execution of the operator $i$.

For a formula $\varphi\in\mathbb{B}[P,P^{\prime}]$, denote
$\varphi^{i,j}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\varphi\bigl{[}P^{i}/P\bigr{]}\bigl{[}P^{j}/P^{\prime}\bigr{]}$
the formula where each predicate $p$ (resp. $p^{\prime}$) is substituted by
the variable $p^{i}$ (resp. $p^{j}$). Similarly,
$\varphi^{i}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\varphi[P^{i}/P]$,
for $\varphi\in\mathbb{B}[P]$.

For a sequence of operators $\mathtt{s}$ and two indices $i,j\in[0,n]$
($i<j$), we define the encoding function $\mathit{enc}^{i,j}(\mathtt{s})$ as
shown in Figure 4, where $\mathtt{s}{\downarrow}$ denotes _the index of the
last operator_ in a sequence $\mathtt{s}$ and, in (4), $\varphi_{\mathtt{op}}$
is the formula encoding the semantics of the operator $\mathtt{op}$ (see
Section 3.3 below). A method $\mathtt{meth}$ with the body $\mathtt{s}$ is
then encoded by the formula

$\mathit{enc}(\mathtt{\mathtt{meth}})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\mathit{axioms}^{0}\land\mathit{enc}^{0,\mathtt{s}{\downarrow}}(\mathtt{s})\,,$

with the formula $\mathit{axioms}$ defined by (5).

(1)
$\displaystyle\mathit{enc}^{i,j}(\mathtt{op;s})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\mathit{enc}^{i,\mathtt{op}{\downarrow}}(\mathtt{op})\land\mathit{enc}^{\mathtt{op}{\downarrow},j}(\mathtt{s})$
(2) $\displaystyle\mathit{enc}^{i,j}(\mathtt{while\,(cnd)\
s})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\lnot\mathit{cnd}^{j}$
$\displaystyle\mathit{enc}^{i,j}(\mathtt{if\,(cnd)\ s_{1}\ else\
s_{2}})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\mathit{enc}^{i,\mathtt{s_{1}}{\downarrow}}(\mathtt{s_{1}})\land\mathit{enc}^{i,\mathtt{s_{2}}{\downarrow}}(\mathtt{s_{2}})$
(3) $\displaystyle{}\land\bigl{(}\mathit{cnd}^{i}\implies\bigwedge_{p\in
P}p^{j}=p^{\mathtt{s_{1}}{\downarrow}}\bigr{)}\land\bigl{(}\lnot\mathit{cnd}^{i}\implies\bigwedge_{p\in
P}p^{j}=p^{\mathtt{s_{2}}{\downarrow}}\bigr{)}$ (4)
$\displaystyle\mathit{enc}^{i,j}(\mathtt{op})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\varphi_{\mathtt{op}}^{i,j}\land\mathit{axioms}^{j}$
(5)
$\displaystyle\mathit{axioms}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}{}$
(14) $\displaystyle\bigwedge_{\begin{array}[]{@{}c@{}}\scriptstyle c\in C\\\
\scriptstyle v_{1},v_{2}\in V\\\ \scriptstyle v_{1}\not\equiv
v_{2}\end{array}}\mathit{ax}_{\ref{ax:same:value}}(c,v_{1},v_{2})\land\bigwedge_{\begin{array}[]{@{}c@{}}\scriptstyle
c_{1},c_{2}\in C\\\ \scriptstyle v\in V\\\ \scriptstyle c_{1}\not\equiv
c_{2}\end{array}}\mathit{ax}_{\ref{ax:same:collection}}(c_{1},c_{2},v)\land\bigwedge_{\begin{array}[]{@{}c@{}}\scriptstyle
c\in C\\\ \scriptstyle v\in V\end{array}}\mathit{ax}_{\ref{ax:empty}}(c,v)$
Figure 4. Definition of the encoding function
$\mathit{enc}^{\cdot,\cdot}(\mathtt{\cdot})$

###  3.3. Predicate semantics of operators

The predicate semantics of an operator $\mathtt{op}$ is given by a quadruple
$(C_{\mathtt{op}},V_{\mathtt{op}},P_{\mathtt{op}},f_{\mathtt{op}})$, where

  * •

$(C_{\mathtt{op}},V_{\mathtt{op}})$ is a context, comprising the sets
$C_{\mathtt{op}}$ and $V_{\mathtt{op}}$ of, respectively, collection and value
variables

  * •

$P_{\mathtt{op}}$ is a subset of predicates as in Section 3.2 indexed by the
variables from $C_{\mathtt{op}}$ and $V_{\mathtt{op}}$

  * •

$f_{\mathtt{op}}\in\mathbb{B}[P_{\mathtt{op}},P_{\mathtt{op}}^{\prime}]$ is a
Boolean formula on these predicates

Intuitively, $P_{\mathtt{op}}$ is the set of predicates whereof the valuations
_may_ be affected by the operator.

For example, consider the method $\mathtt{c.add(v)}$ of a $\mathtt{HashSet}$
$\mathtt{c}$. Its predicate semantics is given by the formula

$f_{\mathtt{c.add(v)}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\mathit{cnt}_{c,v}^{\prime}\land\lnot\mathit{empty}_{c}^{\prime}\,.$

Here, $C_{\mathtt{c.add(v)}}=\\{c\\}$, $V_{\mathtt{c.add(v)}}=\\{v\\}$,
$P_{\mathtt{c.add(v)}}=\\{\mathit{cnt}_{c,v},\mathit{empty}_{c}\\}$.

Let us consider, as another example, the method $\mathtt{c.clear()}$ of a
collection $\mathtt{c}$. Its predicate semantics is given by the formula

$f_{\mathtt{c.clear()}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\mathit{empty}_{c}^{\prime}\,.$

Despite $v$ not appearing in $f_{\mathtt{c.clear()}}$, we take the same
$C_{\mathtt{c.clear()}}=\\{c\\}$, $V_{\mathtt{c.clear()}}=\\{v\\}$ and
$P_{\mathtt{c.clear()}}=\\{\mathit{cnt}_{c,v},\mathit{empty}_{c}\\}$ as above.
Indeed, the value of the $\mathit{cnt}_{c,v}$ predicate, _for all value
symbols in the context_ , may be modified by this method, even though
$\mathit{ax}_{\ref{ax:empty}}$ means that this does not have to be specified
explicitly in $f_{\mathtt{c.clear()}}$.

For each operator invocation in the source code, some of the variables in
$C_{\mathtt{op}}$ and $V_{\mathtt{op}}$ will be positionally matched with the
symbols in the context $(C,V)$. E.g., for an invocation
$\mathtt{idSet.clear()}$, $c\in C_{\mathtt{c.clear()}}$ is matched to
$\mathit{idSet}\in C$ but $v\in V_{\mathtt{c.clear()}}$ is not matched to any
symbol in $V$. For the sake of clarity, let us abuse the notation as follows:
we denote $C_{\mathtt{op}}\setminus C$ (resp. $V_{\mathtt{op}}\setminus V$)
the set of variables that are not matched positionally.

The formula $\varphi_{\mathtt{op}}$ encoding the operator $\mathtt{op}$ (see
(4) in Figure 4) is then defined as follows:

(17)
$\displaystyle\varphi_{\mathtt{op}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\bigwedge_{\begin{array}[]{@{}c@{}}\scriptstyle\mu:C_{\mathtt{op}}\setminus
C\rightarrow C\\\ \scriptstyle\nu:V_{\mathtt{op}}\setminus V\rightarrow
V\end{array}}f_{\mathtt{op}}[\mu,\nu]\land\bigwedge_{p\in{P}_{\mathit{free}}}p^{\prime}=p$
(20)
$\displaystyle\text{with}\qquad{P}_{\mathit{free}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}P\setminus\bigcup_{\begin{array}[]{@{}c@{}}\scriptstyle\mu:C_{\mathtt{op}}\setminus
C\rightarrow C\\\ \scriptstyle\nu:V_{\mathtt{op}}\setminus V\rightarrow
V\end{array}}P_{\mathtt{op}}[\mu,\nu]\,,$

where $f_{\mathtt{op}}[\mu,\nu]$ denotes the formula obtained by substituting
each unmatched variable $c\in C_{\mathtt{op}}\setminus C$ (resp. $v\in
V_{\mathtt{op}}\setminus V$) by the symbol $\mu(c)$ (resp. $\nu(v)$) and
similarly for $P_{\mathtt{op}}[\mu,\nu]$.

Intuitively, the first conjunct in (17) means that the formula
$f_{\mathtt{op}}$ is instantiated for all possible values of the unmatched
variables. The second conjunct means that all predicates in $P$ that do not
appear in the semantics of $\mathtt{op}$ maintain their previous values.

Notice, finally, that a predicate $p^{\prime}$, with $p\in P_{\mathtt{op}}$,
that is not fully constrained by $f_{\mathtt{op}}$ might take any value,
representing the absence of the corresponding information. For instance,
consider the method $\mathtt{c.remove(v)}$ of a $\mathtt{HashSet}$
$\mathtt{c}$. Its predicate semantics is given by the formula

$f_{\mathtt{c.remove(v)}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\lnot\mathit{cnt}_{c,v}^{\prime}\land(\mathit{empty}_{c}\implies\mathit{empty}_{c}^{\prime})\,,$

with, again, $C_{\mathtt{c.remove(v)}}=\\{c\\}$,
$V_{\mathtt{c.remove(v)}}=\\{v\\}$ and
$P_{\mathtt{c.remove(v)}}=\\{\mathit{cnt}_{c,v},\mathit{empty}_{c}\\}$. If
$\mathtt{c}$ is not empty before the call to $\mathtt{c.remove(v)}$ it may or
may not become empty after the call, depending on whether $\mathtt{v}$ is the
only value contained therein.

###  3.4. Computing the FSM

Given a context $(C,V)$ with the corresponding set of predicates $P$ as
defined in Section 3.2, we observe that the symbols can be partitioned into
_state_ and _indeterminacy_ symbols: $C=C_{st}\uplus C_{nd}$ and
$V=V_{st}\uplus V_{nd}$, such that $C_{st}$ and $V_{st}$ contain constants and
class fields, whereas $C_{nd}$ and $V_{nd}$ contain method parameters,
unevaluated functions etc. This induces several partitions on the set of
predicates: $P=P_{st}\uplus P_{nd}$, such that $P_{st}$ is a subset of
predicates that refer only to symbols in $C_{st}$ and $V_{st}$.

A _state_ is a partial valuation $\sigma:P_{st}\rightharpoonup\mathbb{B}$. A
_concrete state_ is a total valuation $\sigma:P_{st}\rightarrow\mathbb{B}$. We
say that one state $\sigma_{1}$ _refines_ another $\sigma_{2}$, denoted
${\sigma_{1}}\prec{\sigma_{2}}$ if
$\operatorname{dom}(\sigma_{2})\subseteq\operatorname{dom}(\sigma_{1})$ and
$\sigma_{1}(p)=\sigma_{2}(p)$, for all $p\in\operatorname{dom}(\sigma_{2})$.
We say that a set of states $\Sigma$ is _complete_ if every state refines some
state of $\Sigma$, i.e. for every $\sigma:P_{st}\rightharpoonup\mathbb{B}$,
there exists $\hat{\sigma}\in\Sigma$, such that ${\sigma}\prec{\hat{\sigma}}$.
Notice that any complete set of states must comprise the empty valuation
$\sigma_{0}$, having $\operatorname{dom}(\sigma_{0})=\emptyset$. Clearly, for
any given implementation of an API, there can be different complete sets of
states. In particular, the set $\\{\sigma_{0}\\}$ is complete. So is the set
of all concrete states
$\bigl{\\{}\sigma\,\bigr{.}\bigl{|}\,\operatorname{dom}(\sigma)=P_{st}\bigr{\\}}\cup\\{\sigma_{0}\\}$.

Given a context $(C,V)$, a set of predicates $P$ and a complete set of states
$\Sigma$, we build a non-deterministic FSM
$(\Sigma,\sigma_{0},\mathit{A},\xrightarrow[]{})$, where $\sigma_{0}$ is the
initial state, $\mathit{A}$ is the set of methods provided by the API under
consideration and
${\xrightarrow[]{}}\subseteq\Sigma\times\mathit{A}\times\mathbb{B}[P_{nd}]\times\Sigma$
is the transition relation, where the third component is the transition
_guard_.

To compute the transition relation $\xrightarrow[]{}$, we proceed as follows.
For each method $\mathtt{meth}\in\mathit{A}$ and each pair of states
$\sigma_{1},\sigma_{2}\in\Sigma$, we define

$\varphi_{0}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\bigwedge_{p\in\operatorname{dom}{\sigma_{1}}}\bigl{(}p^{0}=\sigma_{1}(p)\bigr{)}\land\mathit{enc}(\mathtt{\mathtt{meth}})\land\bigwedge_{p\in\operatorname{dom}{\sigma_{2}}}\bigl{(}p^{\mathtt{\mathtt{meth}}{\downarrow}}=\sigma_{2}(p)\bigr{)}$

(see Section 3.2) and submit it to a SAT solver. If $\varphi_{0}$ is
satisfiable we obtain a model $m_{1}:\\{p^{i}\,|\,p\in
P,i\in[0,\mathtt{\mathtt{meth}}{\downarrow}]\\}\rightarrow\mathbb{B}$. We
define

$\varphi_{1}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}\varphi_{0}\land\lnot\bigwedge_{i=0}^{\mathtt{\mathtt{meth}}{\downarrow}}\bigwedge_{p\in
P}\bigl{(}p^{i}=m_{1}(p^{i})\bigr{)}$

and submit it to the SAT solver again, repeating until we obtain some
$\varphi_{n}$ that is unsatisfiable. The transition is then

$\sigma_{1}\xrightarrow[]{\mathtt{meth}[g]}\sigma_{2}\,,\qquad\text{with
}g=\bigvee_{i=1}^{n}\bigwedge_{p\in P_{nd}}\bigl{(}p=m_{i}(p^{0})\bigr{)}\,.$

Notice that, if $\varphi_{0}$ is unsatisfiable, we have $g=\mathit{false}$.

Applying this approach to the example in Figure 1 we obtain the FSMs in
Figures 2 and 3. We do so using the set of all concrete states, in which each
state is a combination of predicates from $P$ (predicates forming the states
could be selected to tune the level of the model’s abstraction, e.g in our
example we rely on the $\mathit{empty}_{c}$ predicate even though $P$ is not
limited by it. The common context for the $\mathtt{HashSet}$ version of the
example is $(\\{\mathit{idSet}\\},\emptyset)$. For methods $\mathtt{add}$ and
$\mathtt{removeId}$ we take the union with, respectively,
$(\emptyset,\\{\mathit{id}\\})$ and
$(\emptyset,\\{\mathit{idMain},\mathit{idOpt}\\})$. The predicates are the
same as in Section 3.2, with $P_{st}=\\{\mathit{empty}_{\mathit{idSet}}\\}$
(we exclude $\mathit{e}$, since it appears neither in the axioms nor in the
semantics of the operators involved).

For the $\mathtt{TreeSet}$ version, we add $\mathit{null}$ to the common
context and $\mathit{e}$ to $P_{st}$ since they appear in the semantics of the
operators, e.g.

$f_{\mathtt{c.add(v)}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(\mathit{eq}_{v,\mathit{null}}=\mathit{eq}_{v,\mathit{null}}^{\prime})\\\
{}\land\lnot\mathit{eq}_{v,\mathit{null}}\implies(\mathit{cnt}_{c,v}^{\prime}\land\lnot\mathit{empty}_{c}^{\prime}\land(\mathit{e}^{\prime}=\mathit{e}))\\\
{}\land\mathit{eq}_{v,\mathit{null}}\implies(\mathit{cnt}_{c,v}=\mathit{cnt}_{c,v}^{\prime}\land\mathit{empty}_{c}=\mathit{empty}_{c}^{\prime}\land\mathit{e}^{\prime})$
$f_{\mathtt{c.remove(v)}}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle\mathit{def}}}{{=}}}(\mathit{eq}_{v,\mathit{null}}=\mathit{eq}_{v,\mathit{null}}^{\prime})\\\
{}\land\lnot\mathit{eq}_{v,\mathit{null}}\implies(\lnot\mathit{cnt}_{c,v}^{\prime}\land(\mathit{empty}_{c}\implies\mathit{empty}_{c}^{\prime})\land(\mathit{e}^{\prime}=\mathit{e}))\\\
{}\land\mathit{eq}_{v,\mathit{null}}\implies(\mathit{cnt}_{c,v}=\mathit{cnt}_{c,v}^{\prime}\land\mathit{empty}_{c}=\mathit{empty}_{c}^{\prime}\land\mathit{e}^{\prime})$

The full Z3 encodings of the two versions can be found in (Anoymous, 2022).

##  4\. Discussion & Future work

The model extraction approach proposed above is based on ideas that are well-
known in the Formal Methods community. The novelty lies in their application
for the extraction of behavioural models from Java source code. More
importantly, our main goal is not to use these models for verification but
rather for assisting software engineers in the development process and,
eventually, for model-based monitoring and coordination. This allows us, in
particular, to aim for a less restrictive behavioural model, namely non-
deterministic FSMs with guards. This change of perspective also makes the
semi-automatic approach more acceptable: indeed, we believe that it is much
easier to get developers to help refining an existing model than to provide
one from scratch.

The semi-automatic nature of our approach arises from several levels of
parametrisation among which the key one is choosing the appropriate predicates
for the specification of the semantics of the basic operations. To some
extent, this remark addresses the simplifying assumption (1) in Section 3.1,
which can be substantially relaxed by including additional predicates to
define the semantics of the terms used in the conditions. Further relaxation
can, of course, be achieved by moving from SAT to SMT.

Deciding which symbols should be part of the context and which predicates
should be used for the encoding is a non-trivial task, which we believe cannot
be fully formalised. We see two approaches to address this question: input
from domain experts, i.e. developers, and various kinds of heuristics
(potentially including Machine Learning techniques). Both approaches—or
combinations whereof—provides directions for future work.

Assumptions (2) and (3) are obviously non-constraining. Moreover, in any
actual implementation, we would use Abstract Syntax Trees and Control Flow
Graphs to explore the source code and compute the Boolean encodings. This
would naturally eliminate the need for these two assumptions.

Thus, the strongest assumption that we have made is the loop termination
assumption (4), which would require deeper static analysis or assistance from
the developers for exhibiting loop variants, which we consider beyond the
near-future scope of this work.

We intend to develop a tool for extracting FSMs from Java source code based on
the approach proposed in this paper. In general, the tool will proceed along
the following steps (see Figure 5): collecting the information about the
sources under analysis and about the fields identified as key to the object
state (1); computing auxiliary data structures, and state values that can be
easily evaluated (2); then using different techniques to generate the FSM. The
last step differs for the basic types and collections. For instance, for
simple types, such as enumerations, simple interpretative techniques could
suffice (3). For complex types such as collections, we will rely on the SAT-
based approach presented in this paper (4).

Figure 5. Intended tool architecture

Finally, another point worth mentioning is the choice of the complete set of
states. For the sake of simplicity, we have chosen to use the set of all
concrete states. This can clearly be improved both a posteriori—e.g. reducing
the FSM by bisimilarity—and a priori—e.g. building the state space on the fly
to avoid unreachable states.

##  5\. Conclusion

We propose an approach to the extraction of behavioural models in the form of
non-deterministic FSMs with guards from Java implementations of library APIs.
The approach is semi-automatic since it is parametrised by the choice of
important symbols, predicates and states. This makes it highly flexible and
allows the integration of expert knowledge from developers. The presented
approach is fully formalised. Although the underlying ideas are well known in
the Formal Methods community, we believe that their combined application for
the extraction of FSMs with guards is novel and can be applied to the benefit
of the Software Engineering community. We are planning to develop a tool based
on the proposed approach and use it in our future projects for the purposes of
monitoring and coordination of software components.

## References

  * (1)
  * jav (2021) 2021\.  Java Collections Framework Overview.  https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/doc-files/coll-overview.html.  [Online; accessed 6-Jan-2022].
  * Ancona et al. (2016) Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2016.  Behavioral Types in Programming Languages.  _Found. Trends Program. Lang._ 3, 2-3 (2016), 95–230.  https://doi.org/10.1561/2500000031
  * Ancona et al. (2018) Davide Ancona, Francesco Dagnino, and Luca Franceschini. 2018\.  A Formalism for Specification of Java API Interfaces. In _Companion Proceedings for the ISSTA/ECOOP 2018 Workshops_ (Amsterdam, Netherlands) _(ISSTA ’18)_. Association for Computing Machinery, New York, NY, USA, 24–26.  https://doi.org/10.1145/3236454.3236476
  * Anoymous (2022) Anoymous. 2022.  Paper’s example z3-encoding.  https://doi.org/10.5281/zenodo.5913271
  * Bartolo Burlò et al. (2020) Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. 2020.  _Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)_.  227–235.  https://doi.org/10.1007/978-3-030-50086-3_13
  * Bloch (2006) Joshua Bloch. 2006\.  How to Design a Good API and Why It Matters. In _Companion to the 21st ACM SIGPLAN Symposium on Object-Oriented Programming Systems, Languages, and Applications_ (Portland, Oregon, USA) _(OOPSLA ’06)_. Association for Computing Machinery, New York, NY, USA, 506–507.  https://doi.org/10.1145/1176617.1176622
  * Bravetti et al. (2020) Mario Bravetti, Saverio Giallorenzo, Jacopo Mauro, Iacopo Talevi, and Gianluigi Zavattaro. 2020\.  A Formal Approach to Microservice Architecture Deployment. In _Microservices, Science and Engineering_.
  * Bravetti and Zavattaro (2019) Mario Bravetti and Gianluigi Zavattaro. 2019.  _Relating Session Types and Behavioural Contracts: The Asynchronous Case_.  29–47.  https://doi.org/10.1007/978-3-030-30446-1_2
  * Brito et al. (2018) Aline Brito, Laerte Xavier, Andre Hora, and Marco Valente. 2018.  Why and how Java developers break APIs. 255–265.  https://doi.org/10.1109/SANER.2018.8330214
  * Brito et al. (2017) Gleison Brito, Andre Hora, Marco Valente, and Romain Robbes. 2017.  On the Use of Replacement Messages in API Deprecation: An Empirical Study.  _Journal of Systems and Software_ 137 (12 2017).  https://doi.org/10.1016/j.jss.2017.12.007
  * Cook et al. (2017) Steve Cook, Conrad Bock, Pete Rivett, Tom Rutt, Ed Seidewitz, Bran Selic, and Doug Tolbert. 2017.  _Unified Modeling Language (UML) Version 2.5.1_.  Standard. Object Management Group (OMG).  https://www.omg.org/spec/UML/2.5.1
  * Corbett (2000) James C. Corbett. 2000\.  Using Shape Analysis to Reduce Finite-State Models of Concurrent Java Programs.  _ACM Trans. Softw. Eng. Methodol._ 9, 1 (Jan. 2000), 51–93.  https://doi.org/10.1145/332740.332741
  * Cruz-Filipe et al. (2017) Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi. 2017\.  The Paths to Choreography Extraction. In _Foundations of Software Science and Computation Structures_ , Javier Esparza and Andrzej S. Murawski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 424–440.
  * Dardha et al. (2017) Ornela Dardha, Simon J Gay, Dimitrios Kouzapas, Roly Perera, A Laura Voinea, and Florian Weber. 2017\.  Mungo and StMungo: Tools for Typechecking Protocols in Java.  _Behavioural Types: from Theory to Tools_ (2017), 309.
  * Dietrich et al. (2014) Jens Dietrich, Kamil Jezek, and Premek Brada. 2014\.  Broken promises: An empirical study into evolution problems in Java programs caused by library upgrades. In _2014 Software Evolution Week - IEEE Conference on Software Maintenance, Reengineering, and Reverse Engineering (CSMR-WCRE)_. 64–73.  https://doi.org/10.1109/CSMR-WCRE.2014.6747226
  * Dig et al. (2006) Danny Dig, Can Comertoglu, Darko Marinov, and Ralph Johnson. 2006.  Automated Detection of Refactorings in Evolving Components.  https://doi.org/10.1007/11785477_24
  * Espinha et al. (2015) Tiago Espinha, Andy Zaidman, and Hans-Gerhard Groß. 2015\.  Web API growing pains: Loosely coupled yet strongly tied.  _J. Syst. Softw._ 100 (2015), 27–43.
  * Gabbrielli et al. (2019) Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. 2019.  Guess Who’s Coming: Runtime Inclusion of Participants in Choreographies. In _The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday_ _(Lecture Notes in Computer Science, Vol. 11760)_ , Mário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, and Frank Valencia (Eds.). Springer, 118–138.  https://doi.org/10.1007/978-3-030-31175-9_8
  * Graf and Saïdi (1997) Susanne Graf and Hassen Saïdi. 1997.  Construction of Abstract State Graphs with PVS. In _Computer Aided Verification, 9th International Conference, CAV ’97, Haifa, Israel, June 22-25, 1997, Proceedings_ _(Lecture Notes in Computer Science, Vol. 1254)_ , Orna Grumberg (Ed.). Springer, 72–83.  https://doi.org/10.1007/3-540-63166-6_10
  * Harel and Gery (1997) D. Harel and E. Gery. 1997\.  Executable object modeling with statecharts.  _Computer_ 30, 7 (1997), 31–42.  https://doi.org/10.1109/2.596624
  * Henning (2007) Michi Henning. 2007\.  API: Design Matters: Why Changing APIs Might Become a Criminal Offense.  _Queue_ 5, 4 (may 2007), 24–36.  https://doi.org/10.1145/1255421.1255422
  * Lorenzoli et al. (2008) Davide Lorenzoli, Leonardo Mariani, and Mauro Pezzè. 2008\.  Automatic generation of software behavioral models.  _Proceedings - International Conference on Software Engineering_ , 501–510.  https://doi.org/10.1145/1368088.1368157
  * Mavridou et al. (2017) Anastasia Mavridou, Valentin Rutz, and Simon Bliudze. 2017\.  Coordination of Dynamic Software Components with JavaBIP.  https://doi.org/10.1007/978-3-319-68034-7_3
  * Montesi (2015) Fabrizio Montesi. 2015\.  Kickstarting Choreographic Programming.  https://doi.org/10.1007/978-3-319-33612-1_1
  * Parízek and Lhoták (2012) Pavel Parízek and Ondřej Lhoták. 2012.  Predicate Abstraction of Java Programs with Collections. In _Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications_ (Tucson, Arizona, USA) _(OOPSLA ’12)_. Association for Computing Machinery, New York, NY, USA, 75–94.  https://doi.org/10.1145/2384616.2384623
  * Raemaekers et al. (2017) S. Raemaekers, A. van Deursen, and J. Visser. 2017\.  Semantic versioning and impact of breaking changes in the Maven repository.  _Journal of Systems and Software_ 129 (2017), 140–158.  https://doi.org/10.1016/j.jss.2016.04.008
  * Rumbaugh et al. (2004) James Rumbaugh, Ivar Jacobson, and Grady Booch. 2004\.  _Unified Modeling Language Reference Manual, The (2nd Edition)_.  Pearson Higher Education.
  * Voinea et al. (2020) A. Voinea, Ornela Dardha, and Simon Gay. 2020.  _Typechecking Java Protocols with [St]Mungo_.  208–224.  https://doi.org/10.1007/978-3-030-50086-3_12