Keywords

1 Introduction

The development process of critical control systems is based essentially on the rigorous execution of guides and regulations [1, 4, 10, 11]. Specialised agencies (like FAA, EASA and ANAC in the aviation field) use these guides and regulations to certify such systems.

Safety plays a crucial role on critical systems and it is the responsibility of the safety assessment process. ARP-4761 [1] defines several techniques to perform safety assessment. One of them is Fault Tree Analysis (FTA). It is a deductive process that uses trees to model faults and their dependencies and propagation. In such trees, the premises are the leaves (basic events) and the conclusions are the roots (top events). Intermediary events use gates to combine basic events and each kind of gate has its own combination semantics definition. For example, the most traditional gates are OR and AND. They combine the events as at least one shall occur and all shall occur, respectively. To analyse fault trees, their structures are then abstracted as Boolean expressions called structure expressions. The analysis with these two traditional gates uses a well-defined algorithm based on Shannon’s method—which originated the Binary Decision Diagrams (BDDs) [3, 6]—to obtain minimal cut sets from the structure expressions and a general formula to calculate the probability of top events.

Besides the traditional OR and AND gates, the Fault Tree Handbook defines other gates. For example the Priority-AND gate, which considers the order of occurrence of events. Although the work reported in [24] defines these new gates, there is no algorithm to perform the analysis of trees that contain such new gates. This motivated the introduction of two new kinds of fault trees: Dynamic Fault Trees [9] (DFTs) and Temporal Fault Trees [26, 27] (TFTs). These variant trees can capture sequence dependencies of fault events in a system. The difference from Temporal Fault Tree [26, 27] (TFT) to Dynamic Fault Tree [9] (DFT) is that Temporal Fault Trees [26, 27] (TFTs) use temporal gates directly, while Dynamic Fault Trees [9] (DFTs) do not—Dynamic Fault Trees [9] (DFTs) gates are an abstraction of temporal gates. To differentiate traditional fault trees from the other two, we will call traditional fault trees as Static Fault Trees (SFTs).

Both TFT and DFT also use structure expressions ([19, 27], respectively) to abstract the tree to enable their analyses. Despite some limitations related to spare gates [19], the structure expressions used in TFTs and DFTs can be formulated in terms of a generic order-based operator.

The NOT operator is absent in the algebras showed in [16, 18, 25, 27]. They conceptually remove such an operator to avoid incorrect analysis, as there is no consensus about the relevance of its use: (i) it can be misleading, generating non-coherent analysis [22], or (ii) it can be essential in practical use [5]. The algebra created in our previous work [8] defines the NOT operator and allows its use.

In structure expressions, the variables represent fault events and the expressions represent a top event, an operational mode of a system. The combination of all operational modes is expected to describe the complete behaviour of a system. For example, if no fault occurs, then the system is in a nominal state; if all faults occur, then the system is definitely in a faulty state. Possibilities in between vary accordingly to the fault tolerance strategies employed in a system. The analysis of all possibilities is what we call completeness analysis. For Boolean algebra, it is equivalent to verify if all rows in a truth table (in which the variables are fault events) are considered in at least one structure expression.

Architecture Analysis and Design Language [12] (AADL) is a standard language to model (among other features) system structure and component interaction. AADL has several tools to perform different analyses to obtain SFT to perform FTA. But AADL’s assertions framework does not express order explicitly as needed for TFT and DFT analyses.

On the analyses of systems and its constituents, there is a distinction of operational modes and error events. Operational modes refer to the behaviour that is perceived on the boundaries of a system. Error events, on the other hand, represent the behaviour detected in a constituent of a system. Such error events may relate to an operational mode, but not necessarily. We abstract these differences and leave the distinction as a parameter. In this article, we refer to such a set as operational modes.

Another concern, left untreated in the literature, is the undesirable possibility of non-determinism in structure expressions. What guarantees can we provide to detect non-determinism in erroneous behaviour? For example, if a commission is observed when fault A is active and an omission is observed when faults A and B are active, then the system may behave non-deterministically with a commission or omission when both A and B are active (A and B implies A). In this work we show three different approaches to check the non-determinism: (i) verify its existence, (ii) indicate which set of operational modes are active for a combination of faults, or (iii) what is the combination of faults that activates a set of operational modes.

Writing and analysing expressions with order-related operators is more complex than analysing expressions with Boolean operators only. In this work, we define a formal Activation Logic (AL) that works together with an inner algebra to perform analysis of system structure and component interaction with a focus on fault modelling and fault propagation, tackling the complexity introduced by order-related operators. AL receives an algebra and the set of operational modes of a system as parameters. The choice of algebra defines which structure expressions can be obtained: if Boolean algebra is passed as a parameter, the AL can generate structure expressions with Boolean operators (SFT); if the Algebra of Temporal Faults  [8] (ATF) is passed as a parameter, the AL can generate structure expressions with order-related operators (TFT and DFT). The AL requires that the inner algebras provide a set of properties (tautology and contradiction) and semantic values. The use of the NOT is essential: besides its use in expressions, we use the complement to normalise the expressions to provide healthy expressions. To obtain critical event expressions used in FTs and to denote faults propagation, the AL provides a predicates notation and verification of non-determinism.

This paper is organised as follows: in Sect. 2 we show the concepts used as the basis for this work. Section 3 presents the proposed AL, and Sect. 4 the case study and the application of the proposed AL. Finally, we present our conclusions and future work in Sect. 5.

2 Background

Faults modelling depends on which analyses we want to perform. For instance, in fault trees, even if a fault can be repaired, it is considered as a non-repairable fault. A fault tree is a snapshotFootnote 1 of a system’s, subsystem’s or component’s topology of faults. The time relations on fault events in TFTs and DFTs allows the analysis of different configurations (or snapshots) of a system, subsystem or component. We discuss these time relations in Sect. 2.1.

Structure expressions are used to analyse fault trees. In general, a structure expression is obtained from gates semantics and basic events. Basic events become variables and gates become operators (a gate may become one or more operators). In Sect. 2.2 we explain these structure expressions for SFTs, TFTs and DFTs.

The AL proposed in this work depends on algebraic rules and relies on a complement operator. Our previous work showed the ATF that extends the Boolean algebra, thus providing the NOT operator and some properties and rules to use the algebra. In Sect. 2.3 we show these properties and rules used in this work.

2.1 Time Relation of Fault Events

The most general case for time relations is to consider that each fault event has a continuous time duration. They are the basis on how fault events discretization are defined. The point of view in this work is the analysis of the effects caused by a combination of faults in a snapshot of a system state. In Fig. 1 we show all possibilities of events relations in a continuous timeline (from A to B; the converse relation is similar):

  1. a.

    A starts before and ends after B has started, but before B has ended;

  2. b.

    A starts before B and ends after B has ended (A contains B);

  3. c.

    B starts after A, but they end at the same time;

  4. d.

    A and B start at the same time, but A ends before B;

  5. e.

    A and B start and end at the same time;

  6. f.

    A starts before B and ends when B starts.

  7. g.

    A starts and ends before B starts;

Considering that fault occurrence corresponds to the start of a fault event and its duration, from Fig. 1 we clearly identify which event comes first: A comes before B, except in the cases (d) and (e), where they start exactly at the same time. If fault events are independent (they are not susceptible to have a common cause) then the probability of their occurrences starting at the same time is very low. The relations (f) and (g) shows the case that the system was repaired, thus A is not active when B starts. In Sect. 2.3 we show that the ATF abstracts the relation of events in continuous time as an exclusive before relation, based on fault occurrence (it is similar—at least implicitly—to what is reported in [17, 27]).

Fig. 1.
figure 1

Relation of two events with duration

Full size image

2.2 Structure Expressions

Structure expressions in FTA are defined in terms of set theory, using symbols for fault events occurrence. If a fault event symbol is in a set, then it means that fault has occurred. A set is a combination of fault events that causes the top-level event of a tree. A structure expression of a tree is denoted by a set of sets of fault event combinations. The OR gate becomes the union operator between sets and the AND gate, the intersection. For example, if a system contains fault events a, b, and c, fault trees for this system contain at most all these three events. The occurrence of the fault event a is denoted by a set of sets A, which contains the following sets:

  1. 1.

    \(\left\{ a\right\} \): only a occurs;

  2. 2.

    \(\left\{ a,b\right\} \): a and b occur;

  3. 3.

    \(\left\{ a,c\right\} \): a and c occur;

  4. 4.

    \(\left\{ a,b,c\right\} \): all three events occur.

The fault tree in Fig. 2 contains only two events and the resulting structure expression for this tree is the expression \(A \cap B\) (TOP), where A and B are the sets of sets that contain a and b, respectively. The resulting combinations for TOP are \(\left\{ a,b\right\} \) and \(\left\{ a,b,c\right\} \) (fault events a and b occur in all possibilities).

Fig. 2.
figure 2

Very simple example of a fault tree

Full size image

After obtaining structure expressions, the next step is to reduce the expressions to a canonical form to obtain the minimal cut sets. Minimal cut sets are the sets that contain the minimum and sufficient events to activate the top-level failure. That is, minimal cut sets are the smallest sets of fault events that, if all occur, cause the top-level failure to occur. Probabilistic analysis is then performed on these events to obtain the overall probability of occurrence of the top-level event. The Fault Tree Handbook shows an algorithm based on Shannon’s method to reduce structure expressions to obtain minimal cut sets. The Boolean expression of the tree shown in Fig. 2 is \(TOP = A \wedge B\).

Structure expressions are also present in TFTs [25, 27, 28], through the PandoraFootnote 2 methodology. These expressions use the FTA operators OR and AND, and three new operators related to events ordering: Priority-AND (PAND), Priority-OR (POR), and Simultaneous-AND (SAND). The semantics of the PAND in TFTs is similar to the semantics of the Priority-AND described in the Fault Tree Handbook. To avoid ambiguous expressions, the semantics in TFTs is stated in terms of natural numbers (instead of Boolean values), using a sequence value function. For every possibility it assigns a sequence value to each fault event. For example, if event A occurs before event B, then the sequence value of A is lower than the sequence value of B, and one formula to express this is A PAND B.

In TFTs, an invariant on sequence values is that there are no gaps for assigned values higher than zero. For example, if faults A and B occur at the same time and there are only these two events, then they should both be assigned value 1. On the other hand, if A occurs before B, then the assigned values are 1 and 2, respectively. Value zero means that the event is not active in the combination. Table 1 shows the semantics of all TFT operators with sequence values.

Table 1. TFT operators and sequence value numbers
Full size table

The reduction of TFT expressions is achieved using dependency trees. In a dependency tree, if all children of a tree node are true, then the node is also true. Conversely, if a node is true, then all its children are also true. An issue with dependency trees is that they grow exponentially. Accordingly to the work reported in [28], it is already infeasible to deal with seven fault events in TFTs. They use an alternative solution based on modularisation and algebraic laws [27] to tackle this.

Structure expressions are also used in DFTs. In [16, 17, 20] fault events occur in a specific time and are instantaneous, stated through a date-of-occurrence function. As the date-of-occurrence function is stated in continuous time, the probability of two events occurring at the same time is negligible. In fact, useful information is obtained from the possibilities of relation in time of the occurrence of the events.

The work reported in [16, 17, 20] describe an algebra with operators OR and AND, and three new operators to express events ordering: (i) non-inclusive-before, (ii) simultaneous, and (iii) inclusive-before. The non-inclusive-before and the simultaneous operators are similar to TFT’s POR and SAND operators, respectively (although in [16, 17, 20] the only true result with the simultaneous operator happens if the operands are the same). The inclusive-before is a composition of the non-inclusive-before and the simultaneous operators.

The work reported in [23, 29] shows the top-level events probability calculation for DFTs by converting them to a simplified version, using only order-based operators. Such a simplified version, which is based on a modified BDD that includes an order-based operator, creates Sequential BDDs that are used to perform the probabilistic analysis.

From the previous explanation, we can conclude that an order-based operator is present on the analyses of TFTs and DFTs. Each approach describes a new algebra (without the NOT operator) based on different representations of events ordering with similar theorems to reduce expressions to a canonical form.

2.3 The Algebra of Temporal Faults

Recall from Sects. 2.1 and 2.2 that fault events are independent on one another if the events are not susceptible to a common cause. Also, the simultaneity of events is probabilistically impossible, so one event occurs exclusively before or after another one, inducing an order of occurrence of events. Moreover, the analysis of fault events considers that they have started and are active, as a snapshot of a system (faulty) state. Thus, the ATF is not used to analyse the effects of a repairable fault. For example, the cases that are possible to analyse with the theory shown here are (a), (b) and (c) of Fig. 1, in Sect. 2.1.

The set-theoretical abstraction of structure expressions for SFTs [24, pp. VI-11] is very close to a Free Boolean Algebra  [13, pp. 256–266] (FBA), where each generator in FBA corresponds to a fault event symbol in fault trees. In FBAs, as generators are “free”, they are independent on one another and Boolean formulas are written as a set of sets of possibilities, which are similar to the structure expressions of SFTs.

The set of sets for FBAs is the denotational semantics for Boolean algebras. We use the concept of generators to define the denotational semantics of ATF using a set of lists without repetition (distinct lists). The choice of lists is because this structure inherently associates a generator to an index, making implicit the representation of order. These lists are composed by non-repeated elements because the events in fault trees are non-repairable, thus they do not occur more than once.

In the following, we show the definitions and laws of the ATF used in Sect. 4. To avoid repetition, let S, T and U be sets of distinct lists. A list xs is distinct if it has no repeated element. So, if x is in xs, then it has a unique associated index i and we denote it as \(x = xs_{i}\).

The ATF form a free algebra, similarly to FBAs. Infimum and Supremum are defined as set intersection (\(\cap \)) and union (\(\cup \)) respectively. The order within the algebra is defined with set inclusion (\(\subseteq \)).

To distinguish the permutations that are not defined in FBA, we need a new operator. The definition of XBefore (\(\rightarrow \)) is given in terms of list concatenation:

(1)

where the \(\mathbf {set}\,\) function returns the set of the elements of a list, and concatenates two lists.

In some cases it is more intuitive to use the XBefore definition in terms of lists slicing because it uses indexes explicitly. Lists slicing is the operation of taking or dropping elements, obtaining a sublist. In slicing, the starting index is inclusive, and the ending is exclusive. Thus the first index is 0 and the last index is the list length. For example, the list \(xs_{\left[ i..\left| xs\right| \right] }\) is equal to the xs list, where \(\left| xs\right| \) is the list length. We use the following notation for list slicing:

$$\begin{aligned} xs_{\left[ i..j\right] }&= \text {starts at } i \text { and ends at } j-1 \end{aligned}$$
(2a)
$$\begin{aligned} xs_{\left[ ..j\right] }&= xs_{\left[ 0..j\right] }\end{aligned}$$
(2b)
$$\begin{aligned} xs_{\left[ i..\right] }&= xs_{\left[ i..\left| xs\right| \right] } \end{aligned}$$
(2c)

List slicing and concatenation are complementary: concatenating two consecutive slices results in the original list:

(3)

There is an equivalent definition of XBefore with concatenation using lists slicing:

$$\begin{aligned} S \rightarrow T = \{zs | \exists i \bullet zs_{\left[ ..i\right] } \in S \wedge zs_{\left[ i..\right] } \in T\} \end{aligned}$$
(4)

A variable in ATF is defined by one generator, and denotes its occurrence:

$$\begin{aligned} \mathbf {var}\, x = \{zs | x \in zs\} \end{aligned}$$
(5)

The following expressions are sufficient to define the ATF in terms of an inductively defined set (\(\mathbf {atf}\)):

$$\begin{aligned} \mathbf {var}\, x&\in \mathbf {atf}&\text {Variable} \end{aligned}$$
(6a)
$$\begin{aligned} S \in \mathbf {atf}\implies -S&\in \mathbf {atf}&\text {Complement, Negation} \end{aligned}$$
(6b)
$$\begin{aligned} S \in \mathbf {atf}\wedge T \in \mathbf {atf}\implies S \cap T&\in \mathbf {atf}&\text {Intersection, }Infimum \end{aligned}$$
(6c)
$$\begin{aligned} S \in \mathbf {atf}\wedge T \in \mathbf {atf}\implies S \rightarrow T&\in \mathbf {atf}&\text {XBefore} \end{aligned}$$
(6d)

Following the definitions, the expressions below are also valid for \(\mathbf {atf}\) (using DeMorgan laws):

$$\begin{aligned} UNIV&\in \mathbf {atf}&\text {Universal set, True} \end{aligned}$$
(6e)
$$\begin{aligned} \left\{ \right\}&\in \mathbf {atf}&\text {Empty set, False} \end{aligned}$$
(6f)
$$\begin{aligned} S \in \mathbf {atf}\wedge T \in \mathbf {atf}\implies S \cup T&\in \mathbf {atf}&\text {Union, }Supremum \end{aligned}$$
(6g)

The following expressions are valid for generators a and b and are sufficient to show that the generators are independent:

$$\begin{aligned}&\mathbf {var}\, a = \mathbf {var}\, b \iff a = b \end{aligned}$$
(7a)
$$\begin{aligned}&\mathbf {var}\, a \not \subseteq - \mathbf {var}\, b \end{aligned}$$
(7b)
$$\begin{aligned}&\mathbf {var}\, a \ne -\mathbf {var}\, b \end{aligned}$$
(7c)
$$\begin{aligned}&- \mathbf {var}\, a \not \subseteq \mathbf {var}\, b \end{aligned}$$
(7d)
$$\begin{aligned}&- \mathbf {var}\, a \ne \mathbf {var}\, b \end{aligned}$$
(7e)

Expressions (6a) to (6g) and (7a) to (7e) imply that the ATF without the XBefore operator (1) forms a Boolean algebra based on sets of lists. And this is also equivalent to an FBA with the same generators.

Note that, as the ATF is a conservative extension of a Boolean algebra, the NOT operator is defined here, so expressions in the ATF can use it.

In the following section, we show properties as a generalisation of the preconditions of laws related to XBefore.

Temporal properties ( tempo ). Temporal properties give a more abstract and less restrictive shape on the XBefore laws. These properties avoid the requirement that every operand of XBefore should be a variable (5).

The first temporal property is about disjoint split. If the first part of a list is in a given set, then every remainder part is not. So, if a generator is in the beginning of a list, it must not be at the ending (and vice-versa).

$$\begin{aligned} \mathbf {tempo}_{1} S&= \forall i, j, zs \bullet i \le j \implies \lnot \left( zs_{\left[ ..i\right] } \in S \wedge zs_{\left[ j..\right] } \in S \right) \end{aligned}$$
(8a)
$$\begin{aligned} \mathbf {tempo}_{2} S&= \forall i, zs \bullet zs \in S \iff zs_{\left[ ..i\right] } \in S \vee zs_{\left[ i..\right] } \in S \end{aligned}$$
(8b)
$$\begin{aligned} \mathbf {tempo}_{3} S&= \forall i, j, zs \bullet j < i \implies \left( zs_{\left[ j..i\right] } \in S \iff zs_{\left[ ..i\right] } \in S \wedge zs_{\left[ j..\right] } \in S \right) \end{aligned}$$
(8c)
$$\begin{aligned} \mathbf {tempo}_{4} S&= \forall zs \bullet zs \in S \iff (\exists i \bullet zs_{\left[ i..\left( i+1\right) \right] } \in S) \end{aligned}$$
(8d)

The second temporal property is about belonging to one sublist in the beginning or in the end. If a generator is in a list, then it must be at the beginning or at the ending.

The third temporal property is about belonging to one sublist in the middle. If a generator belongs to a sublist between i and j, then it belongs to the sublist that starts at first position and ends in j and to the sublist that starts at i and ends at the last position (both sublists contain the sublist in the middle).

Finally, if a generator belongs to a list, then there is a sublist of size one that contains the generator.

Variables have all four temporal properties. For a generator x, the following is valid:

$$\begin{aligned} \mathbf {tempo}_{1} \left( \mathbf {var}\, x\right) \wedge \mathbf {tempo}_{2} \left( \mathbf {var}\, x\right) \wedge \mathbf {tempo}_{3} \left( \mathbf {var}\, x\right) \wedge \mathbf {tempo}_{4} \left( \mathbf {var}\, x\right) \end{aligned}$$

Other expressions also meet one or more temporal properties:

$$\begin{aligned} \mathbf {tempo}_{1} S \wedge \mathbf {tempo}_{1} T&\implies \mathbf {tempo}_{1} \left( S \cap T \right) \end{aligned}$$
(9a)
$$\begin{aligned} \mathbf {tempo}_{3} S \wedge \mathbf {tempo}_{3} T&\implies \mathbf {tempo}_{3} \left( S \cap T \right) \end{aligned}$$
(9b)
$$\begin{aligned} \mathbf {tempo}_{2} S \wedge \mathbf {tempo}_{2} T&\implies \mathbf {tempo}_{2} \left( S \cup T \right) \end{aligned}$$
(9c)
$$\begin{aligned} \mathbf {tempo}_{4} S \wedge \mathbf {tempo}_{4} T&\implies \mathbf {tempo}_{4} \left( S \cup T \right) \end{aligned}$$
(9d)

XBefore Laws. We now show some laws to be used in the algebraic reduction of ATF formulas. The laws follow from the definition of XBefore, from events independence, and from the temporal properties.

We define events independence (\({\triangleleft }{\triangleright }\)) as the property that one operand does not imply the other. For example, we need to avoid that the operands of XBefore are \(\mathbf {var}\, a\) and \(\mathbf {var}\, a \cup \mathbf {var}\, b\) (it results in {}, see (11e)).

$$\begin{aligned} S {\triangleleft }{\triangleright }T = \forall i, zs \bullet \lnot \left( zs_{\left[ i..\left( i+1\right) \right] } \in S \wedge zs_{\left[ i..\left( i+1\right) \right] } \in T \right) \end{aligned}$$
(10)

The absence of occurrences ({}, the empty set of \(\mathbf {atf}\)) is a “0” for the XBefore operator.

$$\begin{aligned} \left\{ \right\} \rightarrow S = \left\{ \right\}&\text {left-false-absorb} \end{aligned}$$
(11a)
$$\begin{aligned} S \rightarrow \left\{ \right\} = \left\{ \right\}&\text {right-false-absorb} \end{aligned}$$
(11b)
$$\begin{aligned} \left( S \rightarrow T \right) \cup S = S&\text {left-union-absorb} \end{aligned}$$
(11c)
$$\begin{aligned} \left( T \rightarrow S \right) \cup S = S&\text {right-union-absorb} \end{aligned}$$
(11d)
$$\begin{aligned} \mathbf {tempo}_{1} S \implies S \rightarrow S = \left\{ \right\}&\text {non-idempotent} \end{aligned}$$
(11e)
$$\begin{aligned} \mathbf {tempo}_{1} S\wedge \mathbf {tempo}_{1} T\wedge&\nonumber \\ \mathbf {tempo}_{1} U\implies&\nonumber \\ S \rightarrow (T \rightarrow U ) = (S \rightarrow T ) \rightarrow U&\text {associativity} \end{aligned}$$
(11f)

The XBefore is absorbed by one of the operands: if one of the operands may happen alone, thus the order with any other operand is irrelevant. However, an event cannot come before itself, thus XBefore is not idempotent Finally, the XBefore is associative.

To allow formula reduction we need the relation of XBefore to the other Boolean operators. We use the XBefore as operands of union and intersection.

$$\begin{aligned} \mathbf {tempo}_{1} S \wedge \mathbf {tempo}_{1} T\implies&\nonumber \\ \left( S \rightarrow T \right) \cap \left( T \rightarrow S \right) = \left\{ \right\}&\text {inter-equiv-false} \end{aligned}$$
(12a)
$$\begin{aligned} \mathbf {tempo}_{1-4} S \wedge \mathbf {tempo}_{1-4} T \wedge S {\triangleleft }{\triangleright }T\implies&\nonumber \\ \left( S \rightarrow T \right) \cup \left( T \rightarrow S \right) = S \cap T&\text {union-equiv-inter} \end{aligned}$$
(12b)

As the XBefore is not symmetric, the intersection of symmetrical sets is empty. The union of the symmetric is a partition of the intersection of the operands.

There are other laws shown in [8]. We are still working on a syntactical reduction for tautology and contradiction. Such an analysis for Boolean algebra uses binary trees for formula reduction. Our initial studies show that the ATF relies on a ternary tree. Besides such a syntactical analysis, we only need those laws shown in this section.

3 The Activation Logic

The Activation Logic (AL) proposed in this work emerges from the need to analyse the behaviour of a system when a subset of the faults is active during the same time period, and to provide completeness analysis of system behaviour. There are at least two strategies to use AL to obtain structure expressions of SFT, TFT, or DFT: (i) model systems directly in AL, and (ii) obtaining operational mode expressions extracted from failure traces, as shown in the work reported in [8]. In approaches as those reported in [16, 27], behavioural completeness is left for the analyst. Using tautology and the indication of undefined nominal values, we ensure that no situation is left forgotten.

The AL associates: (i) an operational mode, and (ii) the expression of fault events that activates the operational mode or error event. The expressions of fault events can be written in any algebra that provides tautology and contradiction properties. Thus, AL is parametrized by: (i) an algebra that provides at least tautology and contradiction, and (ii) operational modes. Figure 3 depicts an overview of AL.

Fig. 3.
figure 3

Activation Logic (AL) overview

Full size image

We summarise the properties of the AL as follows:

  1. 1.

    No expression predicate is a contradiction: there are no false predicates in activation expressions;

  2. 2.

    The predicates in the terms of an expression consider all possible situations: expression tautology;

  3. 3.

    There are no two terms with exactly the same operational mode: all expression terms are related to a unique operational mode.

These properties form the healthiness conditions [14] of an expression in the AL.

We show the general form of the AL to model faults in Sect. 3.1, the healthiness conditions to normalize expressions in Sect. 3.2, how to identify non-determinism in an expression in Sect. 3.3, and the predicates notation to analyse systems and model fault propagation in Sect. 3.4.

3.1 The Activation Logic Grammar

Each term in an expression is a pair of a predicate and an operational mode. The predicate is written in either Boolean algebra, ATF, or any algebra that provides these properties: tautology and contradiction. We assume that the set of possible faults on a system is finite and that each variable declared in a predicate represents a fault event.

The operational mode has two generic values: (i) Nominal, and (ii) Failure. Nominal values either determine value, or an undefined value (in this case, the constant value “\(undefined\)” is assumed). Failure values denote an erroneous behaviour, which can be a total failure (for example, signal omission) or a failure that causes degradation (for example, a signal below or above its nominal range). The choice of the operational modes depends on the system being analysed and its definition is generic and is left for the analyst. For the AL, it is sufficient to specify that it is an erroneous behaviour.

The grammar is parametrized by the syntax of an algebra (Algebra) and a set of operational modes (OperModes). The initial rules of the grammar are defined as follows:

figure a

The denotational semantics of the expressions in AL is a set of pairs. The predicate in each term of an expression depends on the semantics of the inner algebra. Thus the predicate evaluates to either true (\(\top \)) or false (\(\bot \)) depending on the valuation in the algebra. In what follows we show a sketch of the denotational semantics of AL.

$$\begin{aligned} \mathtt {\left( P_1, O_1\right) }&\mapsto \{\left( P_1, O_1\right) \}\\ \mathtt {\left( P_1, O_1\right) | \left( P_2, O_2\right) }&\mapsto \{\left( P_1, O_1\right) , \left( P_2, O_2\right) \}\\ \mathtt {Nominal~100}&\mapsto \mathop {\mathrm {Nominal}} 100\\ \mathtt {Nominal~undefined}&\mapsto \mathop {\mathrm {Nominal}} undefined\\ \mathtt {Failure~Omission}&\mapsto \mathop {\mathrm {Failure}} Omission \end{aligned}$$

In an expression, if the ith predicate evaluates to true (\(\top \)), we say that the ith operational mode is activated. To simplify the presentation of the expressions and to ease the understanding, we use the denotational semantics in the remainder of this article (the right-hand side of the sketch above).

In this section, to illustrate the properties and possible analyses, we use an example of a system with faults A and B and the following outputs:  

\(O_1\)::

when A is active;

\(O_2\)::

when B is active;

\(O_3\)::

when A is active, but B is not;

\(O_4\)::

when A or B are active.

 

The expression for this example in AL is:

$$\begin{aligned} S = \left\{ \left( A, O_1\right) , \left( B, O_2\right) , \left( A \wedge \lnot B, O_3\right) , \left( A \vee B, O_4\right) \right\} \end{aligned}$$
(13)

In this example we see that one of the healthiness conditions is not satisfied: when for instance, A and B are both inactive (\(\lnot \left( A \wedge B\right) \)), there is no explicit output defined. In Sect. 4 we show a more detailed case study to illustrate the reasoning about temporal faults. In the next section, we show how to normalise the expression, so that the three healthiness conditions are satisfied.

3.2 Healthiness Conditions

The healthiness conditions are fix points of a language. The property is defined as a function of an expression and returns another expression. For example, if a healthiness condition \( \mathrm {H}\) is satisfied for an expression Exp, thus \( \mathrm {H}\left( Exp\right) = Exp\).

In what follows we show the three healthiness conditions for the AL. All definitions in this section refer to an algebra that has the following properties:

  • contradiction: the expression always evaluates to false;

  • tautology: the expression always evaluates to true.

\(\mathbf H _\mathbf {1}\) : No predicate is a contradiction. This property is very simple and it is used to eliminate any term that has a predicate that always evaluates to false.

Definition 1

Let exp be an expression in the AL, then:

$$\begin{aligned} \mathrm {H}_1 \left( exp\right) = \left\{ \left( P,O\right) | \left( P,O\right) \in exp \bullet \lnot \mathrm {contradiction}\left( P\right) \right\} \end{aligned}$$
(14)

where the operator \(\in \) indicates that a term is present in the expression.

Applying the first healthiness condition to our example results in:

$$\begin{aligned} \mathrm {H}_1 \left( S\right) = S \end{aligned}$$

Thus, we conclude that S is \( \mathrm {H}_1 \text {-healthy}\).

\(\mathbf H _\mathbf {2}\) : All possibilities are covered. This property is used to make explicit that there are uncovered operational modes. In this case, there is a combination of variables in the inner algebra that was not declared in the expression. Very often the focus when modelling faults is the erroneous behaviour, so we assume that such an uncovered operational mode is nominal, but has an undefined value.

Definition 2

Let exp be an expression in the AL, and \(\tau \) is:

$$ \tau = \lnot \left( \bigvee _{\left( P,O\right) \in exp} P\right) $$

then:

$$\begin{aligned} \mathrm {H}_2 \left( exp\right) = {\left\{ \begin{array}{ll} exp, &{} \textit{if } \mathrm {contradiction}\left( \tau \right) \\ exp \cup \left\{ \left( \tau ,\mathop {\mathrm {Nominal}} undefined\right) \right\} , &{} \textit{otherwise} \end{array}\right. } \end{aligned}$$
(15)

This property states that if the expression is already complete, so all possibilities are already covered, thus the expression is healthy.

Applying the second healthiness condition to our example results in the following expression after simplification:

$$\begin{aligned} \mathrm {H}_2 \left( S\right) = S \cup \left\{ \left( \lnot A \wedge \lnot B, \mathop {\mathrm {Nominal}} undefined\right) \right\} \end{aligned}$$

Thus, we conclude that S is not \( \mathrm {H}_2 \text {-healthy}\).

\(\mathbf H _\mathbf {3}\) : There are no two terms with exactly the same operational mode. This property merges terms that contain the same operational mode. It avoids unnecessary formulas and may reduce the expression.

Definition 3

Let exp be an expression in the AL. Then:

$$\begin{aligned} \begin{aligned} \mathrm {H}_3 \left( exp\right) = \left\{ \right.&\left( P_1, O_1\right) | \left( P_1, O_1\right) \in exp \wedge \\&\forall \left( P_2,O_2\right) \in exp \bullet \left( P_1, O_1\right) = \left( P_2, O_2\right) \vee O_1 \ne O_2 \left. \right\} \cup \\&\left\{ \left( P_1 \vee P_2, O_1\right) | \left( P_1, O_1\right) ,\left( P_2, O_2\right) \in exp \wedge O_1 = O_2 \right\} \end{aligned} \end{aligned}$$
(16)

Applying \( \mathrm {H}_3 \) in the example in the beginning of the section, we conclude that S is \( \mathrm {H}_3 \text {-healthy}\). On the other hand, if we consider an \(S'\) system being a copy of S, but making \(O_1 = O_2\), then:

$$ \mathrm {H}_3 \left( S'\right) = \left\{ \left( A \vee B, O_1\right) , \left( A \wedge \lnot B, O_3\right) , \left( A \vee B, O_4\right) \right\} $$

Thus, we conclude that \(S'\) is not \( \mathrm {H}_3 \text {-healthy}\).

Healthy Expression. To obtain a healthy expression, we apply all three healthiness conditions. The order of application of each healthiness condition does not change the resulting expression. The healthiness function is written as composition of functions as follows:

$$\begin{aligned} \mathrm {H}= \mathrm {H}_1 \circ \mathrm {H}_2 \circ \mathrm {H}_3 \end{aligned}$$
(17)

After applying the three healthiness conditions to S, the resulting expression is:

$$ \begin{aligned} \mathrm {H}\left( S\right) = \left\{ \right.&\left( A, O_1\right) , \left( B, O_2\right) ,\\&\left( A \wedge \lnot B, O_3\right) , \left( A \vee B, O_4\right) ,\\&\left( \lnot A \wedge \lnot B, \mathop {\mathrm {Nominal}} undefined\right) \left. \right\} \end{aligned} $$

The healthiness conditions are useful to faults modelling, aiding the faults analyst to check contradictions and completeness. Also, obtaining safe predicates is only possible in healthy expressions. In the next section, we show how to verify non-determinism in AL expressions.

3.3 Non-determinism

The non-determinism is usually an undesirable property. It causes an unexpected behaviour, so the analysis shall consider the activation of fault even if the fault might or not be active.

To identify a non-determinism, we can check for the negation of a contradiction in a pair of predicates in the inner algebra.

Definition 4

(Non-determinism). Let exp be an expression in AL.

$$\begin{aligned} \begin{aligned} \mathrm {nondeterministic}\left( exp\right) =&\exists \left( P_1,O_1\right) ,\left( P_2, O_2\right) \in exp~\bullet \\&\lnot \mathrm {contradiction}\left( P_1 \wedge P_2\right) \end{aligned} \end{aligned}$$
(18)

If there is at least one combination that evaluates \(P_1 \wedge P_2\) to true (it is not a contradiction), then exp is non-deterministic. Our example is clearly non-deterministic as at least \(A \wedge \left( A \vee B\right) \) is not a contradiction.

To analyse components and systems, and to model faults propagation, a predicates notation is shown in the next section. The predicates notation offers more two ways to check non-determinism.

3.4 Predicates Notation

The AL needs a special notation to enable the analysis of: (i) a particular faults expression, or (ii) a propagation in components. Such a special notation extracts predicates in the inner algebra given an output of interest.

Definition 5

(Predicate). Let exp be an expression in AL, and \(O_x\) an operational mode. A predicate over exp that matches \(O_x\) is then:

$$\begin{aligned} \left\langle \mathrm {out}\left( exp\right) = O_x \right\rangle \iff \left. \exists \left( P, O\right) \in \mathrm {H}\left( exp\right) \ \mid \ O = O_x \bullet P\right. \end{aligned}$$
(19)

The predicate notation function returns a predicate in the inner algebra. For the example in the beginning of this section, the predicate for \(O_2\) is obtained as follows:

$$ \left\langle \mathrm {out}\left( S\right) = O_2 \right\rangle = B $$

To allow fault propagation of components we need another special notation that expands the modes of an expression with a predicate in the inner algebra.

Definition 6

(Modes). Let exp be an expression in AL, and P a predicate in the inner algebra, then:

$$\begin{aligned} \mathrm {modes}\left( exp,P\right) = \left\{ \left( P_i \wedge P, O_i\right) \ \mid \ (P_i, O_i) \in \mathrm {H}\left( exp\right) \right\} \end{aligned}$$
(20)

Finally, to check the possible outputs, we need a function to obtain a set of outputs given an expression.

Definition 7

(Activation). Let exp be an expression in AL, and \(P_x\) a predicate in the inner algebra, then:

$$\begin{aligned} \mathrm {activation}\left( exp, P_x\right) = \left\{ O | (P, O) \in \mathrm {H}\left( exp\right) \wedge \mathrm {tautology}\left( P_x \implies P\right) \right\} \end{aligned}$$
(21)

The non-determinism can also be checked using the predicates notation and the activation property:

$$\begin{aligned} \mathrm {activation}\left( S, A \wedge \lnot B\right) =&\left\{ O_1, O_3\right\} \end{aligned}$$
(22a)
$$\begin{aligned} \left\langle \mathrm {out}\left( S\right) = O_1 \right\rangle \wedge \left\langle \mathrm {out}\left( S\right) = O_3 \right\rangle =&A \wedge \lnot B \end{aligned}$$
(22b)

Equation (22a) shows that both \(O_1\) and \(O_3\) can be observed if \(A \wedge \lnot B\) is true. Equation (22b) states that if the possible operational modes of healthy S are \(O_1\) and \(O_3\), then the predicate is \(A \wedge \lnot B\). In the next section, we show a practical case study using these properties and notations.

4 Case Study

EMBRAER provided us with the Simulink model of an Actuator Control System (depicted in Fig. 4). The failure logic of this system (that is, for each of its constituent components) was also provided by EMBRAER (we show some of them in Table 2). In what follows we illustrate our strategy using the Monitor component.

Fig. 4.
figure 4

Block diagram of the ACS provided by EMBRAER (nominal model)

Full size image
Table 2. Annotations table of the ACS provided by EMBRAER
Full size table

A monitor component is a system commonly used for fault tolerance [15, 21]. Initially, the monitor connects the main input (power source on input port 1) with its output. It observes the value of this input port and compares it to a threshold. If the value is below the threshold, the monitor disconnects the output from the main input and connects to the secondary input. We present the Simulink model for this monitor in Fig. 5.

Fig. 5.
figure 5

Internal diagram of the monitor component (Fig. 4(A)).

Full size image

Now we show two contributions: (i) using only Boolean operators, thus ignoring ordering, we can obtain the same results obtained in [7], and (ii) using the order-related operator reported in [8] obtaining an expression in ATF with the same results as shown in [8]. To simplify formulas writing, we associate the fault events as:

$$\begin{aligned} B_1&= \text {LowPower-In1}\\ B_2&= \text {LowPower-In2}\\ F&= \text {SwitchFailure} \end{aligned}$$

The power source has only two possible operational modes: (i) the power source works as expected, providing a nominal value of 12V, and (ii) is has an internal failure \(B_i\), and its operational mode is “low power”. In AL it is modelled as:

$$\begin{aligned} PowerSource_i = \left\{ \left( B_i, LP\right) , \left( \lnot B_i, \mathop {\mathrm {Nominal}} 12V\right) \right\} \end{aligned}$$
(23)

where LP is the LowPower failure. The expression \(PowerSource_i\) is healthy.

The monitor is a bit different because its behaviour depends not only on internal faults, but also on its inputs. We will now use the predicates notation defined in Sect. 3.4 to express fault propagation. As the monitor has two inputs and its behaviour is described in Fig. 5, then it is a function of the expressions of both inputs:

$$\begin{aligned} \begin{aligned} Monitor_{bool}&\left( in_1, in_2\right) = \\&\mathrm {modes}\left( in_1,\left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge \lnot F\right) \cup \\&\mathrm {modes}\left( in_2,\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge \lnot F\right) \cup \\&\mathrm {modes}\left( in_2,\left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge F\right) \cup \\&\mathrm {modes}\left( in_1,\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge F\right) \end{aligned} \end{aligned}$$
(24)

where X is an unbound variable and assumes any value. The expression states the following:

  • The monitor output is the same as \(in_1\) if the output of \(in_1\) is nominal and there is no internal failure in the monitor:

    $$ \mathrm {modes}\left( in_1,\left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge \lnot F\right) $$

  • The monitor output is the same as \(in_2\) if the output of \(in_1\) is not nominal and there is no internal failure in the monitor:

    $$ \mathrm {modes}\left( in_2,\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge \lnot F\right) $$

  • The monitor output is the converse of the previous two conditions if the internal failure F is active:

    $$ \begin{aligned} \mathrm {modes}\left( in_2,\left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge F\right)&\cup \\ \mathrm {modes}\left( in_1,\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge F\right)&\end{aligned} $$

The operational modes (observed behaviour) of the monitor depend on: (i) its internal fault, and (ii) propagated errors from its inputs. Composing the monitor with the two power sources, we obtain the AL expression of a power supply subsystem \(System_{\mathrm {bool}}\):

$$\begin{aligned} =&Monitor_{bool} \left( PowerSource_1, PowerSource_2\right) \\ =&\mathrm {modes}\left( in_1,\lnot B_1 \wedge \lnot F\right) \cup \mathrm {modes}\left( in_2,\lnot \lnot B_1 \wedge \lnot F\right) \cup \\&\mathrm {modes}\left( in_2,\lnot B_1 \wedge F\right) \cup \mathrm {modes}\left( in_1,\lnot \lnot B_1 \wedge F\right)&\text {by Eq. (19)}\\ =&\mathrm {modes}\left( in_1,\lnot B_1 \wedge \lnot F\right) \cup \mathrm {modes}\left( in_2, B_1 \wedge \lnot F\right) \cup \\&\mathrm {modes}\left( in_2,\lnot B_1 \wedge F\right) \cup \mathrm {modes}\left( in_1,B_1 \wedge F\right)&\text {by simplification}\\ =&\left\{ \left( P_i \wedge \lnot B_1 \wedge \lnot F, O_i\right) | \left( P_i, O_i\right) \in in_1 \right\} \cup \\&\left\{ \left( P_i \wedge B_1 \wedge \lnot F, O_i\right) | \left( P_i, O_i\right) \in in_2 \right\} \cup \\&\left\{ \left( P_i \wedge \lnot B_1 \wedge F, O_i\right) | \left( P_i, O_i\right) \in in_2 \right\} \cup \\&\left\{ \left( P_i \wedge B_1 \wedge F, O_i\right) | \left( P_i, O_i\right) \in in_1 \right\}&\text {by Eq. (20)}\\ =&\left\{ \left( B_1 \wedge \lnot B_1 \wedge \lnot F, LP\right) , \right. \\&\left( \lnot B_1 \wedge \lnot B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \\&\left( B_2 \wedge B_1 \wedge \lnot F, LP\right) ,\\&\left( \lnot B_2 \wedge B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \\&\left( B_2 \wedge \lnot B_1 \wedge F, LP\right) , \\&\left( \lnot B_2 \wedge \lnot B_1 \wedge F, \mathop {\mathrm {Nominal}} 12V\right) ,\\&\left( B_1 \wedge B_1 \wedge F, LP\right) , \\&\left. \left( \lnot B_1 \wedge B_1 \wedge F, \mathop {\mathrm {Nominal}} 12V\right) \right\}&\text {replacing vars}\\ \end{aligned}$$

Simplifying and applying \( \mathrm {H}_1 \), we obtain:

$$ \begin{aligned} \mathrm {H}_1 \left( System_{\mathrm {bool}}\right) =&\\&\left\{ \left( \lnot B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \left( B_2 \wedge B_1 \wedge \lnot F, LP\right) ,\right. \\&\left( \lnot B_2 \wedge B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \left( B_2 \wedge \lnot B_1 \wedge F, LP\right) , \\&\left. \left( \lnot B_2 \wedge \lnot B_1 \wedge F, \mathop {\mathrm {Nominal}} 12V\right) , \left( B_1 \wedge F, LP\right) \right\} \end{aligned} $$

Applying, \( \mathrm {H}_3 \), we simplify to:

$$ \begin{aligned} \mathrm {H}_3 \circ \mathrm {H}_1&\left( System_{\mathrm {bool}}\right) \\ =&\left\{ \left( \begin{aligned} \left( \lnot B_1 \wedge \lnot F\right) \vee \\ \left( B_1 \wedge \lnot B_2 \wedge \lnot F \right) \vee \\ \left( \lnot B_1 \wedge \lnot B_2 \wedge F \right) \end{aligned}, \mathop {\mathrm {Nominal}} 12V \right) , \right. \\&\left. \left( \begin{aligned} \left( B_1 \wedge B_2 \wedge \lnot F\right) \vee \\ \left( \lnot B_1 \wedge B_2 \wedge F\right) \vee \\ \left( B_1 \wedge F\right) \end{aligned}, LP \right) \right\} \\ =&\left\{ \left( \left( \lnot B_1 \wedge \lnot B_2\right) \vee \lnot F \wedge \left( \lnot B_1 \vee \lnot B_2\right) , \mathop {\mathrm {Nominal}} 12V\right) , \right. \\&\left. \left( F \wedge \left( B_1 \vee B_2\right) \vee \left( B_1 \wedge B_2\right) , LP\right) \right\} \end{aligned} $$

The monitor expression is \( \mathrm {H}_2 \text {-healthy}\) (the predicates are complete), thus:

$$ \mathrm {H}_2 \circ \mathrm {H}_3 \circ \mathrm {H}_1 \left( System_{\mathrm {bool}}\right) = \mathrm {H}_3 \circ \mathrm {H}_1 \left( System_{\mathrm {bool}}\right) $$

The resulting expression for the monitor after applying all healthiness conditions is:

$$\begin{aligned} \begin{aligned} \mathrm {H}\left( System_{\mathrm {bool}}\right) =&\left\{ \left( \left( \lnot B_1 \wedge \lnot B_2\right) \vee \lnot F \wedge \left( \lnot B_1 \vee \lnot B_2\right) , \mathop {\mathrm {Nominal}} 12V\right) ,\right. \\&\left. \left( F \wedge \left( B_1 \vee B_2\right) \vee \left( B_1 \wedge B_2\right) , LP\right) \right\} \end{aligned} \end{aligned}$$
(25)

The operational modes of \(System_{\mathrm {bool}}\) is either \(\mathop {\mathrm {Nominal}} 12V\) or LP (low power).

Finally, we obtain the low power structure expression (see Table 2) using the predicates notation:

$$ \left\langle \mathrm {out}\left( System_{\mathrm {bool}}\right) = LP \right\rangle \iff F \wedge \left( B_1 \vee B_2\right) \vee \left( B_1 \wedge B_2\right) $$

The monitor expression also indicates that if the switch is operational (\(\lnot F\)) and at least one PowerSource is operational (\(\lnot B_1 \vee \lnot B_2\)), the monitor output is nominal. But if at least one PowerSource is faulty (\(B_1 \vee B_2\)) and the monitor has an internal failure (F) the system is not operational. These two sentences written in AL using predicates notation are:

$$\begin{aligned}&\mathrm {activation}\left( System_{\mathrm {bool}}, \lnot F \wedge \left( \lnot B_1 \vee \lnot B_2\right) \right) \nonumber \\&\qquad \quad \,\, = \left\{ O | \left( P, O\right) \in \mathrm {H}\left( System_{\mathrm {bool}}\right) \wedge \right. \nonumber \\&\qquad \qquad \,\, \left. \mathrm {tautology}\left( \lnot F \wedge \left( \lnot B_1 \vee \lnot B_2\right) \implies P\right) \right\} \qquad \text {[by Eq. (21)]}\nonumber \\&\qquad \quad \,\, = \left\{ \mathop {\mathrm {Nominal}} 12V\right\} \qquad \qquad \qquad \qquad \qquad \,\,\, \text {[by simplification]}\end{aligned}$$
(26a)
$$\begin{aligned}&\mathrm {activation}\left( System_{\mathrm {bool}}, F \wedge \left( B_1 \vee B_2\right) \right) \nonumber \\&\qquad \quad \,\, = \left\{ O | \left( P, O\right) \in \mathrm {H}\left( System_{\mathrm {bool}}\right) \wedge \right. \nonumber \\&\qquad \qquad \,\, \left. \mathrm {tautology}\left( F \wedge \left( B_1 \vee B_2\right) \implies P\right) \right\} \qquad \text {[by Eq. (21)]}\nonumber \\&\qquad \quad \,\, = \left\{ LP\right\} \qquad \qquad \qquad \qquad \qquad \qquad \,\,\,\, \text {[by simplification]} \end{aligned}$$
(26b)

Now, let’s consider the same system but with a subtle modification. As shown in [8], the order of the occurrence of faults may be relevant, and the qualitative and quantitative analyses results may be different than those results without considering the order of the occurrence of faults. Observing Fig. 5, we see that if F activates before a failure in the first input of the monitor, then it would display a nominal behaviour, because the internal failure F anticipates switching to the second input. On the other hand, if the first input fails before F, then the monitor would switch to the second input, then switch back, due to the internal failure. We obtain the following expression for the monitor, now using the ATF:

$$\begin{aligned} \begin{aligned} Monitor_{ATF}&\left( in_1, in_2\right) = \\&\mathrm {modes}\left( in_1,\left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge \lnot F\right) \cup \\&\mathrm {modes}\left( in_2,\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge \lnot F\right) \cup \\&\mathrm {modes}\left( in_2,\left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \wedge F\right) \cup \\&\mathrm {modes}\left( in_1,\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \rightarrow F \right) \cup \\&\mathrm {modes}\left( in_2,F \rightarrow \lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} X \right\rangle \right) \end{aligned} \end{aligned}$$
(27)

where X is an unbound variable and assumes any value.

The difference to \(System_{\mathrm {bool}}\) (Eq. (24)) is only the finer analysis of the cases of erroneous behaviour of the first input and an internal failure. Note that the finer analysis splits the predicate

$$\begin{aligned}&\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} 12V \right\rangle \wedge F&\text {(activates } in_1\text {)} \end{aligned}$$

into:

$$\begin{aligned}&\lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} 12V \right\rangle \rightarrow F&\text {(activates } in_1\text {)}\\ \end{aligned}$$

and

$$\begin{aligned}&F \rightarrow \lnot \left\langle \mathrm {out}\left( in_1\right) = \mathop {\mathrm {Nominal}} 12V \right\rangle&\text {(activates } in_2\text {)} \end{aligned}$$

We can assure that such a split is complete because the predicate notation evaluates to \(B_1\). Thus the operands satisfy all temporal properties (Eqs. (8a) to (8d)) and events independence (Eq. (10)), thus the law shown in Eq. (12b) is valid. For case (i), the expected behaviour is the same as \(in_1\) because the system switches to \(in_2\), but then an internal failure occurs, and it switches back to \(in_1\). For case (ii), it switches to \(in_2\) due to an internal failure, then the first input fails, so the behaviour is similar to the nominal behaviour (see the second modes in Eq. (27)).

Following the similar expansions of Eq. (24), we obtain:

$$\begin{aligned} System_{ATF} =&Monitor_{ATF} \left( PowerSource_1, PowerSource_2\right) \\ =&\left\{ \left( B_1 \wedge \lnot B_1 \wedge \lnot F, LP\right) , \right. \\&\left( \lnot B_1 \wedge \lnot B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \\&\left( B_2 \wedge B_1 \wedge \lnot F, LP\right) ,\\&\left( \lnot B_2 \wedge B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \\&\left( B_2 \wedge \lnot B_1 \wedge F, LP\right) , \\&\left( \lnot B_2 \wedge \lnot B_1 \wedge F, \mathop {\mathrm {Nominal}} 12V\right) ,\\&\left( B_1 \wedge B_1 \rightarrow F , LP\right) , \\&\left. \left( \lnot B_1 \wedge B_1 \rightarrow F , \mathop {\mathrm {Nominal}} 12V\right) \right\} , \\&\left( B_2 \wedge F \rightarrow B_1 , LP\right) , \\&\left. \left( \lnot B_2 \wedge F \rightarrow B_1 , \mathop {\mathrm {Nominal}} 12V\right) \right\} \\ \end{aligned}$$

Simplifying and applying \( \mathrm {H}_1 \) to remove contradictions, we obtain:

$$ \begin{aligned} \mathrm {H}_1 \left( System_{ATF}\right) =&\\&\left\{ \left( \lnot B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \left( B_2 \wedge B_1 \wedge \lnot F, LP\right) ,\right. \\&\left( \lnot B_2 \wedge B_1 \wedge \lnot F, \mathop {\mathrm {Nominal}} 12V\right) , \left( B_2 \wedge \lnot B_1 \wedge F, LP\right) , \\&\left( \lnot B_2 \wedge \lnot B_1 \wedge F, \mathop {\mathrm {Nominal}} 12V\right) , \left( B_1 \rightarrow F , LP\right) , \\&\left. \left( B_2 \wedge F \rightarrow B_1 , LP\right) , \left( \lnot B_2 \wedge F \rightarrow B_1 , \mathop {\mathrm {Nominal}} 12V\right) \right\} \end{aligned} $$

Applying \( \mathrm {H}_3 \) to remove redundant terms with identical operational modes and using the rules shown in Sect. 2.3, we simplify to:

$$ \begin{aligned} \mathrm {H}_3 \circ \mathrm {H}_1&\left( System_{\mathrm {ATF}}\right) \\ =&\left\{ \left( \begin{aligned} \left( \lnot B_1 \wedge \lnot F\right) \vee \\ \left( B_1 \wedge \lnot B_2 \wedge \lnot F \right) \vee \\ \left( \lnot B_1 \wedge \lnot B_2 \wedge F \right) \vee \\ \left( \lnot B_2 \wedge F \rightarrow B_1 \right) \end{aligned}, \mathop {\mathrm {Nominal}} 12V \right) , \right. \\&\left. \left( \begin{aligned} \left( B_1 \wedge B_2 \wedge \lnot F\right) \vee \\ \left( \lnot B_1 \wedge B_2 \wedge F\right) \vee \\ \left( B_1 \rightarrow F \right) \vee \\ \left( B_2 \wedge F \rightarrow B_1 \right) \end{aligned}, LP \right) \right\} \\ =&\left\{ \left( \left( \lnot B_1 \wedge \lnot B_2\right) \vee \lnot F \wedge \left( \lnot B_1 \vee \lnot B_2\right) \vee \right. \right. \\&\left. \lnot B_2 \wedge F \rightarrow B_1 , \mathop {\mathrm {Nominal}} 12V\right) , \\&\left. \left( \left( B_1 \wedge B_2\right) \vee \left( \lnot B_1 \wedge B_2 \wedge F\right) \vee \left( \lnot B_2 \wedge B_1 \rightarrow F \right) , LP\right) \right\} \end{aligned} $$

The monitor expression is \( \mathrm {H}_2 \text {-healthy}\). Simplifying Boolean operators as usual, the XBefore expression:

$$\begin{aligned} \lnot B_2 \wedge F \rightarrow B_1&\vee \lnot B_2 \wedge B_1 \rightarrow F \end{aligned}$$

simplifies to

$$\begin{aligned} \lnot B_2\wedge&F \wedge B_1&\text {by Eq. (12b)} \end{aligned}$$

Thus:

$$ \mathrm {H}_2 \circ \mathrm {H}_3 \circ \mathrm {H}_1 \left( System_{\mathrm {ATF}}\right) = \mathrm {H}_3 \circ \mathrm {H}_1 \left( System_{\mathrm {ATF}}\right) $$

The resulting expression for the monitor after applying all healthiness conditions is:

$$\begin{aligned} \begin{aligned} \mathrm {H}\left( System_{ATF}\right) =&\left\{ \left( \left( \lnot B_1 \wedge \lnot B_2\right) \vee \lnot F \wedge \left( \lnot B_1 \vee \lnot B_2\right) \vee \right. \right. \\&\left. \lnot B_2 \wedge F \rightarrow B_1 , \mathop {\mathrm {Nominal}} 12V\right) , \\&\left( \left( B_1 \wedge B_2\right) \vee \left( \lnot B_1 \wedge B_2 \wedge F\right) \vee \right. \\&\left. \left. \left( \lnot B_2 \wedge B_1 \rightarrow F \right) , LP\right) \right\} \end{aligned} \end{aligned}$$
(28)

Finally, we obtain the low power structure expression of the monitor using the predicates notation:

$$ \left\langle \mathrm {out}\left( System_{\mathrm {ATF}}\right) = LP \right\rangle \iff \left( B_1 \wedge B_2\right) \vee \left( \lnot B_1 \wedge B_2 \wedge F\right) \vee \left( \lnot B_2 \wedge B_1 \rightarrow F \right) $$

Thus, \(System_{\mathrm {ATF}}\) fails with LP if:

  • Both power sources fail;

  • The monitor fails to detect the nominal state of the first power source and the second power source is in a failure state;

  • The monitor fails to detect the failure state of the first power source (the monitor fails after the failure of the first power source).

Note that if the monitor fails before the failure of the first power source, it fails to detect the operational mode of the first power source and switches to the second power source, which is in a nominal state (see expression \(\lnot B_2 \wedge F \rightarrow B_1 \) in Eq. (28)).

5 Conclusion

In this work we proposed a parametrized logic that enables the analysis of systems depending on the expressiveness of a given algebra and a given set of operational modes. If ATF is used as a parameter, then the order of occurrence of faults can be considered. Although the logic is not as detailed as AADL, the predicates notation in conjunction with the ATF provides a richer assertion framework. Also, it is possible to verify non-determinism on the model, by: (i) verifying its existence with the \(\mathrm {nondeterministic}\) function, (ii) providing an expression and obtaining the possible operational modes with the \(\mathrm {activation}\) function, or (iii) using the predicates notation to obtain a predicate that enables two or more operational modes.

The AADL is extensible. The work reported in [2] shows an extension to perform dependability analysis through state machines and expressions on fault events and operational modes. Although such an extension captures system behaviour, operational mode activation conditions are expressed in state transitions in combination with an extension of Boolean expressions (not related to order). Our work relates operational modes and fault occurrences order explicitly.

As presented in [8], TFTs and DFTs structure expressions can be written as formulas in ATF. As the root events of TFTs and DFTs represent operational modes of a system, the ATF can be used to associate root events with operational modes, thus allowing the combination of two or more fault trees.

Although the properties of AL require that the inner algebra provides tautology and contradiction, and we used ATF in the case study, we did not show tautology and contradiction for ATF. Instead, we used a law to reduce the ATF expression to a Boolean expression. The methodology to check tautology and contradiction in ATF is a future work.

The original expression shown in the case study was already \( \mathrm {H}_2 \text {-healthy}\). The second healthiness condition about completeness uses the concept of undefined value to make any expression \( \mathrm {H}_2 \text {-healthy}\). Algebraically it is fine, but in practice, the property should be met originally, thus the initial expression is already \( \mathrm {H}_2 \text {-healthy}\). This property should be used as an alert to the analyst if it not met originally.