Fabien Bouffaron
email: fabien.bouffaron@univ-lorraine.fr

Pascale Marange
email: pascale.marange@univ-lorraine.fr

Gérard Morel
email: gerard.morel@univ-lorraine.fr

Checking models based on an iterative co-specification process of a critical system

Keywords: model based systems engineering, cospecification, verification/validation, model-checking, dependability requirements, I

Recurrent incident reports indicate that critical systems such as power plants exhibit unintended emergent behaviors outside of acceptable limits, despite of the increasing development of dependable automation technologies as well as of a lot of techniques related to dependability issues. Among many causes, the role of human for operating technical artefacts is of importance, but also for designing them from the early stages of specification in order to check the basic property of wholeness of any system. A mean is to ensure a continuum of compliant models to component integration through an iterative process between all the disciplines involved to engineer these systems as whole all along their life cycle. However, a human-based process to check the "right-system requirements-right" remains not fully adequate at the scale of real systems engineering projects and in any case to critical issues. This paper explores the formal checking compliance of architecting models with dependability requirements. These models are refined iteratively by specialist and specialty engineers interoperating with a system engineer through a co-specification process on a particular case study of a critical power-plant subsystem.

INTRODUCTION

Because of the resilient nature of human operators to face unintended emergent behaviors [START_REF] Hollnagel | Joint cognitive systems: Foundations of cognitive systems engineering[END_REF], a generation of power plant remains largely under human control. They are assisted in their work by automation technologies that provide the least important part of the overall control information. Control room operators and field operators interoperate together to perform documented procedures in order to align a lot of devices only partly automated to process energy flows. The increasing readiness level of automation technologies embedding somewhat of a technical intelligence is expected to enlarge the part of digital control information in order to offer new services to field operators. This last objective is addressed by the R&D programme of the CONNEXION 1 cluster for the next 1 https://www.cluster-connexion.fr/ generation of power plant as well as for the revamping of current ones. Its purpose is to design innovative architectures compliant with the main advances in component solutions for distributed industrial automation systems. To meet the main objective of increasing the dependability integrity levels of the overall process, the systems engineering (SE) framework is a model-based integrative approach. Its aim is to check how the system parts, and consequently the related engineering ones, interoperate such that they reproduce or transform a whole. The expected result, "in contradistinction with traditional control engineering approaches focusing first on separate parts"2 , is to check the "right-system requirements-right" between all the stakeholders involved throughout a power plant life cycle, including the enabling systems, and especially the automation system engineering. The use of models for verification and validation of dependable requirements to component solution integration is compliant with the last recommended best practices in industry [START_REF] Fanmuy | Requirements verification in the industry[END_REF].

The role of the system architect beyond technical aspect remains challenging and issues presented in this paper and others related ones [START_REF] Bouffaron | Revisiting the interoperation relationships between Systems Engineering collaborative processes[END_REF], [START_REF] Bouffaron | Integrative construct for Model-Based Human-System Integration: a case study[END_REF] are in line with those of this R&D programme. Section 2 contextualizes our CISPI-AFW case study reflecting on a lab-platform some critical features of power plant automation. It also presents the co-specification process used to engineer this system. Section 3 details a particular co-specification scenario to design a logical architecture in order to highlight the set of models refined iteratively by specialist and specialty engineers interoperating with a system engineer. Section 4 formally checks the consistency of the overall models with dependability system requirements at different stages of the studied cospecification process. To conclude, section 5 highlights on going works related to others engineering domains involved in a broader cospecification process for critical power plant control. Moreover, some perspectives are drawn on how to combine model-checking and co-simulation techniques for verification and validation issues.

II. CO-SPECIFICATION PROCESS OF THE STUDIED

SYSTEM

Our case study reflects, on the one hand, some features of an auxiliary feedwater (AFW) system in emergencies. It is historically recognized as a critical sub-system [START_REF] Casada | Auxiliary feedwater system aging study[END_REF] [6] of some power-plant generations. AFW aim is to maintain an adequate water level in the steam generator (SG) by providing feedwater to the latter, during normal operations (startup and shutdown evolutions) as well as for emergency issues (Fig. 1). Fig. 1. AFW sub-system in emergencies (adapted from [START_REF] Duco | Accidents nucléaires. Three Mile Island (Etats-Unis)[END_REF] ) Then, our co-specification process reflects, on the other hand, a set of engineering domains involved in the automation design of such AFW sub-system. Systems engineering play an integrative role as a concurrent, iterative and recursive problem-solving process when architecting a system solution through feedbacks (Fig. 2).

A. Studied Critical Sub-System

Our CISPI lab platform3 is composed of three tanks, one of which may be associated with the feedwater storage tank and another with a steam generator. SG tank leakage output aims to simulate the flow of steam released relaxation into the atmosphere. These two tanks are interconnected by two redundant lines consisting of a manual valve, a flow meter and a control valve (Fig. 3). The architectural concept is to distribute around a fieldbus a set of "intelligent actuation and measurement systems" (IAMS) within an integrated system of control, maintenance and technical management (CMMS), including control by human operators [START_REF] Dobre | Improving humansystem digital interaction for industrial system control: some systems engineering issues[END_REF]. This paper highlights some dependability issues related to the preliminary logical definition of this architecture by several specialist and specialty engineering. This step is before the allocation of the specified function blocks to human operators and/or to automation components.

B. Studied Co-Specification Process

We revisited in previous works [START_REF] Bouffaron | Revisiting the interoperation relationships between Systems Engineering collaborative processes[END_REF] the nature of these SE feedbacks focusing mainly on the System Breakdown Structure. (Fig. 2). Following and extending the problem-frame approach for software engineering [START_REF] Jackson | Problem frames: analysing and structuring software development problems[END_REF] related to the meaning of requirements specification [START_REF] Jin | Revisiting the meaning of requirements[END_REF], we argue that the basic driver of these feedbacks is first the quest of knowledge by the system architect from specialist engineering domains at each level, which is then reiterated through the system breakdown structure. Let's consider such a knowledge-based iteration 4between the problem-space (PS SE ) of the SE domain and a solution-space (SS AE ) of the Automation Engineering domain. We argue that the added knowledge (K_SS AE ) from the AE solution-space (1) contributes iteratively to achieve the satisfaction of an automation (software-based) system specification (S AE ) from system requirements (S SE ) described by an SE problem-space (2) according to entailments:

K_SS AE , S SE  S AE (1)
K_PS SE , S AE  S SE [START_REF] Fanmuy | Requirements verification in the industry[END_REF] At the scale of an overall SE process restricted to our case-study, we generalize this iterative cospecification process between all the problemspace/solution-space of the engineering domains ( W OP , S SE  R OE [START_REF] Hollnagel | Joint cognitive systems: Foundations of cognitive systems engineering[END_REF] where W OP represents the operational environment knowledge of the target system and R OE is a set of requirements described by the related operational engineering problem space (PS OE ).

Note that each specialist specification may be verified, for example by execution of models, within its own solution-space but must be validated by the related problem-space. In order to improve a lean management of the overall engineering workflow, we suggest distributing this co-specification process around a bus (Fig. 4). A main interest is that engineers from various domains can use their own tools, methods, technics to interoperate with each other by the mean of a common language, such as the de-facto standardized SysML [START_REF] Omg | OMG Systems Modeling Language (OMG SysML)[END_REF] in our case-study. Indeed, maturity of digital technologies for modeling and simulation allows considering the exchange and model coexecution through standardized interfaces for connecting different simulation environments. The "Functional Mockup Interface" [START_REF] Blochwitz | Functional mockup interface 2.0: The standard for tool independent exchange of simulation models[END_REF] defined by the European ITEA2 Modelisar project is a promising candidate to become the industry standard for cosimulation models and cross-company collaboration [START_REF] Bertsch | The Functional Mockup Interface-seen from an industrial perspective[END_REF]. The validation of a co-specification by coexecution of models can replace current technics of code generation and integration that are dependent on interoperability levels between tools. Thus, in our R&D framework, various domains and their respective tools (process engineering: Dymola ® , automation engineering: Matlab ® /Simulink ® , system engineering: IBM Rational ® Rhapsody) interoperate through a co-simulation bus 5 .

Section III, describes a co-specification scenario between SE problem space (PS SE ) and specialist engineers who prescribe specification models (S model ) from the system specification (S SE ). As addressed in section IV, a special attention should be paid to the transversal dependability engineering solution space (SS DE ) to check more formally theses specification models satisfying:

K_PS SE , S model , K_SS DE  S SE .
(2)

III. LOGICAL ARCHITECTURE CO-SPECIFICATION

We focus our scenario on the study of systems engineering activities during the co-specification of logical architecture. At this point, we consider the following set of system requirements (S SE ) satisfying the set of stakeholder requirements (R OE ) during an accident situation (W OP ) (Fig. 1) according to the entailment (3):

Stereotype ID Text

Functional

S SE1

The water level shall be maintained at 50 cm in the steam generator tank

Functional

S SE2

The emergency water flow shall be 20 L.min -1 Dependability S SE3

The feedwater system shall satisfy single failure criterion System engineer has to prescribe a logical architecture (LA SE ) requiring knowledge of several specialist solution spaces (process and automation engineering) in order to meet system requirements.

A. Specification of the AFW process

A first iteration is to specify the physical process to be controlled. From this task, there is an emergent problem about the specification of a process observing the laws of physics. Indeed, system engineer does not have the expertise to perform this task. In this sense, system engineering problem space formalizes this problem into requirements. These are then broadcast on the co-specification bus, pending a specialist engineer can address it. Process engineering solution space (SS PE ) being able to meet this problem (S SE ) specifies CISPI-AFW process (S PE ) according to: K_SS PE , S SE  S PE [START_REF] Bouffaron | Revisiting the interoperation relationships between Systems Engineering collaborative processes[END_REF] S PE prescribes a process with two alignment functions (Water_Supply) providing transport of water between two storage functions (Water_Storage). So that the process engineer can interact with the system engineer, it is important that both share a common representation of the solution in a common language. In this sense, the process engineer has to externalize his specification (S PE ) by transcribing it in SysML language (red in Fig. 5 and Fig. 7). Once done, process solution space engineer prescribes S PE to SE problem space for validation. CISPI-AFW being a critical system, systems engineer must formally validate at least that S PE is compliant with dependability requirement S SE3 . However, systems engineering domain does not necessarily have the skills to formally perform this task. In this sense, a second iteration is on the expertise of dependability engineering solution space to formally validate S PE . This validation task is described in the next section.

B. Specification of the AFW control functions

Once the CISPI-AFW process validated, it remains to specify the control thereof.

As with process engineering domain, control functions specification requires a third iteration between SE problem space and automation engineering solution space (SS AE ). As addressed by [START_REF] Blochwitz | Functional mockup interface 2.0: The standard for tool independent exchange of simulation models[END_REF], automation as a specialist engineering has to broaden its traditional disciplinary domain in order to prescribe a control functions specification (S AE ) compliant with both process specification (S PE ) and system requirements (S SE ) according to entailment: K_SS AE , S SE , S PE  S AE [START_REF] Bouffaron | Integrative construct for Model-Based Human-System Integration: a case study[END_REF] This specification S AE consists in the definition of two control functions (Control_Water_Height) and one observation function (Observation_Height) (blue in Fig. 5). In the same way as for the validation of S PE , systems engineer draws again on the expertise of DE solution space to formally validate S AE . This validation task is also described in the next section.

C. Specification of the AFW logical architecture

In this stage, the CISPI-AFW process specification (S PE ) and the control functions specification (S AE ) are validated by systems engineering domain.

Taking into account dependability engineering specification S DE ("adding an observation function" see next section), SE problem space (PS SE ) must logically architecting process and control components in order to provide a logical architecture of CISPI-AFW system (LA SE ) according to the entailment: K_PS SE , S PE , S AE , S DE  LA SE [START_REF] Casada | Auxiliary feedwater system aging study[END_REF] This task requires to compromise between specialist and specialty specifications in order to prescribe LA SE . Indeed, systems engineering solutions has to check that the resulting architecture of logical architectural design process is compliant with systems requirements (S SE ). Thus, a last iteration with dependability engineering solution space is required to verify the specified architecture (LA SE ).

IV. CHECKING CO-SPECIFIED MODELS

Through the integrative system engineering processes, it is important to perform validation process [START_REF] Pyster | Guide to the Systems Engineering Body of Knowledge (SEBoK). Version 1.0[END_REF]. This is in order to check that any engineering products resulting from engineering processes are compliant with given system requirements models according to the predicate (4). This is particularly true with critical systems and dependability requirements where the use of formal techniques is strongly recommended [START_REF] Fanmuy | Requirements verification in the industry[END_REF] by safety standards.

The dependability requirement (S SE3 ) of our case-study is about the single failure criterion. Critical systems satisfy this criterion if their aim is ensured in the presence of any single component failure. CISPI-AFW system being used for short term during emergencies, only the single active failures must be taken into account, i.e. alignment, control and observation components. In other words, the system requirement S SE3 can be expressed as following: "if a failure is present on one of components, is there an alternative (another way) to achieve the system aim?" This led us to use reachability analysis method to check the compliance of the different specialist specification models with S SE3 . Indeed, the reachability analysis is a particular model checking method, which determines in a state-space (behaviour) if there is a way that respects a given property. Moreover, model checking methods allow producing a counterexample when a model fails to satisfy a desired property. "This faulty trace provides a priceless insight to understanding the real reason for the failure as well as important clues for fixing the problem" [START_REF] Cassandras | People In Control[END_REF].

To express the property, the language that we have chosen for formal checking is Computational Tree Logic (CTL) [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic: Springers[END_REF] because it is sufficient to formalize the requirements of our case study into properties. The tool used is UPPAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF] which is an integrated tool environment for modelling and model-checking timed automata.

A. Checking of CISPI-AFW process specification (S PE )

For model checking and reachability analysis purposes, the dependability requirement S SE3 has to be refined as a formal property. During the first iteration between system specialist engineering and dependability specialty engineering, the checking should determine whether the specified CISPI-AFW process (S PE ) is compliant with S SE3 . In other words, "if a failure is present on one of alignment functional components, is there a way to achieve the system aim?" This is represented by an observer (Fig. 6) with an initial state, followed one state representing the occurrence of a failure and followed by another state representing the system aim satisfaction. For each failure, the property to check is: "Is there a way to reach the system aim after the failure occurrence?" In the CTL, this property is written: E <> (failure i == 1) && (Observ.aim) [START_REF] Belles | Precursors to potential severe core damage accidents: 1998, A status report[END_REF] This property must be checked considering that each process function may have a failure. Two results are possible:

• The property is satisfied: this result allows concluding that CISPI-AFW process specification (S PE ) is compliant with system requirement (S SE3 ). • The property is not satisfied: this result allows concluding that CISPI-AFW process specification (S PE ) is not compliant with system requirement (S SE3 ). However, by analysing the counterexample returned by the model checker, dependability specialist is able to identify where the problem is.

Note that the checking of this property, allows also checking the compliance with systems requirements S SE1 and S SE2 . Indeed, from a point of view of the process, we assume that if the upstream flow of the SG tank is greater or equal to the downstream flow (20 L.mn -1 ), the system can ensure to maintain the level in the SG tank (Fig. 6). This is implemented in automaton diagram by the guard: flow_SG>=0 && (Alignment_Performed_way1 + Alignment_Performed_way2) where flow_SG = downstream_flow_SG -upstream_flow_SG (Fig. 9).

Thus, with SE problem space and DE solution space knowledge (K_PS SE , K_SS DE ) we are able to check the compliance of CISPI-AFW process specification (S PE ) with systems requirements (S SE ) according to the instance of entailment (4):

K_PS SE , S PE , K_SS DE  S SE [START_REF] Duco | Accidents nucléaires. Three Mile Island (Etats-Unis)[END_REF] To perform the checking, the specified behavior of functional process components must be modeled in UPPAAL. For this, the DE solution space has to translate behavior described by SE problem space in SysML statechart diagram into timed automata diagrams. Note that for reasons of size, the models presented in this paper do not represent the complete system. We focus for this study to the alignment function (Fig. 7 and Fig. 8) and to the formalization of the logical architecture (Fig. 9). Many studies deal with the passage from statechart to automata diagrams [START_REF] Knapp | Model checking timed UML state machines and collaborations[END_REF] [START_REF] Ji | Slicing hierarchical automata for model checking UML statecharts[END_REF]. However, to apply these rules, several iterations between dependability and systems engineers have been necessary for the interpretation of the semi-formal SysML statechart diagram. Thus, each SysML states are represented by automaton states. Note that the state Operational does not appears in the automaton but it includes in the states {Aligned, Misaligned, Aligning, Misaligning}. Moreover, in the automaton diagram the state Init_State is included in the state Init. Therefore we add two transitions to the state Init to initialize the alignment component either in state Aligned or in state Misaligned. Finally, the specified process architecture (red in Fig. 5) needs to be also modeled by an automaton (Fig. 9). This automaton represents the link between functional process components through water flows exchanged between them. Moreover, it allows updating water flow values at each evolution of the system. From these models, we are able by model checking to check that the property ( 8) is satisfied. Therefore we can affirm that the CISPI-AFW process specification S PE is compliant with systems requirements S SE according to predicate [START_REF] Faisandier | collection : Engineering and Architecing multidisicplinary systems, Sinergy'Com[END_REF].

B. Checking of CISPI-AFW control functions specification (S AE )

As for the checking of process specification (S PE ), the same approach can be applied to check the compliance of control function specification (S AE ) with systems requirements (S SE ) according to the instance of predicate (4): K_PS SE , S AE , K_SS DE  S SE [START_REF] Pyster | Guide to the Systems Engineering Body of Knowledge (SEBoK). Version 1.0[END_REF] The property [START_REF] Pyster | Guide to the Systems Engineering Body of Knowledge (SEBoK). Version 1.0[END_REF] to check is the same as previously, however the observer has to be redefined to take into account control and observation functions. Indeed, the satisfaction of S SE1 requires to observe and to control process in order to maintain level in SG tank. Thus, the observer (Fig. 10) consists on an initial state, followed of a state representing the occurrence of a failure, and followed by another state representing the system aim satisfaction if system is able to control and to observe the water level in the SG tank. Following the same method as previously, dependability engineer transforms statechart diagrams of control and observation functional components into automaton diagrams. Diagrams are not presented in this paper for space limitations. Once all models have been updated, dependability engineer checks the property (8) for each components failure. For functional control component failure, the single failure criterion is satisfied. Indeed, if a failure occurs on Control_1component, the Control_2 component on waterway 2 (with its associated process) components can ensure the CISPI-AFW system aim. As against, for functional observation component, if a failure occurs there are no other functional observation component to observe the water level in SG tank. Therefore, it is no longer possible to ensure the CISPI-AFW system aim. In this sense, DE solution space prescribes to systems engineering problem space that the AE specification (S AE ) is not compliant with systems requirements (S SE ). It prescribes also that another functional observation components is required to ensure the compliance of S AE with S SE . A new iteration between SE problem space and AE solution space is necessary to satisfy the predicate [START_REF] Dobre | Improving humansystem digital interaction for industrial system control: some systems engineering issues[END_REF].

V. CONCLUSION AND PERSPECTIVES

We would point out that UPPAAL is not yet integrated into our co-simulation framework but it could be in future works. This means that the verification/validation process remains humanbased (properties formalization, models transformation) with the aid of an automated checker. On contrary, it is important to emphasize the role of the co-specification process to aid also human checking modeller to ensure the correctness of its own dependability engineering models through several iterations with the system engineer in order to exhibit the right properties to the satisfaction of S SE . A future work will focus on the use of SCADE ® tool for checking with the advantage to automatically import IBM Rhapsody ® statechart diagrams.

Others ongoing works continue to experiment the powerful role of this co-specification framework based on the quest of knowledge from the systems engineering domain to others specialistengineering domains. For example, we are working with human-centred engineering (4) in order to satisfy operational requirements when field operators perform some control tasks but also with automation engineering in order to define a new kind of intelligent controller for CISPI-AFW [START_REF] Fliess | Model-free control[END_REF]. A future work will also improve this cospecification process to fully define a logical architecture and then a technical one. All these works, sometimes exploratory, are based on sound modelling rather than drawing for systems engineering, and aim in-fine to contribute to Human System Integration, both in operation and Design, as addressed by [START_REF] Boy | Unifying Human Centered Design and Systems Engineering for Human Systems Integration[END_REF].

Fig. 2 .

 2 Fig.2. Systems engineering and management paradigm[START_REF] Pyster | Guide to the Systems Engineering Body of Knowledge (SEBoK). Version 1.0[END_REF] [START_REF] Faisandier | collection : Engineering and Architecing multidisicplinary systems, Sinergy'Com[END_REF]

Fig. 3 .

 3 Fig. 3. Piping and instrumentation diagram of CISPI AFW-like process

Fig. 4 .

 4 Fig. 4. Distributed co-specification process

Fig. 5

 5 Fig. 5 Internal Block Diagram representing control functions specification (SAE) (blue) of AFW process (red).

w aterway_1:Water_Supply 1 O 1

 11 pe r a t i o ns Wat e r_T ransport at ion(fl ow _se t point :doubl... _Re gu lat i o n ( he ig ht _ m easu re :d ou b le, h e igh t _ se t p oin t :int ) :flo . . . _Re gu lat i o n ( he ig ht _ m easu re :d ou b le, h e igh t _ se t p oin t :int ) :flo . . . Ope r a t ions f a il u r e ( ) Height _Me asure(w ate r_he ight :dou... w ater_height hei ght_measure

Fig. 6 .

 6 Fig.6. Observer for process specification (SPE)

Fig. 7 .Fig. 8 .

 78 Fig. 7. SysML statechart diagram of alignment function (Water_Supply)

Fig. 9 .

 9 Fig. 9. Logical architecture of AFW process represented in timed automaton

Fig. 10 .

 10 Fig. 10. Observer for control specification (SAE)

  PS OE ∧SS OE , PS SE ∧SS SE , PS PE ∧SS PE, PS AE ∧SS AE PS DE ∧SS DE ) interoperating to satisfy the originating operational entailment:

TABLE I .

 I DRIVING CISPI-AFW SYSTEM REQUIREMENTS (S SE )

http://www.collegepublications.co.uk/systems/syt/

http://safetech.cran.univ-lorraine.fr/

"K_PS iE " and "K_SS jE " notations correspond respectively to the knowledge of problem space i (PS iE ) and solution space j (SS jE ) for the next sections

http://site.cosimate.com/