=Paper=
{{Paper
|id=Vol-2289/paper2
|storemode=property
|title=Using LNT Formal Descriptions for Model-Based Diagnosis
|pdfUrl=https://ceur-ws.org/Vol-2289/paper2.pdf
|volume=Vol-2289
|authors=Birgit Hofer,Radu Mateescu,Wendelin Serwe,Franz Wotawa
|dblpUrl=https://dblp.org/rec/conf/safeprocess/Hofer0SW18
}}
==Using LNT Formal Descriptions for Model-Based Diagnosis==
https://ceur-ws.org/Vol-2289/paper2.pdf
Using LNT Formal Descriptions for Model-Based Diagnosis
Birgit Hofer1 and Radu Mateescu2 and Wendelin Serwe2 and Franz Wotawa1
1
Institute for Software Technology, TU Graz, Inffeldgasse 16b/II, 8010 Graz, Austria
e-mail: {bhofer,wotawa}@ist.tugraz.at
2
Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP∗ , LIG, 38000 Grenoble, France
e-mail: {Radu.Mateescu,Wendelin.Serwe}@inria.fr
Abstract primary purpose of validation, which can be done using test-
ing or formal verification. In case of a system model, either
Providing models for model-based diagnosis has test cases can be automatically extracted from the model
always been a challenging task. There has never or additional properties can be checked using the system
been an agreement on an underlying modeling model. Testing as a task can be seen as a falsification step
language, making it almost impossible to share for systems whereas formal verification as a proof whether
models within our community. In addition, there certain properties are holding generally.
are other domains like formal methods or model- The objective behind this paper is to show on the exam-
based testing relying on system models for formal ple of LNT [4], that these formal specification languages
verification and automated test case generation. can not only be used for verification, but also for diagno-
Although, there we face the situation of different sis of systems. If formal models in LNT can be effectively
modeling languages as well, the question remains used for diagnosis, first we would be able to re-use these
whether it is possible to re-use these models in LNT models in a diagnosis setting, and second we could use
the context of model-based diagnosis. In this pa- LNT as a general modeling language that can be used for
per, we elaborate on this question and show how simulation, verification, and also diagnosis of the same sys-
models written in LNT can be used for fault local- tem. For this purpose, we introduce a general wrapper com-
ization only requiring simple modification. This ponent that adds diagnosis capabilities to any LNT model
allows re-using formal method’s models for diag- of the same component. Hence, we do not use the original
nosis directly. Besides discussing the underlying LNT model for diagnosis but an extended model where each
principles, we also present a use case showing the component that should be considered for diagnosis has to be
applicability of the methods. replaced with its corresponding wrapper component. Such a
wrapper component cannot only capture the unknown faulty
behavior, which is used in consistency-based diagnosis [5]
1 Introduction but also fault models used in abductive diagnosis [6].
Despite the fact that model-based diagnosis offers a lot of Besides discussing the methodologies behind the appli-
advantages compared to other approaches of diagnosis, its cation of LNT to diagnostic reasoning, we also report on
use in practice, despite running as part of prototype im- applying diagnosis to a model of the data encryption stan-
plementations and case studies, is somehow limited. One dard where we were able to localize faults using the basic
reason behind is that modeling in general is a non trivial concept of wrapper components for diagnosis.
task and that there is a lack on commonly agreed modeling This paper is organized as follows: To be self contained,
languages that are capable of providing the right means for we first discuss preliminaries including model-based diag-
modeling for diagnosis. This includes capturing temporal nosis and the basic concepts behind LNT. Afterwards, we
behavior and also dealing with the right level of abstraction. introduce the methodology behind using LNT models for
In many industrial applications being able to handle time diagnosis including the concept of wrapper components and
appropriately as well as models that closely capture phys- obtaining diagnosis candidates from them. Furthermore, we
ical properties is essential and for some of those issues a report on the results obtained from a case study based on
specialized diagnosis procedure has already been presented, the data encryption standard where we manually introduced
including diagnosis for communication systems (e.g. [1] faults. Finally, we discuss related research and conclude the
or [2]) or the use of modeling languages like Modelica paper.
for extracting models to be used for model-based diagnosis
(see [3]).
In this paper, we tackle the challenge of providing models 2 Preliminaries
for model-based diagnosis. But instead of relying on mod-
els used for simulation, we elaborate on the use of speci- In this section, we discuss the basic definitions of model-
fication languages for diagnosis. Formal specification lan- based diagnosis and formal methods in order to be self-
guages have been developed for modeling systems with the contained. We mainly focus on formal methods and intro-
duce the modeling language LNT (formerly called LOTOS
∗
Institute of Engineering Univ. Grenoble Alpes New Technology) and CADP (Construction and Analysis of
From a diagnosis system we immediately come to a diag-
M1
a nosis problem, when adding observations.
x x
A1 Definition 2.2 (Diagnosis problem). Given a diagnosis sys-
b
M2
+ f tem (SD, COMP ) and a logical sentence OBS describing
the given observations. The tuple (SD, COMP , OBS ) is a
c x y
A2 diagnosis problem.
d + g Example 2. (cont. Ex. 1) For the d74 circuit we may use
M3 the following observation set OBS :
e
x z
in 1 (M 1) = 2 ∧ in 2 (M 1) = 3 ∧
in 1 (M 2) = 2 ∧ in 2 (M 2) = 3 ∧
in 1 (M 3) = 3 ∧ in 2 (M 3) = 2 ∧
Figure 1: The classical d74 circuit. out(A1) = 10 ∧ out(A2) = 12
Obviously, there is a fault in the circuit, because the out-
Distributed Processes) tools available1 . For the sake of sim- put of adder A1 needs to be 12 and not 10 as observed when
plicity, we make use of the classical d74 circuit from Fig- assuming all components to work as expected.
ure 1 often used in diagnosis literature, e.g., see [7], to ex- Given a diagnosis problem, a diagnosis should explain
plain both model-based diagnosis and formal methods based deviations between expected values at any input and out-
on LNT. put as well as intermediate connection between components,
and given observations. In consistency-based diagnosis a di-
2.1 Consistency-based diagnosis agnosis is defined as a set of components that when assumed
We briefly discuss the basic definitions behind model-based to behave abnormally and all other components are expected
diagnosis, and there consistency-based diagnosis in particu- to work correctly, will not contradict any observation when
lar, which are based on Reiter’s seminal work [5]. We start using the underlying system model. Formally, diagnoses are
defining a diagnosis system comprising a model SD and the defined as follows:
set of components COMP . The idea here is to allow only el- Definition 2.3 (Diagnosis). Given a diagnosis problem
ements of COMP to be working as expected or faulty. In or- (SD, COMP , OBS ). A set of components∆ ⊆ COMP
der to make the information regarding a component’s health is a diagnosis if and only if SD ∪ OBS ∪ Ab(C) | C ∈
state explicit, we introduce a predicate Ab(C) for each com-
∆ ∪ ¬Ab(C) | C ∈ COMP \ ∆ is satisfiable.
ponent C from COMP stating that C behaves abnormally.
The model SD itself covers the structure of a system and In this definition a diagnosis needs not to be minimal. We
the behavior of each component. In case of consistency- define a minimal diagnosis as a diagnosis where none of its
based diagnosis, only the correct behavior of components subsets is itself a diagnosis accordingly to Definition 2.3.
is covered. This can be formalized using rules of the form Example 3. (cont. Ex. 2) For the given observations and
¬Ab(C) → behavioral description. When modeling using the d74 model, the four sets {M 1}, {A1}, {M 2, M 3}, and
implications, we do not restrict the faulty behavior of com- {M 2, A2} are all minimal diagnoses and there are no other
ponents. In particular, a component may behave correctly minimal diagnoses.
even in case its health state indicates that it is faulty. For a The dual concept of diagnoses are conflicts, i.e., a set
detailed discussion on fault models we refer to [8]. of components that, when assumed to behave correctly, to-
Definition 2.1 (Diagnosis system). A diagnosis system is a gether with the model SD contradict the given observations
tuple (SD, COMP ) where SD is a set of logical sentences OBS .
describing the structure and behavior of the system, and Definition 2.4 (Conflict). Given a diagnosis problem
COMP the set of system components. (SD, COMP , OBS ). A set of components CO ⊆ COMP
Example 1. For the d74 circuit, we are able to specify the is a conflict, if and only if SD∪OBS ∪ ¬Ab(C) | C ∈ CO
behavior of the adder and multiplier components as follows: is a contradiction.
Example 4. (cont. Ex. 3) For the d74 circuit we
obtain 2 minimal conflicts, i.e.: {M 1, M 2, A1}, and
ADD(C) → ¬Ab(C) → out(C) = in 1 (C) + in 2 (C)
{M 1, M 3, A1, A2}.
MULT (C) → ¬Ab(C) → out(C) = in 1 (C) ∗ in 2 (C)
Reiter [5] showed that there is a close relationship be-
The structure of the circuit comprises a definition of the tween diagnoses and conflicts. In particular, every minimal
components and their connections. In this particular case diagnosis is a minimal hitting set of all conflicts. Reiter
COMP = {M 1, M 2, M 3, A1, A2}. also introduced an algorithm computing such hitting sets
where conflicts are computed during computation. Greiner
et al. [9] provided a corrected version of Reiter’s diagno-
MULT (M 1) ∧ MULT (M 2) ∧ MULT (M 3) ∧
sis algorithm. However, there are many other algorithms
ADD(A1) ∧ ADD(A2) ∧
available for computing diagnoses. Some are based on con-
out(M 1) = in 1 (A1) ∧ out(M 2) = in 2 (A1) ∧
flicts whereas the others compute diagnoses directly from
out(M 2) = in 1 (A2) ∧ out(M 3) = in 2 (A2)
the model and the given observations. Nica et al. [10] in-
The model of the d74 circuit comprises all the described troduced an empirical evaluation of the runtime of different
logical rules. diagnosis algorithms. Note that in this paper, we make use
of algorithms for computing diagnoses directly from mod-
1
http://cadp.inria.fr els.
2.2 Formal methods end var
LNT [11] culminates a 30-year effort [4] aimed at supple- end process
menting the international standard LOTOS [12] with lan- It repeatedly (instruction loop ... end loop) waits for
guage features borrowed from classical programming lan- two natural numbers (in1 and in2) on its gates IN1 and
guages in order to enhance its user-friendliness and allow IN2, computes the result as soon as both inputs are avail-
for a wider industrial dissemination. LNT is firmly rooted in able, and then outputs the result on its gate SUM (in a ren-
concurrency theory: its operational semantics is defined as dezvous, inputs are described by ?x, where x is a variable
an LTS (Labeled Transition System) and its composition op- that will be assigned by the rendezvous). The inputs are
erators are compatible with behavioral equivalences (bisim- read in parallel (instruction par ... end par), i.e., with-
ulations). out any constraint on the order. All gates are of channel type
In general, the behavior of an LNT model is defined as the NAT_C, specifying that a natural number is communicated
parallel composition of processes communicating and syn- during a rendezvous.
chronizing only by multiway rendezvous [13, 14]. Each of The process ADDER can be wrapped inside a pro-
these processes is described with usual programming con- cess ADDER_WRAP with a Boolean parameter faulty
structs (assignments, if-then-else, loops, etc.) and can ma- (corresponding to the predicate Ab), which, using an
nipulate data values and complex data structures (such as if-then-else, chooses between a call to the original pro-
lists and trees). cess ADDER and a faulty version. The faulty version is
LNT is the principal modeling language supported by the same as the body of the process ADDER excepting for
the CADP (Construction and Analysis of Distributed Pro- the computation of the result, in which the output of a
cesses) toolbox [15], which provides an extensive set of lan- concrete value is replaced by a nondeterministic assign-
guages and tools assisting the whole design process: com- ment (instruction “:= any Nat”), constrained by a pred-
pilation and rapid prototyping, interactive and guided sim- icate “P (in1, in2, result)” returning true if and
ulation, LTS generation, equivalence and model checking, only if the wrapped process should allow the output result
test case generation, and performance evaluation. Among for the inputs in1 and in2. For instance, P could be used to
these tools, the most useful for diagnosis are the LNT com- specify that certain bits of the result are forced to a constant.
pilers, the equivalence checker BISIMULATOR, the model
checker EVALUATOR [16], and the SVL language [17] for process ADDER_WRAP [IN1, IN2, SUM: NAT_C]
describing verification scenarios. There also exists tools for (faulty: Bool) is
if faulty then
(distributed) code generation and test case extraction. A
loop
noteworthy feature of BISIMULATOR and EVALUATOR var in1, in2, result: Nat in
is that these tools operate on the fly, i.e., they only explore par
the part of the model required to obtain a result. IN1 (?in1)
LNT and CADP have been used for many case studies || IN2 (?in2)
in various domains2 : avionics, cloud computing, distributed end par;
algorithms, hardware design, human-computer interaction, result := any Nat
industrial systems, etc. where P (in1, in2, result);
SUM (result)
end var
3 Using LNT for diagnosis end loop
To use an LNT model for diagnosis, it must be param- else
eterized to enable the selection of the set of components ADDER [IN1, IN2, SUM]
that should behave according to the considered fault model. end if
Concretely, this implies end process
1. to wrap all individual components inside wrapper pro- To represent the most generic failure model, where predi-
cesses with a Boolean parameter to select between nor- cate P always returns true, i.e., where any output can be
mal and faulty behavior and nondeterministically chosen, the wrapper process can be
2. to add these parameters to the overall system. simplified by removing the local variables, leaving all ren-
dezvous unconstrained (“?any Nat”):
3.1 Wrapping individual components process ADDER_WRAP_ND [IN1, IN2, SUM: NAT_C]
To illustrate the wrapping of a component, consider the fol- (faulty: Bool) is
lowing LNT model of an adder, such as A1, A2 in the d74 if faulty then
circuit. loop
par
process ADDER [IN1, IN2, SUM: NAT_C] is IN1 (?any Nat)
var in1, in2, result: Nat in || IN2 (?any Nat)
loop end par;
par SUM (?any Nat)
IN1 (?in1) end loop
|| IN2 (?in2) else
end par; ADDER [IN1, IN2, SUM]
result := in1 + in2; end if
SUM (result) end process
end loop
This approach can be generalized to arbitrary processes.
2
http://cadp.inria.fr/case-studies Indeed, it is sufficient to copy the original code and modify
any constraints on the rendezvous according to the chosen or checking inclusion modulo equivalence relations
fault model — in the extreme case removing the constraints (with BISIMULATOR).
completely. Note that the instantiation (step 2) and the use of on-the-
3.2 Analyzing faulty configurations fly verification techniques (step 4) help in handling models
with a large state space only a small fragment of which is
The behavior of the whole system is obtained by composing reachable and necessary to inspect.
all wrapper processes in parallel and synchronizing them ac- Once the LNT model of the system and components is
cording to the system architecture. The LNT MAIN process available, the analysis of various faulty configurations of the
describing the d74 circuit from Figure 1 is shown below. system can be readily performed using SVL [17] scripts in-
Each of the five components has a synchronization interface voking the appropriate CADP tools. For the d74 circuit,
consisting of its input and output gates. The gates corre- we can represent the observation set given in Example 2 by
sponding to the interaction of the system with its environ- the following event sequence in the SEQ format of CADP
ment (e.g., the entries IN1, IN2 of multiplier M1 or the out- (where each line corresponds to the label of transition):
put OUT2 of adder A2) are kept visible, whereas the gates
that connect and synchronize components (e.g., the output "IN1 !2"
C1 of M1 connected to the first input of A1), are abstracted "IN2 !3"
"IN3 !3"
away (i.e., hidden by the hide operator) in the final system:
"IN4 !2"
they are not in the list of gate parameters of MAIN. "IN5 !2"
process MAIN [IN1, IN2, IN3, IN4, IN5, "OUT1 !10"
OUT1, OUT2: NAT_C] "OUT2 !12"
(f1, f2, f3, f4, f5: Bool,
i1, i2, i3, i4, i5: Nat) is Assuming the observation sequence is stored in a file
hide C1, C2, C3: NAT_C in "obs.seq", the following SVL statements verify the in-
par clusion of the sequence (modulo the preorder of branching
IN1, IN2, IN3, IN4, IN5 -> bisimulation) in the models of the healthy system and of the
IN1 (i1); IN2 (i2); IN3 (i3); faulty system with diagnosis {M 2, M 3} from Example 3:
IN4 (i4); IN5 (i5); stop
|| IN1, IN3, C1 -> (* M1 *) % I1=2; I2=3; I3=3; I4=2; I5=2
MULTI_WRAP [IN1, IN3, C1] (f1) branching comparison
|| IN2, IN4, C2 -> (* M2 *) "obs.seq" <= "MAIN(false,false,false,
MULTI_WRAP [IN2, IN4, C2] (f2) false,false,$I1,$I2,$I3,$I4,$I5)" ;
|| IN3, IN5, C3 -> (* M3 *) branching comparison
MULTI_WRAP [IN3, IN5, C3] (f3) "obs.seq" <= "MAIN(false,true,true,
|| C1, C2 -> (* A1 *) false,false,$I1,$I2,$I3,$I4,$I5)" ;
ADDER_WRAP [C1, C2, OUT1] (f4) Note the usage of shell-script instructions (lines starting
|| C2, C3 -> (* A2 *)
ADDER_WRAP [C2, C3, OUT2] (f5)
with a %) to initialize the shell-script variables I1, ..., I5,
end par which are subsequently used to feed the input of the MAIN
end hide processes representing the two system configurations. The
end process health states of the components are set by giving appropriate
values to the Boolean parameters f1, ..., f5 of the MAIN
The health states of individual components (i.e., the val- processes. The results of the two verifications above show
ues of the predicate Ab) are given by the Boolean parame- that the observation sequence is absent in the healthy model
ters f1, ..., f5 of the MAIN process, which are used to instan- and present in the faulty one.
tiate the faulty arguments of the wrapper processes. The The same verification can be carried out using on-the-fly
values of inputs, injected into the system by the first behav- model checking, by encoding the existence of the obser-
ior of the par operator, are given by the i1, ..., i5 param- vation sequence as a weak possibility modality “<< ... >>
eters of MAIN. By varying these parameters of the model, true” in MCL [16] and then evaluating it on a given system
various faulty configurations of the system can be explored. configuration. The SVL statement (note the inlined MCL
In the CADP setting, the consistency-based diagno- formula) below performs this check (which yields a positive
sis approach, i.e., checking whether a set of components verdict, as expected) on the faulty configuration {M 1} from
∆ ⊆ COMP is a diagnosis for a diagnosis problem Example 3.
(SD, COMP , OBS ) can be carried out as follows:
property FAULTY_M1_OBS is
1. model the system structure SD and the behavior of in- "MAIN(true,false,false,false,false,
dividual components COMP in LNT, $I1,$I2,$I3,$I4,$I5)" |= with evaluator4
2. instantiate the system, specifying a component C as <<
faulty (via the corresponding parameter) if and only if "IN1 !2" .
"IN2 !3" .
C belongs to ∆, "IN3 !3" .
3. represent the observations OBS as temporal formulas "IN4 !2" .
(in MCL [16]) or sequences of events (i.e., a particular "IN5 !2" .
kind of LTS), and "OUT1 !10" .
"OUT2 !12"
4. determine the presence of observations in the consid- >> true ;
ered system configuration using on-the-fly verification expected TRUE
techniques, e.g., model checking (with EVALUATOR) end property ;
This consistency checking approach can be easily inte- results of several reference implementations. These verifi-
grated into classical diagnosis algorithms, such as HSDAG cation steps are described in [18] and can be replayed by
(Hitting Set Directed Acyclic Graph) [5], either by encod- executing the SVL script included in the CADP demo.
ing the diagnosis algorithm as an SVL script, or by connect- To obtain an incorrect output, we falsified the model of
ing an existing implementation of it with the CADP tool- the DES by modifying one entry in one of the S-boxes such
box, by implementing consistency checks by system calls that a single bit of output was flipped. Then we studied
to CADP’s equivalence and model checkers operating on whether using wrapper processes (on the original, correct
the LNT model of the system under diagnosis. model of the DES) could identify the S-box responsible for
the incorrect output. For the wrappers, we considered the
most generic fault model: hence, a faulty S-box may return
4 Case study: asynchronous DES circuit any 4-bit vector. The wrapper process for the S-Box S1 is:
To study the feasibility and scalability of the approach, we process S1_WRAPPER [INPUT: C6, OUTPUT: C4]
experimented with the LNT model of an asynchronous im- (faulty: Bool) is
plementation of the DES (Data Encryption Standard) [18]. if faulty then
This model is interesting, because it is publicly available loop
as a demo example of the CADP toolbox3 , because it is INPUT (?any BIT6);
complex (more than twenty processes and a corresponding OUTPUT (?any BIT4)
LTS with several million states and transitions), and be- end loop
else
cause cryptographic algorithms should challenge fault lo- S1 [INPUT, OUTPUT]
calization, as they aim to hide internal computations. end if
In a nutshell, the DES is a block-cipher taking three in- end process
puts: a Boolean indicating whether encryption or decryp-
tion is requested, a 64-bit key, and a 64-bit block of data. A faulty S-box may produce 16 possible outputs (rather
For each triple of inputs, the DES computes the 64-bit (de- than a single one), so that, due to the sixteen iterations of
)crypted data, performing sixteen iterations of the same ci- the DES, the complete model would have 1616 = 264 possi-
pher function, each iteration with a different 48-bit sub-key ble outputs. Because this is clearly too large, we simplified
extracted from the 64-bit key. the model of the DES to perform only a single iteration, so
The DES is specified as a data-flow diagram [19], which that the state space becomes manageable. For both, the cor-
translates smoothly to the architecture shown on Figure 2. rect and incorrect model, the corresponding LTS has 79,416
Roughly, a CONTROLLER schedules the flow of the key (re- states4 and 513,940 transitions (64 states and 82 transitions
spectively, the data) through the KEY_PATH (respectively, after reduction with strong bisimulation), and for a model
DATA_PATH). The main computation is performed by the
with a single activated wrapper, the corresponding LTS has
cipher function CIPHER in the DATA_PATH. 473,316 states and 3,204,445 transitions (1000 states and
2551 transitions after reduction with strong bisimulation).
The principal elements of CIPHER are so-called S-boxes
Checking the inclusion of the incorrect model in each
(noted S1, ..., S8 on Figure 2), which compute for a 6-bit
of the models with a single faulty S-box identifies the S-
input vector a 4-bit output vector. Given that each S-box is
box responsible for the incorrect output, because the inclu-
specified by a table with four rows and 16 columns (see Fig-
sion holds only for the model where the (incorrect) S-box
ure 3, taken from [19, Appendix 1], for S1 ), human errors
is faulty. Thus, there is no need to consider instances with
in implementing these tables are highly probable. In LNT,
multiple faulty S-boxes.
these tables are encoded as two-dimensional arrays (in LNT,
We used an SVL script to
constants are represented by functions without arguments)
1. generate and minimize the correct model, the incorrect
function S1 : S_BOX_ARRAY is model, and the eight models with one faulty S-box,
return
S_BOX_ARRAY 2. check that the correct and incorrect model are not
(ROW (14, 4, 13, 1, 2, 15, 11, 8, branching bisimilar,
3, 10, 6, 12, 5, 9, 0, 7), 3. check that the correct model is included (modulo the
ROW ( 0, 15, 7, 4, 14, 2, 13, 1, preorder of branching bisimulation) in each of the
10, 6, 12, 11, 9, 5, 3, 8), models with a faulty S-box, and
ROW ( 4, 1, 14, 8, 13, 6, 2, 11,
15, 12, 9, 7, 3, 10, 5, 0), 4. check whether the incorrect model is included (modulo
ROW (15, 12, 8, 2, 4, 9, 1, 7, the preorder of branching bisimulation) in one of the
5, 11, 3, 14, 10, 0, 6, 13)) models with a faulty S-box.
end function On a laptop with a Intel Core i5 M560 CPU at 2.67 Ghz and
The LNT model of the DES has been validated in several 8 MB of RAM, executing this SVL script takes about eleven
ways (see the SVL script of the CADP demo for details). In minutes, the bunch of the time being spent in the generation
particular, several properties expressing the correct ordering and minimization step (i.e., step 1); the comparisons with
of the sixteen iterations have been expressed as MCL for- BISIMULATOR (i.e., steps 2 to 4) only take seconds.
mulae and checked with EVALUATOR. Also, a prototype Experiments with other errors in the S-boxes, such as a
implementation was derived from the LNT model and used copy-paste error (replace the definition of an S-box by the
to check the correctness by comparing the result to known definition of another one), led to similar results, because in
a single iteration each S-box is called only once so that only
3 one error is visible.
ftp://ftp.inrialpes.fr/pub/vasy/demos/
4
demo_38 By construction, all these states are reachable.
DATA
CONTROLLER
IP
CS
FIRST_L FIRST_R COUNTER CTRL_DMUX_K
CHOOSE_R CTRL_MUX_LR CTRL_SHIFT
CRYPT
CR_FX
CR_CL E CTRL_MUX_LR CTRL_MUX_K
CHOOSE_L
ER KEY
CL_XR
XOR_48 PC1
F_K
IS1 IS2 IS3 IS4 IS5 IS6 IS7 IS8
CHOOSE_K
S1 S2 S3 S4 S5 S6 S7 S8
K KKK
OS1 OS2 OS3 OS4 OS5 OS6 OS7 OS8
SHIFT
SK
P
CIPHER
DUP_K
FX_XR
I_K
XOR_32
PC2
OUTPUT_L OUTPUT_R XR_CR
SUBKEY
IIP
DATA_PATH KEY_PATH
OUTPUT
Figure 2: Architecture of the DES asynchronous circuit
Figure 3: Table specification of the S-box S1
5 Related Work errors in safety-critical, real-time systems. Starting from an
execution trace violating a given safety property, counterfac-
Shapiro was one of the first who introduced an automated tual reasoning is used to distinguish component failures that
software debugging approach in the 80’s. Davis [20] and actually contributed to the outcome from failures that had
Reiter [5] proposed model-based diagnosis approaches to no impact on the violation of the property. Blaming was im-
locate faults in hardware. In the 90’s, Console et al. [21] ap- plemented in [29] through a reduction to a model checking
plied model-based diagnosis to software, in particular logic problem for timed automata.
programs. Bond [22] improved the work of Console et al.. Debugging of LNT descriptions was also considered,
In the late 90’s, several researchers used the principles of in addition to the classical verification features of CADP.
model-based diagnosis to locate faults in programs written Salaün and Ye [30] devised a coverage analysis based on in-
using sequential, concurrent, and functional programming serting probes (special actions) at suitable places in an LNT
languages [23–25]. We refer the interested reader to Wong description without disturbing its behavior (i.e., the inserted
et al.’s overview paper on software fault localization [26]. probes, if considered as internal actions, yield a behavior
Pill and Quaritsch [27] proposed a scenario-based ap- branching bisimilar to the original one). The probes enable
proach for diagnosing faults in formal LTL specifications. to track the execution of decisions and statement blocks in
In contrast to our work, they support weak and strong fault the underlying LTS model, and thus to detect lacks in cov-
models. Peischl et al. [28] proposed to use Modelica mod- erage and/or anomalies in the LNT description.
els to describe cyber-physical systems and to derive fault Barbon et al. [31] proposed an approach to facilitate
models from these models. the analysis of (sequence) counterexamples produced by a
Another way of diagnosing faults in component-based model checker when evaluating a temporal property on an
systems is blaming, introduced by Goessler and Aste- LNT description. This is achieved by spotting, in a given
fanoaiei [29] to determine the components responsible for counterexample, the actions triggering a switch of the sys-
tem execution from incorrect to correct behavior. These [3] Johan de Kleer, Bill Janssen, Daniel G. Bobrow, Tolga
actions indicate possible causes of errors, being especially Kurtoglu, Bhaskar Saha, Nicholas R. Moore, and Sar-
useful for large and intricate counterexamples. Both ap- avan Sutharshana. Fault augmented Modelica models.
proaches [30, 31] have been automated in connection with In 24th Int. Workshop on Principles of Diagnosis (DX),
CADP, but are generally applicable to formal languages pages 71–78, 2013.
with action-based, interleaving semantics. [4] Hubert Garavel, Frédéric Lang, and Wendelin Serwe.
From LOTOS to LNT. In Joost-Pieter Katoen, Rom
6 Conclusion Langerak, and Arend Rensink, editors, ModelEd,
In this paper, we introduced a method that allows to use TestEd, TrustEd – Essays Dedicated to Ed Brinksma
models written in LNT for fault localization. The underly- on the Occasion of His 60th Birthday, volume 10500
ing methodology is based on the concept of wrapper compo- of Lecture Notes in Computer Science, pages 3–26.
nents that are themselves written in LNT. There the idea is to Springer-Verlag, October 2017.
introduce a variable representing the health state of the com- [5] Raymond Reiter. A theory of diagnosis from first prin-
ponent and to distinguish the correct behavior implemented ciples. Artificial Intelligence, 32(1):57–95, 1987.
in the original LNT model from the faulty behavior where
a simulator can use all domain values for the component’s [6] Luca Console, Daniele Theseider Dupré, and Pietro
parameters. The approach is not limited to capture the un- Torasso. On the relationship between abduction
known faulty behavior but also to introduce failure modes and deduction. Journal of Logic and Computation,
together with their corresponding models, e.g., in order to 1(5):661–690, 1991.
introduce stuck-at faults. The models are used together with [7] Johan de Kleer and Brian C. Williams. Diagnosing
a script to find all single faults of a system via setting one multiple faults. Artificial Intelligence, 32(1):97–130,
health variable for a component to faulty after the other and 1987.
stating the rest of the components as working as expected. [8] Johan de Kleer, Alan K. Mackworth, and Raymond
Besides the underlying foundations, we also present a
Reiter. Characterizing diagnosis and systems. Artifi-
case study using the well-known data encryption standard
cial Intelligence, 56(2-3):197–222, 1992.
(DES) were we are able to determine all the manually in-
troduced faults using the proposed model. For model-based [9] Russell Greiner, Barbara A. Smith, and Ralph W.
diagnosis the advantages are (1) to be able to make use of Wilkerson. A correction to the algorithm in Reiter’s
a modeling language that was developed for system verifi- theory of diagnosis. Artificial Intelligence, 41(1):79–
cation for diagnosis, and (2) to obtain a rich set of already 88, 1989.
developed models and tools, which can now be further re- [10] Iulia Nica, Ingo Pill, Thomas Quaritsch, and Franz
used for fault localization. Wotawa. The route to success - a performance com-
Future research will include further improving diagnosis parison of diagnosis algorithms. In International Joint
via more closely integrating the LNT tools with available di- Conference on Artificial Intelligence (IJCAI), pages
agnosis algorithms and further experiments to assess the po- 1039–1045, Bejing, China, 2013.
tential and scalability of the approach. In particular, we plan
to experiment with different failure models in LNT, multiple [11] David Champelovier, Xavier Clerc, Hubert Garavel,
faults, and more available LNT models of other case studies. Yves Guerte, Christine McKinty, Vincent Powazny,
Frédéric Lang, Wendelin Serwe, and Gideon Smeding.
Acknowledgments Reference Manual of the LNT to LOTOS Translator
(Version 6.7). INRIA, Grenoble, France, July 2017.
We are grateful to Hermann Felbinger and Josip Bozic for
their very much helpful discussions finally leading to this [12] ISO/IEC. LOTOS – A Formal Description Technique
paper and the LNT model wrapper. The research presented Based on the Temporal Ordering of Observational Be-
in the paper has been funded in part by the Austrian Re- haviour. International Standard 8807, International Or-
search Promotion Agency (FFG) under grant 865248 (Se- ganization for Standardization – Information Process-
curing Web Technologies with Combinatorial Interaction ing Systems – Open Systems Interconnection, Geneva,
Testing - SecWIT), RIDINGS (RIgorous DesIgN of GALS September 1989.
Systems) project of the PHC Amadeus program, and the Ré- [13] Stephen D. Brookes, C. A. R. Hoare, and A. W.
gion Auvergne-Rhône-Alpes within the program ARC 6. Roscoe. A Theory of Communicating Sequential Pro-
cesses. Journal of the ACM, 31(3):560–599, July 1984.
References [14] Hubert Garavel and Wendelin Serwe. The Unher-
[1] Yannick Pencolé and Marie-Odile Cordier. A for- alded Value of the Multiway Rendezvous: Illustration
mal framework for the decentralised diagnosis of large with the Production Cell Benchmark. In Holger Her-
scale discrete event systems and its application to manns and Peter Höfner, editors, Proceedings of the
telecommunication networks. Artif. Intell., 164(1- 2nd Workshop on Models for Formal Analysis of Real
2):121–170, 2005. Systems (MARS’17), Uppsala, Sweden, volume 244 of
[2] Gianfranco Lamperti and Marina Zanella. Context- Electronic Proceedings in Theoretical Computer Sci-
sensitive diagnosis of discrete-event systems. In Toby ence, pages 230–270, April 2017.
Walsh, editor, IJCAI 2011, Proceedings of the 22nd In- [15] Hubert Garavel, Frédéric Lang, Radu Mateescu, and
ternational Joint Conference on Artificial Intelligence, Wendelin Serwe. CADP 2011: A Toolbox for
Barcelona, Catalonia, Spain, July 16-22, 2011, pages the Construction and Analysis of Distributed Pro-
969–975. IJCAI/AAAI, 2011. cesses. Springer International Journal on Software
Tools for Technology Transfer (STTT), 15(2):89–107, [28] Bernhard Peischl, Ingo Pill, and Franz Wotawa. Us-
April 2013. ing Modelica programs for deriving propositional horn
[16] Radu Mateescu and Damien Thivolle. A Model clause abduction problems. In KI, volume 9904 of
Checking Language for Concurrent Value-Passing Lecture Notes in Computer Science, pages 185–191.
Systems. In Jorge Cuellar, Tom Maibaum, and Kaisa Springer, 2016.
Sere, editors, Proceedings of the 15th International [29] Gregor Gössler and Lăcrămioara Aştefănoaei. Blam-
Symposium on Formal Methods (FM’08), Turku, Fin- ing in component-based real-time systems. In Pro-
land, volume 5014 of LNCS, pages 148–164. Springer ceedings of the 14th International Conference on Em-
Verlag, May 2008. bedded Software, EMSOFT’14, pages 7:1–7:10, New
[17] Hubert Garavel and Frédéric Lang. SVL: a Script- York, NY, USA, 2014. ACM.
ing Language for Compositional Verification. In [30] Gwen Salaün and Lina Ye. Debugging Process Al-
Myungchul Kim, Byoungmoon Chin, Sungwon Kang, gebra Specifications. In VMCAI 2015, volume 8931,
and Danhyung Lee, editors, Proceedings of the 21st page 18, Mumbai, India, January 2015. Springer.
IFIP WG 6.1 International Conference on Formal [31] Gianluca Barbon, Vincent Leroy, and Gwen Salaün.
Techniques for Networked and Distributed Systems Debugging of Concurrent Systems Using Counterex-
(FORTE’01), Cheju Island, Korea, pages 377–392. ample Analysis. In Mehdi Dastani and Marjan Sirjani,
IFIP, Kluwer Academic Publishers, August 2001. Full editors, Revised selected papers of 7th International
version available as INRIA Research Report RR-4223. Conference on Fundamentals of Software Engineering
[18] Wendelin Serwe. Formal Specification and Verifica- (FSEN 2017), Tehran, Iran, volume 10522 of Lecture
tion of Fully Asynchronous Implementations of the Notes in Computer Science, pages 20–34. Springer-
Data Encryption Standard. In Rob van Glabbeek, Verlag, April 2017.
Jan Friso Groote, and Peter Höfner, editors, Proceed-
ings of the International Workshop on Models for For-
mal Analysis of Real Systems (MARS’15), Suva, Fiji,
volume 196 of Electronic Proceedings in Theoreti-
cal Computer Science. Open Publishing Association,
2015.
[19] National Institute of Standards and Technology. Data
encryption standard (DES). Federal Information Pro-
cessing Standards Publication 46-3, October 1999.
[20] Randall Davis. Diagnostic reasoning based on struc-
ture and behavior. Artificial Intelligence, 24:347–410,
1984.
[21] Luca Console, Gerhard Friedrich, and Daniele Thesei-
der Dupré. Model-based diagnosis meets error diag-
nosis in logic programs. In Proceedings 13th Inter-
national Joint Conf. on Artificial Intelligence, pages
1494–1499, Chambery, August 1993.
[22] Gregory W. Bond. Logic Programs for Consistency-
Based Diagnosis. PhD thesis, Carleton University,
Faculty of Engineering, Ottawa, Canada, 1994.
[23] Gerhard Friedrich, Markus Stumptner, and Franz
Wotawa. Model-based diagnosis of hardware designs.
Artificial Intelligence, 111(2):3–39, July 1999.
[24] Markus Stumptner and Franz Wotawa. Debugging
Functional Programs. In Proceedings 16th Inter-
national Joint Conf. on Artificial Intelligence, pages
1074–1079, Stockholm, Sweden, August 1999.
[25] Cristinel Mateis, Markus Stumptner, and Franz
Wotawa. Modeling Java Programs for Diagnosis. In
ECAI, pages 171–175, Berlin, Germany, 2000. IOS
Press.
[26] W. Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, and
Franz Wotawa. A survey on software fault localization.
IEEE Trans. Software Eng., 42(8):707–740, 2016.
[27] Ingo Pill and Thomas Quaritsch. Behavioral diag-
nosis of LTL specifications at operator level. In In-
ternational Joint Conference on Artificial Intelligence,
pages 1053–1059, 2013.