Michael Rathmair
email: rathmair@ict.tuwien.ac.at

Ralph Hoch
email: hoch@ict.tuwien.ac.at

Hermann Kaindl
email: kaindl@ict.tuwien.ac.at

Roman Popp
email: popp@ict.tuwien.ac.at

Consistently Formalizing a Business Process and its Properties for Verification: A Case Study

Formal verification of business process models can be done through model checking (also known as property checking), where a model checker tool may automatically find violations of properties in a process model. This approach obviously has formal representations as a prerequisite. However, a key challenge for applying this approach in practice is to consistently formalize the process and its properties, which clearly cannot be done automatically. We studied this challenge in a case study of formally verifying an informally given business process against a guideline written like a legal text. Major lessons learned from this case study are that formalizing is key to success and that in its course a semi-formal representation of properties is useful. In the course of such a step-wise and incremental formalization, problems with the given process model have been found already, apart from those found with a model checker tool that used the formal property specification. In total, our approach revealed five problems not found by the official review. In summary, this paper investigates in a case study consistently formalizing a business process and its properties for verification through model checking.

Introduction

Hardware and software should be free of errors, and the same applies to business processes. Usual quality assurance techniques for hardware and software in practice are reviews and tests. These have the purpose of finding errors but they can, in general, not show that there are no errors. Research both related to hardware and software investigates model checking for formal verification, which can, in principle, show that there are no errors with regard to certain properties. This requires both a formally specified behavioral model and formulas specifying properties to verify them against. Neither of them are usually available in practice, unfortunately.

Roughly speaking, a formal representation is one that allows (automatic) reasoning purely based on its form, which has defined semantics. In particular, illustrative diagrams or natural language are not formal representations. That is why formalization is necessary when something is given informally, e.g., in such diagrams or in natural language. Business process models typically are behavioral models, but usually not (really) formally defined in practice. So, their formalization is important but even more so the consistent formalization of properties to check them against. These properties are sometimes hard to get in practice and at best, informally described. The properties typically refer to the behavioral models, but this means some coupling. And if the person who formalizes properties has the behavioral model available, then there will be some influence on the properties. This is reminiscent of someone writing test cases for his own software. So, we argue for more or less independent formalization of a behavioral model and of the properties to check it against. Unfortunately, this may lead to inconsistent formalizations that do not fit together for the purpose of model checking. Therefore, consistent formalization of behavioral model and properties is a challenge, which we address in this paper.

We investigated this challenge in the context of a case study where it became apparent. The task was verifying a high-level business process of our university against a corresponding guideline, both of which were given informally. More precisely, this is a real process enacted on a regular basis (for searching and appointing a full professor). For the case study, a process diagram in informal notation was used, as given in the course of preparations for an official Quality Audit. The guideline is an official document of our university, derived from the Austrian law for universities. In particular, its writing style is like that of this legal text, i.e., a special kind of text in natural language.

So, there was informal input, but formal representations of both process and properties are needed for formal verification using model checking. Of course, there is neither an automated transformation nor a defined sequence of steps available for such a task of formalization, and we did not attempt to define something like that, either. Still, we suggest, based on the case study, to use a semi-formal representation in the course of the formalization. Its usefulness is a major lesson learned, generalized from the case at hand.

The remainder of this paper is organized in the following manner. First, we present some background material on model checking in order to make this paper self-contained. Then we discuss related work. The core part presents a case study of model checking an informally given high-level process against a guideline based on legal text, where consistent formalization was particularly studied, and concludes with lessons learned from it. After that, we discuss threats to validity. Finally, we derive general conclusions on consistently formalizing properties used for model checking business processes.

Background on Model Checking

Model checking (or property checking) is a formal verification technique based on models of system behavior and properties, specified unambiguously in formal languages (see, e.g., [START_REF] Baier | Principles of Model Checking[END_REF]). The behavioral model of the system under verification is often specified using a Finite State Machine (FSM), in our case using synchronized FSMs. Their expressiveness is sufficient for our case, but Petri nets, e.g., could be used as well, if needed (depending on the tool used). The properties to be checked on the behavioral model are formulated in a specific property specification language, usually based on a temporal language . Several tools (such as SPIN [START_REF]SPIN: SPIN Verifying Multi-threaded Software with Spin[END_REF] or NuSMV [START_REF] Nusmv | NuSMV: a new symbolic model checker[END_REF]) exist for performing these checks by systematically exploring the state-space of the system. When such a tool finds a property violation, it reports it in the form of a counterexample.

In this work, we make use of Linear Temporal Logic, or Linear-time Temporal Logic, (LTL) and Computational Tree Logic (CTL) for property specification. More precisely, we use PLTL (LTL with past). Since a rough understanding of some of their operators is needed for understanding our formalization approach, let us briefly sketch these here. PLTL provides expressions of relations between states (path formulas) using operators referring to behavior over time. In PLTL, the set of traditional propositional logic operators is extended by time operators such as:

-G (Globally): an expression p is true at time t if p is true at all times t ≥ t.

-F (Future): an expression p is true at time t if p is true at some time t ≥ t.

-O (Once): an expression p is true at time t if p is true at some previous time t ≤ t.

CTL features the specification of branching time properties. While PLTL allows the specification of properties to hold for all computation paths related to a given point in time, CTL provides operators for specifying whether there exists (eventually) a computation path where a specific state property holds. In this work, we use the following CTL operators:

-EF (Eventually in the Future): an expression p is true in the initial state s 0 and there exists a state sequence

s 0 → s 1 → s 2 → • • • → s n such that p is true in s n .
-AG (Always Globally): an expression p is true in the initial state s 0 and in each state of all transitions

s 0 → s 1 → s 2 → • • • → s n .

Related Work

Previous related work made it absolutely clear that some representation with defined semantics is a prerequisite for formal verification, also of business processes. Given such a representation, checking correctness properties inherent in the business process itself is possible. Since we rather focus on formalizing properties given in addition to a business process, we cite only a few references here. Wynn et al. [START_REF] Wynn | Business process verification -finally a reality![END_REF] verify business processes against four defined properties (soundness, weak soundness, irreducible cancellation regions and immutable OR-joins). Sbai et al. [START_REF] Sbai | On the verification of business processes by model checking techniques[END_REF] show how a model checker can be used to identify problems with a specification of a business process to be automated as a workflow, and how a verification of certain correctness properties can be accomplished. Kherbouche et al. [START_REF] Kherbouche | Using model checking to control the structural errors in bpmn models[END_REF] propose an approach for using model checking as a mechanism to detect errors such as deadlocks or lifelocks. Some previous work addressed the question of what to verify a business process model against, to determine possible violations of certain properties given in addition to the process model itself. Fisteus et al. [START_REF] Fisteus | Applying Model Checking to BPEL4WS Business Collaborations[END_REF] propose a framework for integrating BPEL4WS and the SPIN and SMV verification tools. This framework can verify a process specification against properties such as invariants and goals through model checking. Armando et al. [START_REF] Armando | Model checking of security-sensitive business processes[END_REF] show how model checking can be used for automatic analysis of security-sensitive business processes. They propose a system that allows the separate specification of the business process workflow and of corresponding security requirements. In more recent work [START_REF] Armando | Model checking authorization requirements in business processes[END_REF], they show how model checking can be specifically used to check authorization requirements that are implemented in parts of business processes. Barros et al. [10] propose to check business processes against execution rules incorporated in workflows with model checking techniques.

Mrasek et al. [START_REF] Mrasek | User-friendly property specification and process verification -a case study with vehicle-commissioning processes[END_REF] point out that formalizing properties in CTL is a difficult task and strive for making it easier through so-called patterns based on textual fragments in natural language. This approach can work in a given context for entering properties, and it helped in a case study. In general, however, the interpretation of these textual patterns is subtle and error-prone. So, they have to be prepared specifically for a given problem by CTL specialists, anyway. In particular, for our case study with given legal text, such an approach would most likely require a variety of different patterns and still be hard to validate.

The focus of our work as presented in this paper is, however, consistently formalizing the business process and its properties as required for automatic verification through model checking. Still, no previous work in the context of model checking of business process models addressed it to our best knowledge, including model-based business process compliance-checking approaches [START_REF] Becker | Generalizability and applicability of model-based business process compliance-checking approaches -a state-of-the-art analysis and research roadmap[END_REF]. Apart from [START_REF] Mrasek | User-friendly property specification and process verification -a case study with vehicle-commissioning processes[END_REF], which addresses formalizing properties (but not formalizing the process), all the publications on model checking of business processes already assume the availability of formal representations.

A Case Study of Model Checking a High-level Process Against a Guideline

We performed a case study, where we verified a high-level business process of our university against a corresponding guideline, both of which were given informally. More precisely, this is a real process enacted on a regular basis (for searching and appointing a full professor), but its 'as-is' process diagram has been yet under development at this time (in the course of preparations for an official Quality Audit).

We used a version of this diagram that was under official review at about the same time as the case study, but in order to keep pace with the tight schedule of the overall endeavor, we only dealt with the core part of this process where the search committee is active. Figure 1 shows a selected part of this core part to be used below for illustration purposes, in the informal notation officially used. (Note, that the arrow from the task "Invite new reviewers" leads outside of this selected part.) The guideline is an official document of our university, and its text (in German) can be found at http://www.tuwien.ac.at/dle/universitaetskanzlei/ satzung/berufungsverfahren/. This guideline is derived from the Austrian law for universities. In particular, its writing style is like the one of this legal text.

Stakeholders

The stakeholders involved in this case study, directly or indirectly, are the following:

-Central group responsible A dedicated group directly assigned to the rectorate was responsible for creating business models of several high-level processes of our university, and for their review. In order to acquire knowledge on these processes, several dedicated working groups were assembled, whose output was fed into the process models created by the central group responsible for that. -Reviewers of process models

In order to get as much feedback as possible on these models, every employee of our university has been invited to participate in the review (via email).

-Case study team

The people having performed this case study are actually the same as the authors of this paper. Two of them had enacted this very process in key roles in 2013.

-Verification engineer

The first author of this paper was the verification engineer in this team and brought in know-how and experience from applying such techniques in hardware design, more precisely circuit verification, see, e.g., [START_REF] Rathmair | Applied formal methods for hardware Trojan detection[END_REF].

Formalization of Guideline and Process Model

Initially, the verification engineer only worked on formalizing the guideline, as he did not know the process at all. Therefore, he could not formalize the process model yet, and also not completely formalize the properties to check it against, since he did not know the states of the process model. So, he created a semi-formal representation of properties according to the guideline first, where he used PLTL/CTL operators already, but still text fragments from the guideline to indicate, e.g., sequences of tasks. This property representation was subject to an informal manual inspection by the complete case study team. Only after that, the verification engineer was given the part of the process model, which he formalized as an FSM. Once having the FSM available, he formalized the properties based on the previously prepared semi-formal representations. Finally, he applied the model checking tool for checking whether the process model is inconsistent with the given guideline.

For illustrating the creation of a semi-formal representation, let us start with an example excerpt from the guideline. §7(1) of the guideline is given in the second column of Table 1: "The chairperson of the search committee forwards . . . ". First, the verification engineer identified all actors and artefacts mentioned in the partial sentence and treated them as individual objects, e.g., CSC and list (of candidates). After that, he identified actions and mapped them to expressions including temporal operators, e.g., F as specifications of allowed sequences. Since this example contains two different actions with different actors, the full paragraph is actually mapped to two properties. The second of these properties in its semi-formal representation, i.e., "G (list = TRUE → F Dean.state = forward candidate list to rector)", expresses that globally (PLTL operator G), if the list exists, then the Dean must reach a future state (PLTL operator F ), where the list of candidates is forwarded to the rector.

Especially with respect to 'time', it is interesting to give an example of what we did not formalize from the given guideline, even though temporal logics are employed. The guideline says, for instance, "reviews should be prepared within 3 months" (as translated from the German text). The verification engineer did not include this statement into the list of properties (not even their semi-formal representation), since he had his focus on sequences in time, although the so-called X operator of LTL could be used in an attempt to model this statement. In hindsight, we briefly discussed this possibility, where time units would be defined, e.g., a day. Based on that, the checker tool could simulate time slots through loops for a defined number of time units corresponding to 3 months. Obviously, there would a minor intricacy involved, since not every month has the same number of days, but this could be approximated. Another, more serious issue with this approach would be that a day would be the minimum duration of each task. All of these intricacies of this thought experiment are, however, beyond the scope of the given guideline text and the law it is based upon.

A related example of what we clearly did not formalize about 'time' is the phrase "as soon as possible" (in the original German text the word "ehestmöglich") in §7(1), see Table 1 in the last row. Without modeling time units, this cannot even be approximated.

The effort for the manual translation of the given part of the guideline to a set of semi-formally represented properties was approximately six hours. It included eleven paragraphs of the guideline, resulting in 25 semi-formally represented properties, and a meeting of the team for their informal inspection.

The informal inspection of the semi-formal property formulations was an essential part of the full verification process. The translation of a natural language text fragment as given by the guideline is an error-prone process. One or more formulated properties have to cover the textually given facts and characteristics of the described process "Appointing a Professor". At the review meeting, all 25 properties were discussed and analyzed whether they are not in conflict, covering the guideline and adequately representing it.

Based on the results of this review, the verification engineer made a few changes to the semi-formal representation of the properties. After that, he was given the process representation in the form of the excerpt shown in Figure 1, essentially an annotated flow diagram. He constructed an FSM for the control flow, which is shown in Figure 2 for the same excerpt. In essence, he mapped each chart element to an FSM state each. State transitions were derived from the task flow of the given process model. Since the arrow from the state "Invite new reviewers" in Figure 1 is outside of the part selected for presentation here, it is not included in the FSM.

Constructing this FSM may even look straight-forward, especially for the excerpt used in this paper. However, the notation of diagrams like those shown in Figure 1 is not formally specified. In fact, forks of lines can either mean procedural or concurrent flows, as we found in such process representations. So, there is essential ambiguity also in such process diagrams, which make formalization hard in general.

Data objects were extracted from the given process model and may influence control flow decisions: reviewer list, review list, application list, and list of candidates. As illustrated in Figure 2, i numReviews is an internal variable of the data object review list. The value of this variable (either > 0 or = 0) directly influences the state transition in the control flow FSM.

Roles of this process as given through the columns with the header "E / D / C / I" in the process diagram of Figure 1 are modeled through a variable each, all of them of type enumeration, with possible values SC, CSC, etc. The values assigned depend on the given FSM state, e.g., for the state Create C L of this FSM corresponding to the task "Create shortlist of candidates", variables to be used by the model checking tool are assigned as follows: E := SC, C := EOW and I := D.

Once the FSM is defined, based on the given process diagram, it is useful to reflect again on the representation of 'time' apart from sequences. There is a task with the text "Prepare review within 3 months" in the process diagram in Figure 1. In the FSM, it is simply a state with a corresponding identifier. So, the semantics of this text is obviously not represented. The verification engineer saw the correspondence of this text with the corresponding text of the guideline (as discussed above) in passing, but there was no formal verification based on a temporal logic.

For the creation of the FSM and the definition of related variables as derived from (the selected part of) the officially given process diagram, a time effort of approximately three hours was used.

According to the given FSM, the verification engineer manually reformulated the semi-formally represented property statements to corresponding PLTL or CTL formulas, respectively. Informal parts of the semi-formally represented property had to be replaced by expressions referencing states of the FSM and its related variables. In the example used above, the formula "G (inst process.state = Forward C R → inst process.E = Dean)" refers to the process state Forward C R. While the list object is not used here, the state Create C L before Forward C R (in the FSM) creates it.

If a semi-formal representation of a property could not be translated to an adapted PLTL or CTL formula, two cases were to be distinguished:

1. The granularity of the given model was partially not compatible with the level of detail specified in the guideline. Hence, if the verification engineer was unable to redefine some semi-formally represented property, this is not necessarily a violation of the given guideline. 2. An error in the model was identified. A subsequent detailed manual inspection of the model uncovered errors like missing or improper states, undefined variables, etc.

An example of a missing state is the first semi-formally represented property of §7(1). It cannot be translated into a refined formula because there is no state in the given model denoting that "The chairperson of the search committee forwards this list as soon as possible to the responsible dean", i.e., the sentence highlighted in light-gray of the guideline in Table 1 and the corresponding semi-formal property representation. More precisely, there is also a confusion in the process model about the actors SC and CSC involved here, which means a second violation of this property. Yet another task was identified to be missing (with respect to preparing and submitting the final report, which were mixed up in the process model), similarly to the one indicated above. So, a total of three violations were found by the verification engineer already in the course of modeling.

After this final formalization effort of approximately two hours, both the model in the form of an FSM and the set of formalized properties were defined and ready for model checking with the tool.

Tool-supported Model Checking and its Results

For the tool-supported model checking, the formalized process model (in the form of the FSM and its associated variables) and the set of refined properties from the guideline (in the form listed in the fourth column of Table 1) were input to the model checker tool NuSMV. For any property violation found by the model checker tool, it returns a counterexample listing. This is presented as a possible execution sequence violating a specific property formulation. These results had to be manually analyzed by the verification engineer to locate the violations in detail and, finally, to interpret them in terms of the given process model and the guideline it has been verified against.

Table 1 contains examples of such violations found by the NuSMV tool, indicated in dark-gray and mid-gray, respectively. Let us explain the violation shown in midgray first. Listing 1 shows a selected part of the counterexample report for this violated property formula. Such listings refer to states, but these are different from the states of the FSM. In fact, NuSMV enumerates its execution states, whose sequence forms a trace. In this example, State 1.1 denotes that the variable i numReviews, which is a local variable of the data object review list, has the value 0. The control flow FSM reaches its FSM state Prepare at (execution) State 1.13. At State 1.14, the control flow FSM reaches its state Extend because the condition "Are at least 2 reviews available" is not fulfilled. The violation of this property is indicated by the following unspecified transition from the FSM state Extend (State 1.14) to Invite (State 1.16). This FSM state sequence is in conflict with the partial sentence "after this deadline, the search committee makes its decision based on the available reviews" (textual part highlighted in mid-gray of column one). In fact, the guideline does not define what to do if i numReviews = 0. As a consequence, the model checking tool automatically indicates that the given formal property is not satisfied on the formalized input model, and hence the guideline is not consistent with the process model.

Listing 1: Counterexample Tool Output Reporting a Property Violation

For the second property violation found by the tool, highlighted in dark-gray in Table 1, the same counterexample as shown in Listing 1 is returned (possibly with different execution states, but this does not matter). In fact, the value 0 is the cause of the contradictions of both properties. In addition, the property highlighted in dark-gray is also violated if the variable i numReviews is assigned to 1. This has actually been checked with the tool by the verification engineer by forcing it to evaluate an example with the value 1, where the tool tells that this is a counterexample as well.

This second property violation is especially interesting, since it expresses that shifting of the deadline for the submission of Reviews is optional and not mandatory if i numReviews < 2. This is formalized as a CTL formula, which enables the combination of path and state operators. Since the property states that the task "Extend the deadline for 1 month" is optional, it has to be checked whether both paths, one including the task and one not, are reachable. In terms of formalization, simply using the EF operator in one direction is not sufficient, therefore, since it defines that a path exists. This would also include the case of a mandatory extension as given in the process model. So, it is necessary to have a conjunction with the same part of the formula negated, see Table 1.

For the dedicated final adaptation and debugging of the formalized model and properties, a final interpretation, and location of the two violations found by the tool, a time effort of approximately two hours was used.

Summary of Results and Lessons Learned

In total, five problems were revealed in the selected part of the process for appointing a professor. In fact, no problems at all were found in this part by the official review, for which all employees of the university had been invited. Now let us briefly generalize from the case at hand and try to indicate lessons learned that may be useful for similar endeavors:

-Possibly conflicting roles Specifying the process model and the properties to be used for verifying it, should be done by different people. The process model should also not be known in advance by the one(s) formalizing the properties. Having it available, however, imposes the risk that knowing the process already may influence the verification engineer in the semantic interpretation of properties. We think that this is reminiscent of a test-case writer who knows the internal details of the program to be tested. In our case study, this helped the verification engineer to avoid related pitfalls. -Usefulness of a semi-formal representation of properties Introducing a semi-formal representation of properties appears to be helpful, when the final formulas cannot be directly stated because the process model is not (yet) available to the verification engineer. In addition, the semi-formal representation was useful for the informal inspection, since not the whole team had to be familiar with the actual modeling language. -Finding violations in the course of formalization

While usually the emphasis is on finding violations through a model checker tool, already in the course of formalizing properties, certain violations can be revealed. In our case study, even three out of five violations were found in the course of trying to translate the semi-formal representation of properties to formulas fitting the FSM of the process model. -Mismatch of the level of abstraction of the business process model and properties to be checked Especially when the model and the properties are formalized separately, a mismatch of their respective levels of abstraction may occur. In our case study, several statements in the official guideline that the given process diagram was verified against were much more detailed than this diagram with its abstractions. Analyzing such cases helped to determine missing tasks in the process model.

-Formalizing time

It may come as a surprise first that in spite of the use of temporal logics certain aspects of 'time' were not formally represented and, therefore, not verified by the model checker tool. One issue in this regard is, again, the level of abstraction to be used for consistent formalization of the process and its properties, another the expressiveness of the given formalisms. -Ambiguity of legal text It does not come as a surprise, however, that natural language is, in principle, ambiguous. Strictly speaking, we had to deal with a kind of legal text in our case study, which is supposed to be less ambiguous. We believe that we made a reasonable formalization of the text "the search committee may extend the deadline for one month", as given in Table 1 in dark-gray, as discussed in relation to a property violation found by the checker tool. The text is, however, "otherwise the search committee may" ("andernfalls kann die Berufungskommission" in the original German text), which could even deserve a legal interpretation by an educated expert in the given context.

While some of these lessons learned have most likely been observed before and in other areas, we think that especially finding violations already in the course of formalization, as well as mismatch of the level of abstraction of the business process model and properties to be checked are new. Some of our lessons learned may even be more generally relevant for other formalization efforts, e.g., usefulness of a semi-formal representation. In fact, it was also observed in the context of requirements engineering [START_REF] Kaindl | Using hypertext for semiformal representation in requirements engineering practice[END_REF].

Threats to Validity

Of course, there are threats to the validity, both external and internal. Regarding threats to the external validity, having performed just a single case study yet is obviously relevant. In addition, this was a relatively small case study. However, the third author is well informed about the spectrum of business processes subject to the official Quality Audit, and we can state that the chosen one is highly representative. So, for gaining first insights into issues and benefits of applying model checking to the verification of such high-level business process, this case study seems to have been appropriate, especially with regard to the formalization challenge. Still, more cases studies along these lines will be required, also in industry, to substantiate the results.

Regarding threats to the internal validity, let us consider the fact that the verification engineer (the first author) comes from the field of hardware design and verification. The work in this case study may have been easier to tackle with more background on business processes and their modeling. However, our experience shows that especially the core task of formalization was possible to be done well even without. The most important background was the know-how for model checking and its tool support as well as the prior experience with behavioral and temporal modeling, even gained in a completely different domain. In addition, a case study with inductively generalized lessons learned is clearly a weak method for gaining trustable results. However, it is a recognized method for empirical studies and for gaining experience, and we applied it according to the usual way of doing a case study according to the current state of the art. Still, for getting more reliable results for specific hypotheses (to be formulated based on our lessons learned), reproducible experiments will be necessary.

Conclusion

In this paper, we investigate formalizing as required for formal model checking. We present a case study of formalizing an excerpt of a high-level business process of our university and of properties derived from a guideline derived from an Austrian law. A fundamental issue involved was formalizing properties consistently with a process model (yet) unknown to the verification engineer. This has been addressed and solved by using a semi-formal intermediary specification. In this case study, problems in the process model were found already while formalizing, and later by the model checker tool. Overall, several problems were revealed by this approach to model checking that were uncovered in the official review.

In this course, we investigated a new verification option for business process owners whose processes and associated properties are given informally. There is quite some effort involved in such a formalization task, and a case study like ours helps to get an idea of the amount. It just depends on the criticality of the business process, whether the results are worth this effort. The process of our case study is one of those most critical for a university, and none of the problems found by our formalization effort and by the model checker has been found in a review by all members of the university, in principle. So, it is up to the people responsible for a given business process to judge whether this effort may pay off. Our case study shows the feasibility of such an approach and provides data on this trade-off.

Based on all that, we conclude that consistently formalizing is key for successful formal and automated verification of business processes. This has not been addressed yet in the literature. Still, much is left for future work, such as systematically extracting data objects and their life cycles from process models and additional sources, and machine support for incremental formalization (possibly building on [START_REF] Kaindl | How to identify binary relations for domain models[END_REF][START_REF] Kaindl | Semiautomatic generation of glossary links: A practical solution[END_REF]).

E

  = Executes; D = Decides; C = Contributes; I = Informed. SC = Search Committee; R = Reviewer; EOW = Equal opportunities working party; D = Dean; CSC = Chair Person of the Search Committee; RE = Rector.

Fig. 1 :

 1 Fig. 1: Diagram of a Part of the Process for Appointing a Professor

G

  (list = TRUE → F Dean.state = forward candidate list to rector) G (inst process.state = Forward C R → inst process.E = Dean) inst process = Process of appointing a professor; Extend = Extend deadline for 1 month; Create C L = Create shortlist of candidates; Prepare = Prepare review within 3 months; Forward C R = Forward shortlist of candidates to rector. Extend = Extend deadline for 1 month; numReviews = signal number of reviews; Create C L = Create shortlist of candidates; Prepare = Prepare review within 3 months; Forward A R = Forward Applications to Reviewers; Forward C R = Forward shortlist of candidates to rector; Invite = Invite new reviewers.

Fig. 2 :

 2 Fig. 2: FSM of the Part of the Process Model shown in Figure 1

-

  -specification G (inst_process.state = Extend -> F inst_process.state = Create_C_L) is false --as demonstrated by the following execution sequence Trace Type: Counterexample -> State: 1.1 <-... inst_review_list.i_numReviews = 0 ... -> State: 1.13 <-inst_process.state = Prepare -> State: 1.14 <-inst_process.state = Extend -> State: 1.16 <-inst_process.state = Invite ...

Table 1 :

 1 A Selection of Properties as Derived from the Guideline, where Violated Properties are Highlighted through Various Shades of Gray as Background §

	Property Formula	G ((inst process.state = Prepare &	inst review list.i numReviews = 2) → F	inst process.state=Create C L)	AG (((inst process.state = Prepare) &	(inst review list.i numReviews < 2)) →	(!(EF inst process.state = Extend) &	(EF inst process.state = Extend))	G (inst process.state = Extend → F	inst process.state=Create C L)	No refined formalization possible, since	no such state exists in the FSM.
	Semi-formal Property Representation	G (SC has received 2 or more reviews →	F SC.state = create list with candidates)		AG (SC has received less than 2 reviews	→ (!EF SC.state = Extend deadline for 1	month & EF SC.state = Extend deadline	for 1 month)	G (SC.state = Extend → F SC.state = cre-	ate list with candidates )	G (list = TRUE → F CSC.state = forward	candidate list to dean)
	Guideline Text	If according to " §3 Absatz 1" of this guideline more	§6(2) than 2 reviews have been requested, and are 2 reviews	available after 3 months, the search committee makes	its decision based on these available reviews, otherwise	the search committee may extend the deadline for one	month ;	after this deadline, the search committee makes its	decision based on the available reviews	§7(1) The chairperson of the search committee forwards	this list as soon as possible to the responsible dean,	who forwards it to the rector.

Acknowledgment

Part of this research has been carried out in the ProREUSE project (No. 834167), funded by the Austrian FFG.


Adèle Boche

Jean-Loup Farges

Henry De Plinval

A continuous and discrete framework for reconfiguration of control of faulty systems

A novel approach for reconfigurable control systems design against sensor and actuator faults is proposed. The scheme is based on an estimation of the state and of the fault parameters, and on a Partially Observable Markov Decision Process (POMDP), used for the decision task of the feedback controller. The following fault types are considered: locking and loss of effectiveness of the device. The modelling framework includes sensor and actuator faults, while the reconfiguration logic is developed only for actuator faults. The effectiveness of the proposed approach is demonstrated on an academic example.

I. INTRODUCTION

Over the last three decades, the growing demand for safety and reliability in complex systems has drawn significant research in Fault-Tolerant Control (FTC) [START_REF] Zhang | Bibliographical review on reconfigurable faulttolerant control systems[END_REF]. Actuator and sensor FTC is more and more discussed in the literature and many effective methodologies and algorithms for FTC have been developed. FTC is a control system that combines diagnosis with control methods to handle faults in an intelligent way. It permits to maintain overall system stability and acceptable performance in the event of component faults. Generally, methods for FTC are classified into two types. Passive FTC methods which are designed to be robust against faults [START_REF] Liao | Reliable robust flight tracking control: an LMI approach[END_REF], and active FTC methods which react to the system component faults actively by reconfiguring control actions. A direct adaptive approach to achieve good reconfiguration performance without system identification is possible and is demonstrated for actuator faults [START_REF] Kim | Reconfigurable flight control system design using direct adaptive method[END_REF]. However, most of the time, the two steps of active FTC are considered separately. The first step, the Fault Detection and Diagnosis (FDD) has drawn significant work [START_REF] Isermann | Model-based fault-detection and diagnosis-status and applications[END_REF]. The second step, i.e. the reconfiguration unit assumes that an FDD is available. This paper addresses active FTC system against actuator and sensor faults. Indeed, actuators and sensors are essential for safety and reliability of complex systems. It has been shown that the FDD problem for sensor and actuator faults can be treated in two steps. First an approach for detecting and isolating sensor faults is proposed, and in a second time the sensor and the actuator faults are isolated and the loss of control effectiveness and the magnitude of stuck actuator faults are estimated [START_REF] Caliskan | Active fault-tolerant control of UAV dynamics against sensor-actuator failures[END_REF]. Differents reconfigurable controller design methods exist. A method based on a two-stage adaptative Kalman filter for the detection and identification of fault parameters, and on eigenstructure assignment technique for computing on-line new feedback and feedforward gains is demonstrated in [START_REF] Zhang | Active fault-tolerant control system against partial actuator failures[END_REF].

However, this scheme only covers loss of effectiveness actuator faults. Most of the time, the reconfiguration is performed either by considering a bank of controllers associated to a bank of models of the system in nominal and faulty conditions or by adapting indirectly a controller to fault parameters [START_REF] Hwang | A survey of fault detection, isolation, and reconfiguration methods[END_REF]. Finally, another approach proposed an FTC method using Linear Parameter Varying (LPV) virtual actuators and sensors for non-linear systems [START_REF] Rotondo | A virtual actuator and sensor approach for fault tolerant control of LPV systems[END_REF]. This method masks the faults adapting the virtual devices to the nominal LPV controller instead of adapting the LPV controller.

This paper presents a novel approach which builds on the advantages of discrete and continuous frameworks to enable efficient reconfiguration in the case of faults. The approach combines indirect adaptive methods, based on continuous framework, and decision making methods, based on discrete framework. It presents the following originalities with respect to the literature:

• Indirect adaptation for a bank of controllers.

• No abrupt detection of faults but an update of a probability distribution over nominal and faulty modes. • Selection of a controller in the bank taking into account the expected performances given the probability distribution. The paper is organized as follows. Section II describes the modelling framework, first the continuous part of the model, second the discrete part of it. Section III discusses the proposed method for the reconfiguration problem. Section IV describes the controllers used for the particular case of actuator faults reconfiguration. Section V shows simulation results for actuator faults obtained on an academic example.

II. MODELLING

The systems considered have several modes, between which they may switch: a nominal mode, and degraded modes. A degraded mode corresponds to the locking or loss of efficiency of a given sensor or actuator. As a result, they exhibit two types of behaviours: A/ a continuous behaviour, as long as the mode and the controller do not change, which is defined by differential equations; B/ a discrete behaviour, which consists in the modes and controllers switchings.

A. Modelling of the continuous behaviour of the system in any given mode Fig. 1 depicts the general structure of the model.

In the figure, u k ∈ R l is the desired control input, e k ∈ R l is the effective control, x k ∈ R n is the system state, y k ∈ R m corresponds to the system outputs, z k ∈ R m corresponds to the measurement, w x k is a zero-mean white Gaussian noise sequence with covariance Q x k representing the modelling errors, v k is a zero-mean white Gaussian measurement noise sequence with covariance R k , A, B, and C are known matrices, and F 1 and F 2 are functions. The function F 1 , respectively F 2 , permits to model the actuator, respectively sensor, faults.

F 1 B + + + 1 z A C F 2 + + u k e k w x k x k y k t k v k z k Fig. 1. System modelling
The objective is to control the system in such a way that the system state x k follows a reference input r k . A cost: k=K k=0 ||r k -x k || indicates the lack of ability of the FTC to perform this tracking.

The modelling framework of F 1 and F 2 proposed in this article is inspired by [START_REF] Kim | Reconfigurable flight control system design using direct adaptive method[END_REF] and is as follow.

1) Actuator faults: An actuator fault is modelled using a simple function of actuator command as shown in Fig. 2:

F 1 (u i k ) = b i 0k + (1 -b i 1k )u i k System u i k i th control signal e i k
e i k = b i 0k + (1 -b i 1k )u i k (1)
The output e k corresponds to the physical motion performed by the actuator, that is limited in its amplitude. Thus, e k , and

u k are bounded in [u, u].
Within this framework, several types of faults are modelled:

• If there is no fault, the nominal case corresponds to the following setting: b i 0k = 0 and b i 1k = 0. • For a locking case in which the effective control is fixed at a certain value δ 0 , b i 0k = δ 0 and b i 1k = 1. • Consider a bias of a certain value δ 0 . This case can be modelled as b i 0k = δ 0 and b i 1k = 0. • With this modelling, we can also represent the decreased effectiveness case by setting b i 0k = 0 and b i 1k ∈]0, 1[ 2) Sensor faults: Similarly, a sensor fault is modelled using a simple function as shown in Fig. 3:

t i k = c i 0k + (1 -c i 1k )y i k (2)
The outputs z k and y k are bounded in [z, z]. With this modelling, the same types of faults may be represented: locking, decreased effectiveness, and bias. Starting from Fig. 1, the modelling of F 1 (1) and the modelling of F 2 (2), the discretised equations of the continuous system are modelled by the following equations:

F 2 (y i k ) = c i 0k + (1 -c i 1k )y i k System y i k t i k i th measurement
x k+1 = Ax k + Bu k + Bb 0k + D k (u k )b 1k + w x k z k = Cx k + c 0k + C k (x k )c 1k + v k (3) with D k (u k ) = B      -u 1 k 0 • • • 0 0 -u 2 k • • • 0 . . . . . . . . . . . . 0 ... 0 -u l k      and C k (x k ) =    -C(1, :)x 1 k • • • 0 . . . . . . . . . 0 ... -C(m, :)x m k   
The values of the parameters b 0 , b 1 , c 0 , and c 1 change in the case of faults. From the estimation viewpoint, these values and their behaviour are unknown. In the continuous part of the model their behaviours are random walks:

       b 0k+1 = b 0k + w b0 k b 1k+1 = b 1k + w b1 k c 0k+1 = c 0k + w c0 k c 1k+1 = c 1k + w c1 k (4)

B. Discrete modelling

The reconfiguration problem can be modelled as a Partially Observable Markov Decision Process (POMDP) [START_REF] Kaelbling | Planning and acting in partially observable stochastic domains[END_REF]. It is classically defined as a 6-tuple {S, A, T, R, Ω, O} :

• S = {s 0 , ...s |S|-1 } is a finite set of states, • A = {a 0 , ...a |A|-1 } is a finite set of actions, • T : S × A × S → [0; 1] is a set of conditional transition probabilities between states, • R : S × A × S → R is the cost function, • Ω = {ω 0 ...ω |Ω|-1 } is a finite set of observations, and • O : S × Ω → [0; 1] is a set of conditional observation
probabilities These elements are defined as follow for the framework. 1) States: The proposed framework considers only single faults. Let m actuator be the number of fault modes of an actuator and m sensor be the number of fault modes of a sensor. Thus, we have at most a nominal mode, m actuator ×l actuator fault modes and m sensor × m sensor fault modes. Each mode m i has an associated controller k i which has been designed for this mode, so its performance is expected to be better than that obtained with the other controllers. However, at a given time step, it is possible that the system is in mode m i and is controlled by another controller k j . Thus, a set S of states s i,j = (m i , k j ) is defined with a mode and a controller. S has at most (1 + m actuator × l + m sensor × m) 2 states.

2) Actions: The action a i consists by definition in selecting the controller k i for next time step. The system dynamics is as shown in Fig. 4. 3) Conditional transition probabilities: The general form of a transition probability is p(s |s, a), however the problem can be simplified. Indeed, on the one hand the dynamics of the active controller: k k+1 = a k is deterministic, and on the other hand the transitions between the modes are not dependant on the controller. The transition probabilities p(m |m) between modes are stationary. To define a realistic model, these probabilities are considering the sensor/actuator documentation that may contain key information such as the failure rate, and previous studies addresing this topic [START_REF] Freeman | Reliability assessment for low-cost unmanned aerial vehicles[END_REF].

m k k k a k r k m k+1 k k+1 a k+1 r k+1 m k+2 k k+2 • • •
Fig. 5 shows an example for a problem with three modes.

m 0 m 1 m 2 p(m 0 |m 0 ) p(m 1 |m 0 ) p(m 2 |m 0 ) p(m 1 |m 1 ) p(m 0 |m 1 ) p(m 2 |m 1 ) p(m 2 |m 2 ) p(m 0 |m 2 ) p(m 1 |m 2 )
Fig. 5. Directed probabilistic graph

4) Cost function:

To find the best controller to choose, different values of costs are imposed depending on the current state s k , the next state s k+1 , and the action a k . With this method, penalties can be added to the event of changing of controller, so that the potential performance loss triggered by this switch may be taken into account. The costs and the penalties can be calculated analytically or numerically. In this article, the costs are calculated numerically with the error between the state and the reference, assuming that the future of the reference input r k is known, and depend on the time. The penalties permit to avoid controller switching without reason and add a conservatism reward. The cost function is as follow:

R(s k , a k , s k+1 ) = E /s k+1 ||r k+1 -x k+1 || + P (k k , a k ) (5)
where E /s k+1 ||r k+1 -x k+1 || is an estimation of the elementary cost of the tracking error at time k + 1 of the controller indicated in s k+1 for the mode of s k+1 and P (k k , a k ) equal to zero is k k = a k and to a given value otherwise. Note that, unlike the classical POMDP framework, the cost function is not stationary.

5) Observations:

The classical POMDP framework requires observations taking values in a discrete set; but, here, the observation is based on the information of the continuous processus provided by an estimation scheme:

ω = { b 0k , b 1k , c 0k , c 1k }.
6) Conditional observation probabilities: In this part, the principle is only explained for an actuator which can be faulty. Assuming that the estimation scheme offers a continuous output, namely: ω = { b 0 , b 1 } and a probability density function; that is even with respect to the errors between on the one hand b 0 and b 0 and on the other hand b 1 and b 1 , the role of the parameters b 0 , b 1 and the role of the estimates b 0 , b 1 , are exchanged.

Thus, assuming p(b 0 , b 1 |ω) = p(ω|b 0 , b 1 ), the observation probability is given by integrating this quantity over the domain corresponding to each mode, namely:

p(ω|m) = f m (b 0 , b 1 )p(ω|b 0 , b 1 )db 0 db 1 (6)
where f m (b 0 , b 1 ) depend on the mode. In order to design an estimation scheme able to determine the most probable current mode, several assumptions are made on the distribution of the parameters b 0 and b 1 , for each mode. For example, in this paper, the hypothesis for the actuator fault modes are the following:

• Nominal case: f m (b 0 , b 1 ) = δ(b 0 )δ(b 1 ) (7)
• Locking case:

f m (b 0 , b 1 ) = 1 u -u H(b 0 -u)H(u -b 0 )δ(b 1 ) (8)
• Loss of effectiveness case:

f m (b 0 , b 1 ) = H(b 1 )H(1 -b 1 )δ(b 0 ) (9)

III. RECONFIGURATION METHOD

A. Estimation 1) Filtering state and fault model parameters: In order to estimate the current mode of the system, the proposed methods consists in estimating the fault parameters b i 0 , b i 1 , c i 0 and c i 1 , which, in turn, necessitates to estimate also the state x of the system. The fault parameters estimates will be exploited to deduce the most probable current mode, which will be used as the observation input for the POMDP. To estimate the state and these parameters, several methods exist. They are usually based on models, and this is the choice made in this paper in the hope that using an accurate model will lead to improved performances. For the estimation of the actuator parameters, the following methods can be used: observer method, Kalman filter or particle filter. For the estimation of the sensor parameters, a non-linear method is required. For example, the following methods can be used: extended Kalman filter, unscented Kalman filter or particle filer. However, the random walks of equation ( 4) are not fully consistent with an abrupt fault occurrence. Thus, the classical filtering methods are modified in order to test the likelihood of each z k and to flatten the probability density function of b i 0 , b i 1 , c i 0 and c i 1 in case of an unlikely z k . 2) Estimating fault mode probabilities: At each time period k, the system is in some state s k ∈ S. The FTC takes an action a k ∈ A, which causes the system to transition to a new state s k+1 ∈ S with probability T (s k+1 |s k , a k ). Then, an observation ω ∈ Ω is computed from the probability density function managed by the continuous filter. The FTC updates a vector made of probabilities of the system being in each discrete state, b(s). This vector, named belief state, is updated using the Bayes rule. In general, the update b a,ω (s ) depends on the action a, the observation ω, and is function of the previous belief state (s = s k+1 follow the state s As explained previously, the transitions between the modes are not dependant on the controller. Thus, the equation ( 10) can be reduced as follows:

= s k ) b a,ω (s ) = p(ω|s )p(s |b, a) p(ω|b, a) (10) where
b ω (m ) = p(ω|m )p(m |b) p(ω|b) (11)
where :

p(m |b) = m p(m |m)b(m) p(ω|b) = m p(ω|m )p(m |b)
and p(ω|m) is given by equation( 6).

B. Switching Decision Optimization 1) Discretisation of the observation domain:

In order to use classical POMDP framework, one needs to discretise the observation domain to recover a discrete observation.

This can be done mostly in two ways:

• by forcing an a priori discretisation on the observation space, • by finding a partition such that each different subdomain leads to a change in the resulting policy [START_REF] Hoey | Solving pomdps with continuous or large discrete observation spaces[END_REF]. Let {Ω 1 , ..., Ω |Ω| } a partition of the continuous space in which the ω parameters evolves. Then, the probability to have the parameters in a given set Ω i is given by:

p(Ω i |m) = ω∈Ω i p(ω|m)dω (12)
Note that this is a multiple integral. For instance, for a single actuator which can be faulty, it is a double integral with dω standing for d b 0 d b 1 . Finally, to this p(Ω i |m) corresponds a p(Ω i |s).

2) Dynamic Programming: In the previously defined framework, the goal is to construct a policy π : ∆ → A (∆ the set of belief state) which minimize a criteria. The objective is to minimize the cost R.

Equation 13 represents the problem to be solved:

V k (b) = min a∈A [r(b, a) + γ |Ω| i=1 p(Ω i |b, a)V k+1 (b a,Ω i )] (13)
where γ ∈ [0, 1[ is a discount factor, and

     r(b, a) = s s b(s)R(s, a, s )p(s |s, a) p(Ω i |b, a) = s p(Ω i |s )p(s |b, a) b a,Ω i (s ) = p(Ω i |m )p(m |b) p(Ω i |b)
This problem can be solved over a finite horizon from time k to time k + H. The policy π specifies the action a which maximizes the value function V k (b) Equation ( 13) is solved by: 1) expending from the current belief state the tree of possible b values in function of all possible future actions and discrete observations and, 2) computing backwards the value of V . In order to compensate for a small value for H, the quantity:

K k =k+H+1 R(s k , k, s k+1 ) with a constant controller is used for initializing V k+H+1 .

IV. CONTROLLERS FOR ACTUATOR FAULTS

As discussed previously, there are (1 + m actuator × l + m sensor × m) controllers k, one for each mode m. Each controller sends different control signal, u k , in order the effective control e k to be like:

e k = -K( x k -r k ) (14)
The information of x k is not available, thus the state estimate x k is used in the control law.

A. Adaptivity

The controllers for the faulty modes should be adaptive, based on the estimation of the fault parameters b 0k and b 1k as shown in Fig. 6.

With no fault, there is no need to have an adaptive controller because b 0 and b 1 are null. Moreover, b 0 and b 1 are noisy because they are estimates. So, in the nominal configuration, a controller without the estimated parameters seem to be more adapted than an adaptive controller which is noisy.

B. Nominal Controller k 0

In the nominal case, all the actuators are nominal, i.e:

∀i, b i 0k = 0 b i 1k = 0 Estimator Controller k i Controller k 0 Controller k 1 . . . . . . b 0k , b 1k u k signal control x k Fig. 6. Adaptative Controller
Thus, e k = u k and so the nominal controller is as follows:

u k = -K( x k -r k ) (15)

C. Controllers for locking modes

By definition, in the locking case, one actuator, the j th one, is locked at some value δ 0 , while the others are nominal, i.e:

∀i = j,        b i 0k = 0 b i 1k = 0 b j 0k = δ 0 ∈ [u, u] b j 1k = 1 Thus, e k = u 1 k • • • u j-1 k δ 0 u j+1 k • • • u l k T .
To be able to compensate for the locked actuator, it is assume that the action of this actuator is a linear combination of other actuators, i.e. the j th column of B is a linear combination of the other columns, i.e.

B .j = i =j λ i B .i , with B = [B .1 • • • B .i • • • B .l ].
On the one hand, the control implies:

Be k = B .j δ 0 + i =j B .i u i k = i =j B .i (λ i δ 0 + u i k )
On the other hand, the requirement implies:

Be k = -BK( x k -r k ) = -i =j B .i (λ i K j. + K i. )( x k -r k ) with K T = [K T 1. • • • K T i. • • • K T l.
]. Identifying the terms in B .i gives:

u k =         -(λ 1 K j. + K 1. )( x k -r k ) -λ 1 δ 0 . . . b 0 . . . -(λ l K j. + K l. )( x k -r k ) -λ l δ 0         (16)
However, with this controller, there is an observability problem. If the j th actuator is no longer locked, the control signal still send the value b 0 and thus, the estimator do not detect the restoration of the actuator. To solve this problem, an input signal, such as a 3211 input signal [START_REF] Heredia | Actuator fault detection in autonomous helicopters[END_REF], could be added to b 0 in order to make the system observable. This signal will have no effect if the j th actuator is actually locked, and in the opposite case, it can solve the problem of observability.

D. Controllers for loss of effectiveness modes

In the loss of effectiveness case, the j th actuator is reduced by a factor γ 1 and the others are nominal, i.e:

∀i = j,        b i 0k = 0 b i 1k = 0 b j 0k = 0 b j 1k = γ 1 ∈]0, 1[ Thus, e k = u 1 k • • • u j-1 k (1 -γ 1 )u j k u j+1 k • • • u l k T
, and so the associated controller is chosen as follow:

u k =          -K 1. ( x k -r k ) . . . -Kj.( x k -r k ) 1-b1 i k . . . -K l. ( x k -r k )          (17)
V. ILLUSTRATIVE EXAMPLE

A. Model

An academic model is used to illustrate the proposed reconfiguration framework. The state x is composed of the position and the velocity of a mobile. Two actuators are used, u = u 1 u 2 T , such as the acceleration is equal to the sum of effects of the actuators, e 1 + e 2 . The control inputs u 1 , u 2 and e 1 , e 2 are bounded to [-10, 10]. The system has two sensors, one for the position and another for the speed. Using a one second sampling time, the discretised model is the following:

       x k+1 = 1 1 0 1 x k + 0.5 0.5 1 1 e k + w x k y k = 1 0 0 1 x k + v k (18)
The reference signal to be followed by the mobile, r, for an horizon of 100 seconds, is presented in the upper part of Fig. 8, for r 1 and in the upper part of Fig. 9 for r 2 .

Only faults of the second actuator are considered:

e 1 k = u 1 k e 2 k = b 0k + (1 -b 1k )u 2 k (19)
Parameters used in the simulation are as follows.

Q x k = diag{0.05 2 , 0.05 2 }, Q b k = diag{0.005 2 , 0.005 2 }, and R k = diag{1 2 , 0.1 2 }.
In this example, there are three modes: nominal m 0 , locking m 1 , and loss of effectiveness m 2 . Each mode will have an associated controller k i . Thus, we have nine discrete states: S = {s 0 , ...s 8 } = {{m 0 , k 0 }, {m 0 , k 1 }...{m 2 , k 2 }}. The mode transition graph is the one of Fig. 5 with:

• p(m 0 |m 0 ) = e -10 -5 • p(m 1 |m 0 ) = p(m 2 |m 0 ) = (1 -p(m 0 |m 0 ))/2 • p(m 0 |m 1 ) = p(m 0 |m 2 ) = 10 -4 • p(m 1 |m 1 ) = p(m 2 |m 2 ) = (1 -10 -4 ) 2 • p(m 2 |m 1 ) = p(m 1 |m 2 ) = 10 -4 (1 -10 -4 )

B. Controllers

Based on the IV. part, the three controllers are:

• the nominal one k 0 associated to the nominal mode m 0 :

u 1 k u 2 k = -K( x k -r k ) -K( x k -r k ) (20)
• the controller k 1 associated to the locking mode m 1 :

u 1 k u 2 k = -2K( x k -r k ) -b 0 b 0 (21)
• the controller k 2 associated to the loss of effectiveness mode m 2 :

u 1 k u 2 k = -K( x k -r k ) -K( x k -r k )-b0 1-b1 (22)
with K = 0.9 0.8 .

C. Cost function

For this example, the cost is calculated as follow:

E /s ||r k -x k || = E /s 100 k =k |x 1 k -r 1 k | + |x 2 k -r 2 k | (23)
where E /s indicates the expectation with respect to the discrete state. For the nominal mode, the expectation is computed by performing 100 runs with different values for noise sequences and averaging the cost values. For non nominal modes, the 100 runs are repeated 19 and 9 times, for respectively the locking and the loss of effectiveness modes, varying the fault parameter. The average is then computed considering the 19 × 100 runs for variation of b 0 and 9 × 100 runs for variation of b 1 . Fig. 7 shows the evolution of the cost. For the nominal case shown in the upper part of Fig. 7:

• The controller k 0 and k 2 are very close. Indeed, b 0 and b 1 are null, thus k 2 controls a loss of effectiveness close to zero, which leads to a controller similar to k 0 . The difference comes from the noise.

• The controller k 1 is not good before 70s, but after the three controllers have similar performance. The bad performance of the controller k 1 at the start of the simulation comes from the saturation of the command. For the locking case shown in the middle part of Fig. 7: • The controllers k 0 and k 2 have the same performance.

Indeed, the first control is the same in the two controllers and the second control is locked. • The controller k 1 has better performance all along the horizon because the locked actuator is compensated by the other. For the loss of effectiveness case shown in the lower part of Fig. 7: • The controller k 2 has the best performance result at the start of the simulation. • The controller k 1 is not good before 70s because of the saturation of the control. After the three controllers have similar performance. Arbitrary penalties, P (k 0 , a 1 ) = P (k 0 , a 2 ) = 1, P (k 1 , a 0 ) = P (k 1 , a 2 ) = 12.5 and P (k 2 , a 0 ) = P (k 2 , a 1 ) = 4, are added in order to avoid sudden changes of controller at the end of the simulation. Indeed, in Fig. 7, it is shown that some costs are similars.

D. Estimation method

To estimate the state x and the parameters b 0 and b 1 , an augmented system is considered, which includes the system "natural" state -position, velocity-with equations 18, together with the fault parameters. Then a Kalman filter is applied to the resulting augmented system, which may be described by:

G. Fault scenario

To test the design, the scenario including a loss of effectiveness case and a locking case, as shown in Table I.

Fig. 2 .

 2 Fig. 2. Modelling of the i th actuator faults

Fig. 3 .

 3 Fig. 3. Modelling of the i th sensor faults

Fig. 4 .

 4 Fig. 4. State update with the action

  : p(s |b, a) = s p(s |s, a)b(s) p(ω|b, a) = s p(ω|s )p(s |b, a)

  Fig. 7. Cost

X 1 C

 1 k+1 = A aug X k + B aug u k + W aug k y k = C aug X k + v k (24) with A aug =   A B .,2 D k.,2 (u k ) 0 aug = C 0 2,1 0 2,1 ,and W aug kIn the estimation algorithm, the covariance P (k + 1|k) is reopened when the following test is not passed:∀i ∈ [1, m],(C i. P (k + 1|k)C T i. + R ii ) -1 (y i k+1 -C i. X(k + 1|k)) 2 ≤ 5 2 (25)The covariance is reopened as follows:P (k + 1|k) reset = Observation probabilitiesApplying Equations 6 to 9 to the example leads to:p(ω|m 0 ) = 1 2π |P | e -12 b T P -1 b with P the 2×2 matrix at the lower right part of P (k+1|k).

F

  . Partition of Ω and Dynamic Programming horizonTo avoid a long computational time, Ω is partitioned in four areas, and the horizon is H = 5. Ω is partitioned as follows:• b 0 ∈ [-0.1, 0.1] and b 1 ∈ [0, 0.1] • b 0 ∈ [-0.1, 0.1] and b 1 ∈ [0.1, 0.9] • b 0 ∈ [-0.1, 0.1] and b 1 ∈ [0.9, 1] • b 0 ∈ [-10, -0.1[∪]0.1, 10] and b 1 ∈ [0.9, 1]

Reference Position

1) Estimation of state and fault parameters: The dashed curves in lower parts of Fig. 8 and Fig. 9 presents the state estimation error. These errors are small, with the exception of a peak at time 70s. The locking event induces a temporary error of about 3m/s for velocity and 1m for position. The values b 0 , b 1 and their estimates are shown in Fig. 10. The estimator detects the fault in less than 10s. For each event, the covariance is reopened to detect the fault. For the locking event, it is reopened twice, indicating an adaptation. This is more difficult than for the other events.

2) Probabilities: The probabilities of the modes are shown in Fig. 11. The probability of the most likely mode is close to one, except for a short time during the transition.

3) Action: As shown in Fig. 12, the controller is changed as follows:

• When the loss of effectiveness is detected, at 23s, the controller is changed at the nest step, at 24s. Indeed the effectiveness of the nominal controller k 0 in the case of loss of effectiveness is lower than the one of the associated controller k 2 . • When the effectiveness of the actuator is back, the controller is not changed from k 2 to k 0 because the reward is not large enough compared to the penalty associated to any change of controller. • When the actuator is locked, at 72s, the controller is changed at the next step, at 73s. 4) Control: Fig. 13 presents the control for the two actuators. Between 20s and 50s, the actuator is reduced of 50%. After 70s, it is locked to 5m/s 2 . The effective control e 2 is over estimated for a short time after the locking event. The plain curves in the lower part of Fig. 8 and Fig. 9 present the tracking error for respectively position and velocity. The errors are between -12 and +12 and are most of the time close to zero, indicating that despite the presence of faults the system state follows the reference leading to an acceptable performance.

Finally, with this FTC method, a gain of 25% on the sum of tracking errors is obtained with respect to the use of only the nominal controller.

VI. CONCLUSION

In this article, a modelling framework is defined for actuator and sensor faults. This modelling combines discrete and continuous frameworks, allowing to take profit of the advantages of discrete and continuous methods. A reconfiguration method is developed for the actuator faults and is tested on an academic example. This method has shown good results; in the event of component faults, this method improves significantly the performance with respect to the use of a single controller. The framework proposed here can be the basis for additional researches about:

• Addition of input signals to the controller for locking modes in order to make the fault parameters observable. • Reconfiguration for sensor faults.

• Computation time reduction for the choice of the action by solving a simplified but still relevant discrete optimisation problem. • Empiric assessment on a large number of scenarios with several devices, possibly faulty.


Sankar

Investigation for Efficient Fractal Antenna Arrays with Novel Design Methodology and Fractal Excitations

  L'archive ouverte pluridisciplinaire

Investigation for Efficient Fractal Antenna Arrays with Novel Design Methodology and Fractal Excitations

V.A.Sankar Ponnapalli 1 ,P.V.Y.Jayasree 2 Dept. of Electronics and Communication Engineering GITAM University, Visakhapatnam Andhra Pradesh, India. vadityasankar3@gmail.com [START_REF] Ma | Theory and Application of Antenna Arrays[END_REF] ,pvyjayasree@gitam.edu 2 Abstract-Fractal Antennas and Antenna arrays are frequency independent-multiband antennas. These antennas have become popular due to their recursive nature and rapid beam forming algorithms. Like conventional antenna arrays, side lobe level and beam width are the primary designing challenges in these arrays. But basic drawback of these arrays is huge number of elements (Depending on expansion factor). To overcome these challenges in fractal antenna arrays, again the solution is in the fractal geometry. In fractal geometry, any shape or structure or number can be recursively generated with fractional dimensions, this means the same shape or number repeats again and again with different dimensions. Fractal antenna technology is geometry-based, not material based, that's why fractal antennas are also called as artistic antennas. Novel design methodologies and new fractal shapes may be helpful for further improvement of antenna parameters. This work proposes a concentric elliptical ring sub array generator design methodology for the systematic expansion of deterministic fractal antenna arrays. Using this design methodology any polygon shape can be constructed. This methodology replicates the concentric circular ring sub array generator but in this case circular generator is replaced with an elliptical generator. This methodology shows better performance in orientation of the structure, Side lobe level and 3-dB beam width rather than previous design methodologies.

Reduced side lobe level in any antenna array can be achieved with non-uniform current excitations. But, due to huge number of elements in fractal arrays application of conventional current excitations like binomial current distribution to this type of arrays may be difficult in practical implementation. Conventional current distributions can be useful for side lobe level reduction and formation of narrow or broad beam widths depending on the application. But thinning of elements cannot be achieved with the conventional current distributions, while maintaining proper side lobe level and beam width values. This work proposes various fractal current distributions exclusively for thinning of fractal antenna arrays with proper balancing between side lobe level and beam width values. The two methods, namely concentric elliptical ring sub array generator and fractal distribution of current can be helpful for the efficient design of fractal antenna arrays with less cost of designing.

Keywords: Fractal Antenna Arrays; Concentric Elliptical-Sub Array Design Methodology; Fractal Excitations; Side lobe level; Beam width;

Design Methodology

New design methodologies may be helpful for the improvement of fractal antenna array performance. This work proposes a concentric elliptical ring sub array generator for the expansion of different types of fractal arrays.

Fractal Sequence

A fractal sequence is a number sequence that obeys the property of self-similarity. Like fractal shapes fractal sequences are also repeats again and again with different values. A wide variety of fractal sequences are available, this report considered three valued fractal sequence proposed by Morse and Thue, the sequence can be extended to infinite set of values. The generalized three-valued Morse-Thue sequence is, 0 (Seed) 0 1 2 (1st iteration) 0 1 2 1 2 0 2 0 1 (2nd iteration) 0 1 2 1 2 0 2 0 1 1 2 0 2 0 1 0 1 2 2 0 1 0 1 2 1 2 0 (3 rd iteration) 0 1 2 1 2 0 2 0 1 1 2 0 2 0 1 0 1 2 2 0 1 0 1 2 1 2 0 1 2 0 2 0 1 0 1 2 2 0 1 0 1 2 1 2 0 0 1 2 1 2 0 2 0 1 2 0 1 0 1 2 1 2 0 0 1 2 1 2 0 2 0 1 1 2 0 2 0 1 0 1 2 0 1 2----------------------

(nth iteration)

Morse-Thue sequence starts with "0", this is the seed of that sequence. Generation of the sequence should depend on the value of the sequence. If the value of the sequence is two then first iteration should be "0 1", if the value of the sequence is three then first iteration should be "0 1 2".In second iteration "0" should be replaced by "0 1 2", "1" should be replaced by "1 2 0" and "3" should be replaced by "2 0 1". By this process series can be extended to nth iteration. Of course, we cannot show the complete sequence, it is infinite. In this work from first iteration to sixth iteration has considered for excitation of antenna elements.