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.