Maria Davie

G Fagherazzi
email: guy.fagherazzi@gustaveroussy.fr

G Gusto

F Romana Mancini

C Dow

K Rajaobelina

B Balkau

M.-C Boutron-Ruault

F Bonnet

Determinants of 20-year non-progression to Type 2 diabetes in women at very high risk: the E3N cohort study

What's new?

• Dietary habits play a major role in diabetes prevention in people at risk of Type 2 diabetes.

• The top characteristic found to be associated with not developing Type 2 diabetes was the limiting of foods typical of a Western diet [in the present study population, essentially processed meat, French fries, appetizers (olives, crackers, peanuts, almonds, hazelnuts, pistachios, walnuts), rice/pasta, potatoes, pulses, pizza/pies, canned fish, eggs, alcoholic beverages, cakes, mayonnaise, and butter/cream].

• The second most important characteristic was a high intake of antioxidant-rich foods (such as coffee, tea, fruit and vegetables, and chocolate).

• Our results provide evidence to aid the design of new intervention and prevention strategies in individuals at very high risk of Type 2 diabetes.

Aims To identify the most important determinants associated with not developing Type 2 diabetes in women considered to be at very high risk.

Methods Between 1995 and 2014, we followed 402 women from the E3N cohort study who were considered to be at very high risk of Type 2 diabetes based on the D.E.S.I.R. score. We then computed a classification and regression tree model to identify, among a large set of risk factors, the top risk factors associated with not having Type 2 diabetes at the end of the follow-up.

Results

During follow-up, 117 women (29%) were diagnosed with Type 2 diabetes, while 285 (71%) were still free of the disease in 2014. A low Western dietary pattern score was the top characteristic associated with not developing Type 2 diabetes, as only 20% of the women at very high risk in the E3N study with that characteristic developed Type 2 diabetes (compared with 29% overall). In women with a moderate or high Western dietary pattern score, the most important characteristic associated with not developing Type 2 diabetes was a high total dietary antioxidant capacity, as only 26% of these women ultimately developed Type 2 diabetes.

Introduction

Identifying key risk factors is key to Type 2 diabetes prevention. It is known that many cases of Type 2 diabetes are preventable through lifestyle modification, with population-attributable fractions related to factors such as diet, excess weight and physical activity of up to 91% [START_REF] Hu | Diet, Lifestyle, and the Risk of Type 2 Diabetes Mellitus in Women[END_REF]. Various Type 2 diabetes risk scores are increasingly used in screening and prevention campaigns all over the world, but many barriers still exist to the uptake of these tools by healthcare practitioners [START_REF] Dhippayom | How diabetes risk assessment tools are implemented in practice: a systematic review[END_REF]. Previous intervention studies have provided useful, but not optimal strategies to decrease Type 2 diabetes risk in high-risk populations [START_REF] Merlotti | Prevention of type 2 diabetes; a systematic review and meta-analysis of different intervention strategies[END_REF]. Insights into the key real-life determinants associated with Type 2 diabetes risk reduction in high-risk individuals would be useful for the design of better interventions. The objective of the present study was to identify the most discriminant factors associated with not developing Type 2 diabetes in women at very high risk of Type 2 diabetes, in the French E3N study.

Participants and methods

Study population

The E3N cohort study is an observational study that included 98 995 women aged 40-65 years at baseline in 1990; the study has already been extensively described elsewhere [START_REF] Fagherazzi | Functional gastrointestinal disorders and incidence of type 2 diabetes: Evidence from the E3N-EPIC cohort study[END_REF], and several Type 2 diabetes risk factors have been studied in this cohort [START_REF] Fagherazzi | The association of body shape trajectories over the life course with type 2 diabetes risk in adulthood: a group-based modeling approach[END_REF]. Type 2 diabetes cases in the E3N study were all validated using a well-defined algorithm that has been described elsewhere [START_REF] Mancini | Dietary antioxidant capacity and risk of type 2 diabetes in the large prospective E3N-EPIC cohort[END_REF]. The women in the E3N study did not participate in specific diabetes screening programmes during follow-up. Dietary information was collected in 1993 using a validated semi-quantitative food frequency questionnaire, that was adapted to the French meal pattern [START_REF] Van Liere | Relative validity and reproducibility of a French dietary history questionnaire[END_REF].

Accepted Article

In the present report, we included all participants who answered the 1995 questionnaire where waist circumference was first collected (n=69 001). We excluded those who had missing information in 1995 that would be used to calculate their D.E.S.I.R. diabetes risk score (waist circumference, hypertension, diabetes in the family; n=13 708), prevalent cases of Type 2 diabetes that occurred before 1995 (n=660), and those with missing information on dietary data (n =2883). Among the remaining 51 750 women, a total of 402 had a D.E.S.I.R. clinical score of 5 and were thus considered to be at a very high risk of Type 2 diabetes.

Type 2 diabetes risk assessment

The most commonly used risk score in France is still the FINDRISC score [START_REF] Meijnikman | Screening for type 2 diabetes mellitus in overweight and obese subjects made easy by the FINDRISC score[END_REF]; however, in the E3N study, the D.E.S.I.R. score has been shown to perform better than the FINDRISC score [START_REF] Balkau | Predicting diabetes: clinical, biological, and genetic approaches: data from the Epidemiological Study on the Insulin Resistance Syndrome (DESIR)[END_REF], therefore we used the clinical D.E.S.I.R. score to identify people at a very high risk of Type 2 diabetes; indeed, for the E3N study, the area under the receiver-operating characteristic curve for incident diabetes with this score was 0.82 [START_REF] Balkau | Predicting diabetes: clinical, biological, and genetic approaches: data from the Epidemiological Study on the Insulin Resistance Syndrome (DESIR)[END_REF]. The score ranges from 0 to 5, with a score of 5 indicating very high risk, which corresponds to an average absolute risk of Type 2 diabetes of 32% in the following 9 years.

The score for women is based on: waist circumference (70-79 cm: 1 point; 80-89 cm: 2 points; 90-99 cm: 3 points; ≥ 100 cm: 3 points), family history of diabetes (yes: 1 point) and hypertension (yes: 1 point).

Statistical analyses

Dietary patterns were derived from principal components analysis based on the main 57 predefined food groups from the dietary questionnaire, using the SAS 'Proc Factor' procedure (SAS Institute Inc., Cary, NC, USA; see Cottet et al. [START_REF] Cottet | Postmenopausal breast cancer risk and dietary patterns in the E3N-EPIC prospective cohort study[END_REF] for more details on the food groups). The first two patterns were characterized as: 1) 'Western: essentially processed meat, French fries, appetizers (olives, crackers, peanuts, almonds, hazelnuts, pistachios, walnuts), rice/pasta, potatoes, pulses, pizza/pies, canned fish, eggs, alcoholic beverages, cakes, mayonnaise and butter/cream and 2) 'prudent/Mediterranean: Accepted Article essentially vegetables, fruits, seafood, olive oil and sunflower oil. For each participant, we calculated the factor score for these two patterns by summing observed consumption from all food groups, weighted by the food group factor loadings. The factor score measures the level of adherence of a woman to the given dietary pattern. These scores were each then divided into three groups, with a low score corresponding to women with a score below the first tertile and a high score corresponding to those with a score above the third tertile.

The most discriminating factors associated with not developing Type 2 diabetes at the end of followup were identified using a classification and regression tree (CART) model using R software (ctree() function from the 'partykit' R package). This model explores the structure of data and develops easily visualized decision rules for predicting a categorical outcome (in the present study, diagnosis of Type 2 diabetes, yes/no). Each included variable is examined and the best categorization is made to maximize the sensitivity and specificity of the classification. The procedure is repeated until the stopping criterion (the predicted probability of diabetes does not depend on the non-included Variables with <5% missing data were imputed with the median (quantitative variables) or the mode (qualitative variables) of the study population, otherwise, an 'unknown' category was included in the analysis.

Results

Study characteristics

Among the 402 women considered to be at a very high risk of Type 2 diabetes in 1995, 117 (29%) were diagnosed with Type 2 diabetes during follow-up (1995-2014) and 285 (71%) were still free of

Accepted Article

the disease in 2014. Women at very high risk who did not develop Type 2 diabetes during follow-up were aged 75 years on average at the end of follow-up (Table 1).

Factors associated with not having diabetes in very high risk women

A low score for the Western dietary pattern was the top characteristic associated with not developing Type 2 diabetes in the women at a very high risk (Fig. 1). Indeed, only 20% of the women at very high risk in the E3N study with a low Western dietary pattern score developed Type 2 diabetes (compared with 29% overall). In women with a moderate or high Western dietary pattern score, the next most important characteristic associated with not developing Type 2 diabetes was total dietary antioxidant capacity. Only 26% of those with a moderate or high intake of antioxidant-rich foods developed Type 2 diabetes over the follow-up period.

Then, in order of decreasing impact were the following factors: extreme sleep duration (≤6 h or ≥9 h per night); birth weight; level of education; a prudent/Mediterranean dietary score; and physical activity. These factors had low discriminant capacities, however, and since some were based on small group sizes, they should be interpreted with caution. The two discriminating factors, therefore, were a low Western dietary pattern score (n=102) and higher total dietary antioxidant capacity (n=193).

Discussion

In the present study in 402 women at very high risk of developing Type 2 diabetes, we were able to isolate the top characteristics associated with not developing diabetes. Our results highlight the importance of diet in Type 2 diabetes prevention. Limiting adherence to a Western diet, characterized in the present study by processed meat, French fries, appetizers, rice/pasta, potatoes, pulses, pizza/pies, canned fish, eggs, alcoholic beverages, cakes, mayonnaise and butter/cream, appeared to be the most important determinant in our study population. In women who had a moderate to high Western dietary pattern score, total dietary antioxidant capacity, characterized by a high consumption

Accepted Article

of coffee, tea, fruit and vegetables and chocolate, and a moderate consumption of wine [START_REF] Mancini | Dietary antioxidant capacity and risk of type 2 diabetes in the large prospective E3N-EPIC cohort[END_REF], was the second most influential factor associated with not developing the disease. Interestingly, although the sample size was relatively small, we identified extreme sleep duration (≤6 h or ≥9 h per night) as the next most important factor discriminating women who developed Type 2 diabetes from those who did not.

The present study had some limitations, including the fact that the study population only included women. The study should therefore be replicated in men, even though findings related to dietary prevention in the literature have not been shown to be sex-specific. We were also unable to include genetic factors, but we did include family history of diabetes. Dietary information was only assessed at baseline, thus misclassification of exposure is possible as dietary habits may change over time. Because of the study design, measurement error is likely to be non-differential and would tend to attenuate the association.

The study also has several strengths. It included a population with a long follow-up and with information on many health determinants and lifestyle factors. We were able to isolate women at very high risk who were well characterized by a validated risk score that has been shown to perform well in the E3N study. Finally, we used a novel approach, modelling the top factors associated with not developing the disease in a real-life setting, which provides new perspectives from which to identify innovative factors to be included in prevention strategies.

In conclusion, we have shown that, among the main established or suspected diabetes risk factors in the literature, the top characteristic associated with not developing Type 2 diabetes despite being at very high risk was a healthy diet, characterized by both a limiting of Western dietary habits and a high intake of antioxidant-rich foods. The results favour the intensification of targeted interventions with regard to diet in very high risk populations. We also recommend that further intervention studies test new approaches based specifically on these findings.

Accepted Article

  variables) is reached. The variables we included in the model are either established risk factors or previously published factors associated with Type 2 diabetes risk in the E3N study, which are listed in the legend for Fig. 1. Variable importance was assessed by the mean decrease in accuracy obtained from 1500 tree iterations.

FIGURE 1

 1 FIGURE 1 Top characteristics* of women at very high risk of Type 2 diabetes who do not develop the

Table 1

 1 Baseline characteristics of participants at very high risk of Type 2 diabetes (D.E.S.I.R.

	clinical risk score = 5, E3N Cohort study; N=402)

Diagnosis of Type 2 diabetes at the end of follow-up (2014)

  n (%) and P values of chi-squared tests for categorical variables.Means (SD) and logistic regression tests for continuous variables.

	(FRAP, mmol/day) Light: <2.5 kg ≤ 6 h	33 (8.2) 72 (17.9)	11 (9.4) 19 (16.2)	22 (7.7) 53 (18.6)
	Body shape trajectory from 8 years to Medium: 2.5-4 kg 7-8 h	269 (66.9) 245 (61.0)	85 (72.6) 79 (67.5)	184 (64.6) 166 (58.2)	0.41
	D.E.S.I.R. clinical risk score components Waist circumference, cm Hypertension: yes, n (%) Family history of diabetes: yes, n (%) Other characteristics Age, years Smoker: yes, n (%) BMI, kg/m² Years of schooling Alcohol, g ethanol/day Energy intake, kcal/day Recreational physical activity, MET-h/week Deprivation index, FDep Western pattern adherence score Prudent pattern adherence score Dietary acid load score (PRAL) Total dietary antioxidant capacity Accepted Article 35-40 years (Fagherazzi et al. [5]) Trajectory 1 Trajectory 2 Trajectory 3 Trajectory 4 Trajectory 5 Trajectory 6 ABO blood group and rhesus O-O+ A+ A-B+ B-AB+ AB-Unknown Laterality Right-handed Left-handed or mixed Unknown Birth weight Accepted Article Heavy: > 4 kg Unknown Age at menarche <13 years ≥ 13 years Unknown Number of children, age at first full-term pregnancy Nulliparous One child, age < 30 years One child, age >30 years At least two children, age <30 years At least two children, age >30 years Unknown Breastfeeding Never Yes for at least one pregnancy Menopausal status Premenopause Postmenopause at <50 years Postmenopause at >50 years Number of hours of sleep per night ≥ 9 h Unknown Treated hypercholesterolaemia No Yes Intestinal transit Normal Diarrhoea Constipation Alternating diarrhoea constipation Unknown Marital status Single In couple Accepted Article Unknown	All (n=402) 96.9 (7.40) 402 (100.0) 402 (100.0) 55.7 (6.65) 23 (5.7) 30.5 (3.96) 13.2 (3.35) 11.6 (16.37) 2245.8 (599.44) 21.4 (24.48) -0.1 (0.96) 0.3 (1.11) 0.3 (1.07) -2.5 (20.30) 13.0 (6.11) 10 (2.5) 135 (33.6) 110 (27.4) 11 (2.6) 114 (28.4) 22 (5.5) 127 (31.6) 26 (6.5) 23 (5.7) 131 (32.6) 6 (1.5) 44 (10.9) 5 (1.2) 8 (2.0) 32 (8.0) 353 (87.8) 36 (9.0) 13 (3.2) 67 (16.7) 33 (8.2) 213 (53.0) 176 (43.8) 13 (3.2) 57 (14.2) 40 (10.0) 12 (3.0) 261 (64.8) 30 (7.5) 2 (0.5) 180 (44.8) 222 (55.2) 121 (30.1) 153 (38.1) 128 (31.8) 74 (18.4) 11 (2.7) 342 (85.1) 60 (14.9) 282 (70.1) 24 (6.0) 39 (9.7) 47 (11.7) 10 (2.5) 85 (21.1) 295 (73.4) 22 (5.5)	Yes (n=117) 97.3 (6.58) 117 (29.1) 117 (29.1) 54.5 (6.32) 7 (6.0) 31.1 (3.69) 13.4 (3.18) 11.4 (14.72) 2247.67 (548.10) 20.2 (18.99) -0.1 (0.99) 0.4 (1.10) 0.2 (1.11) 0.1 (20.54) 12.8 (6.13) 2 (1.7) 45 (38.5) 31 (26.5) 1 (0.9) 34 (29.1) 4 (3.3) 41 (35.0) 8 (6.8) 6 (5.1) 38 (32.5) 1 (0.9) 10 (8.6) 2 (1.7) 3 (2.6) 8 (6.8) 102 (87.1) 12 (10.3) 3 (2.6) 16 (13.7) 5 (4.3) 61 (52.1) 53 (45.3) 3 (2.6) 15 (12.8) 9 (7.7) 6 (5.1) 79 (67.5) 7 (6.0) 1 (0.9) 50 (42.7) 67 (57.3) 44 (37.6) 37 (31.6) 36 (30.8) 18 (15.4) 1 (0.9) 97 (82.9) 20 (17.1) 90 (76.9) 6 (5.2) 6 (5.2) 13 (11.1) 2 (1.7) 27 (23.1) 86 (73.5) 4 (3.4)	No (n=285) 96.7 (7.71) 285 (70.9) 285 (70.9) 56.3 (6.72) 16 (5.6) 30.3 (4.04) 13.1 (3.42) 11.7 (17.02) 2245.0 (620.21) 21.9 (26.39) -0.1 (0.95) 0.2 (1.11) 0.3 (1.05) -3.5 (20.14) 13.1 (6.11) 8 (2.8) 90 (31.6) 79 (27.7) 10 (3.5) 80 (28.1) 18 (6.3) 86 (30.2) 18 (6.3) 17 (6.0) 93 (32.5) 5 (1.8) 34 (11.9) 3 (1.1) 5 (1.8) 24 (8.4) 251 (88.1) 24 (8.4) 10 (3.5) 51 (17.9) 28 (9.8) 152 (53.3) 123 (43.2) 10 (3.5) 42 (14.6) 31 (10.9) 6 (2.1) 182 (63.9) 23 (8.1) 1 (0.4) 130 (45.6) 155 (54.4) 77 (27.0) 116 (40.7) 92 (32.3) 56 (19.7) 10 (3.5) 245 (86.0) 40 (14.0) 192 (67.4) 18 (6.3) 33 (11.6) 34 (11.9) 8 (2.8) 58 (20.4) 209 (73.3) 18 (6.3)	P 0.97 --0.52 0.98 0.49 0.15 0.02 0.12 0.62 0.91 0.83 0.48 0.05 0.59 0.92 0.58 0.44 0.75 0.38 0.60 0.08 0.34 0.43 0.18

*FDep, xxx; PRAL, xxx.

Acknowledgements

The authors are grateful to all participants for providing the data used in the E3N cohort Study. G.F. takes full responsibility for the work as a whole, including the study design, access to data, and the decision to submit and publish the manuscript.

Funding sources

The E3N cohort is being carried out with the financial support of the Mutuelle Générale de l'Education Nationale, the European Community, French League against Cancer, Gustave Roussy,

Accepted Article

and the French Institute of Health and Medical Research. The present study was also supported by the French Research Agency (Agence Nationale de la Recherche) via an Investissement d'Avenir (investment for the future) grant (ANR-10-COHO-0006) that supports the E4N study, and the IDEX Paris Saclay (Nutriperso project).

Conflict of interest

None declared.


Vincent Leildé

Vincent Ribaud
email: vincent.ribaud@univ-brest.fr

Ciprian Teodorov

Philippe Dhaussy

A Problem-Oriented Approach to Critical System Design and Diagnosis Support

Keywords: Problem Oriented Method, Diagnosis, Security Patterns

For critical software applications, dependability and safety are required features that should respect security principles. To cope with these constraints, the design activity should use new methods that foster knowledge sharing and reuse, in particular security problems and their solutions. In this paper, we present a problem-oriented method that follows a step-wise building of the solution. Problems are reused using various mechanisms, and a solution is conceived, verified and diagnosed. We illustrate the approach on the problem of building a secure SCADA architecture.

Introduction

Critical software systems are pervading our daily lives and sustaining in many different domains (transportation, avionics, health-care or information management). To improve their dependability and safety, regardless their complexity, critical software design should be carried out with respect to security principles.

Over time, knowledge about security has been captured into patterns, a packaged solution to a recurrent problem in a specific context [START_REF]Design patterns: elements of reusable object-oriented software[END_REF]. A security pattern is a reusable solution for a recurring security problem. It is used to analyze, construct and evaluate secure systems [START_REF] Fernandez | Designing Secure SCADA Systems Using Security Patterns[END_REF]. It provides detailed guidelines about the application of an architectural solution for a particular problem of security. Several research work address security issues using security patterns, and we exploit as a case study the approach set by F. Obeid [START_REF] Obeid | Validation Formelle d Implantation de Patrons de Securite[END_REF]. The author secures SCADA systems through the composition of the SCADA architecture with security patterns. Safety and security requirements of the composition are then validated through model-checking.

Our research work is focused on methods and tools intended to ease this verification activity, especially the diagnosis activities. Briefly stated, our approach aims to answer diagnosis issues with a general diagnosis ontology [START_REF] Leilde | A diagnosis framework for critical systems verification[END_REF], a management system to perform and enable verification and diagnosis activities [START_REF] Leilde | An Organizing System to Perform and Enable Verification and Diagnosis Activities[END_REF], and a domain-oriented method [START_REF] Leilde | Domain-oriented Verification Management[END_REF].

Verification at the early stages of the engineering process prevents expensive defects from occurring in the final product. A software organization that manages quality should have a corporate infrastructure that links together and transcends single projects by capitalizing on successes and learning from failures [START_REF] Basili | Improve software quality by reusing knowledge and experience[END_REF]. These tasks require to manage past diagnosis experiences (gathering a set of heterogeneous artifacts) and to correlate discovered abnormalities with experiences. This can be achieved with a knowledge based system together with a well-defined method. This paper we present how our method and tools support the application of security patterns as set in the case study mentioned above.

To some extent, the method we use in this paper borrows the Twin Peaks idea of performing round trips between problem and solution spaces for improving the verification process [START_REF] Hall | Relating software requirements and architectures using problem frames[END_REF]. It should help the engineer to bring closer highlevel information and abnormalities observations. It focuses on a progressive constitution of a knowledge base, containing both problems and solutions, that can be reused. Solutions are packaging formal designs and verification runs, and problems are formalized with a set of properties together with a structure of various solutions.

Section 2 overviews the method. In section 3, we shows the application of the method to secure an application using security patterns. Section 4 discusses how problem cases is a support to design and diagnosis, and section 5 concludes this study.

Overview of the Method

The method focuses on a progressive understanding of the problem. First, this should help the designer to find rapidly a solution to his problem, by decomposing the problem in smaller subproblems, and reusing existing solutions. Second, it should help the verifier to understand the root causes of abnormalities for a selected solution, by providing diagnosis task with relevant information. This section describes the process used to formalize problems and the different steps of the process flow.

The step-wise method is presented by the activity diagram in figure 1. The method is reiterated until a satisfactory solution is achieved.

To illustrate the method, let us consider the following example. Suppose a board game with one board and two players. The board asks an infinite number of questions to each player, in a non deterministic manner. If the player has a right answer, it increases its score by one point, otherwise no point is awarded. The match ends when a player reaches 3 points. This model is not fair because in some case, the board can ask more questions to one player rather the other.

(1) The problem is formulated as a set of properties and constraints (architectural, technical choices). The structure of formulated problem conforms to the conceptual model of figure 5 and is presented in section 4.1. For instance, "at the end of the game, each player has played the same number of times". [START_REF] Ball | From symptom to cause: localizing errors in counterexample traces[END_REF] The problem is decomposed into subproblems, either known problems -called problem cases -selected from a knowledge base, or unknown situations. For in-Fig. 1: Method steps stance, we may decide that "a turn mechanism is used". (3) When the need for a concrete view occurs, we move towards the solution space. The potential solution elements are organized. For instance, we may decide that "the turn problem case is introduced into the current solution". ( 4) We consider how to combine the selected problem cases together. This solution may be either composed ( 5) with other problem cases, applied as a pattern [START_REF] Fernandez | Designing Secure SCADA Systems Using Security Patterns[END_REF], or problem cases may be merged (7)3 . ( 8) At this point, we built a part of the expected solution; hence we are able to start a verification cycle. When abnormalities are observed, it triggers a diagnosis process. Verification results are stored in the knowledge base. (9) Diagnosis process is performed, problem cases can be used to enhance this process. The design is corrected, and the verification endeavor repeated. In some cases, the selected problem cases do not suit, hence we have to backtrack and rework the problem combination, and it might be useful to keep track of this failed attempt.

This step-wide method is repeated several times while useful components can be combined. The engineer is left with a reduced problem for which no known solutions exist and where a classical design and verification activity has to be achieved.

The method space is divided in two parts, the problem space, related to the problem elaboration, and the solution space, related to design and verifying the solution. Whereas the problem elaboration produces specification to the solution design, the resulting solution produces expanded specifications (from design choices) to the problem space. This is similar to the Twin Peak model [START_REF] Hall | Relating software requirements and architectures using problem frames[END_REF], a software iterative development process that focuses on the combination of problem structures and solution structures.

The method applicability is illustrated in the next section onto a critical system design. Let see now how to use the method on the securized SCADA case study.

Application

We reuse a case study extracted from the work of [START_REF] Obeid | Validation Formelle d Implantation de Patrons de Securite[END_REF]. The approach aims at securing architectures by applying security patterns together with a security policy. The approach has been demonstrated on several kinds of architectures.

Problem Formalization

The figure 2 represents an unsecured architecture composed of four entities, a global controller (GC ), two local controllers (LC1 and LC2 ), and a communication network (NETWORK ) that links together GC, LC1 and LC2. The local controller LC1 owns the resource RES1, while the local controller LC2 owns the resource RES2. Some READ and WRITE operations for accessing a resource are granted for an entity according to its role. Different roles are ADMIN (READ and WRITE access to RES1 and RES2 ), GCOWNER (READ access to RES1 and RES2 ), LC1OWNER (READ and WRITE access to LC1 ) and LC2OWNER (READ and WRITE access to LC2 ). This architecture can be seen at a higher abstraction level, as a set of NET and ACCESS components. A NET is an abstraction of a NETWORK entity that forwards messages to other components. An ACCESS component is an abstraction of LC1, LC2 and GC entities protect access to resources. An ACCESS component behaves as depicted in figure 2.

In this figure, the transitions between states bear the Event-Condition-Action expression represented as Si

{Event}[Condition]Action

-----------------→ Sj. Si and Sj are states, the arrows stand for transitions, labeled with events that cause the transitions to be triggered. A condition is a boolean expression, and an action represents some variable assignments or events sending. When an event occurs, the guard condition is evaluated and the transition is fired only if the condition is true, performing the action.

Each ACCESS component begins with an Idle state, where it waits for a request (req). If a request is received and if the request is addressed to the component (req.target==id ), the resource is accessed (Access) and the component replies (sending). When the request is not for the component (req.target!=id ), the component forwards the request to other connected components through the network. In our case, when the environment ENV wants to access to the architecture, it sends a message to GC together with an indication about the target (either RES1 or RES2 ), and the corresponding operation (READ or WRITE ). GC receives requests from the environment(ENV ). GC forwards the request to LC1 or LC2 through the NETWORK. LC1 or LC2 receives and processes the request from the NETWORK, and replies.

The architecture: a global controller(GC), a network, and local controllers(LC1, LC2).

The behavior of GC, LC1 and LC2.

Fig. 2: Description of the application extracted from [START_REF] Obeid | Validation Formelle d Implantation de Patrons de Securite[END_REF] To guarantee integrity and confidentiality constraints regarding LC1 and LC2, security mechanisms are applied. These security mechanisms must ensure: -PRT1Init, when a component sends a request that respects the access rights for accessing a resource, the access must be realized. -PRT2Init, any resource access must respect the access rights.

Domain Description

We suppose that a knowledge base has been built from previous experiences. The base contains a set of problem cases structured by security patterns. The author [START_REF] Obeid | Validation Formelle d Implantation de Patrons de Securite[END_REF] defines a security pattern with a list of properties, its name, its functionalities and a description of the problem it is intended to solve, a static and a dynamic structure of the solution, formal properties and some examples of use.

The authorization (AUTH ) pattern implements security measures for a resource (read, write, execution). AUTH pattern ensures that a resource access by an entity Ent, for an operation OpRes is granted. When an access is authorized, the access is realized, otherwise counter-measures are triggered.

The structure of this problem case is depicted in figure 3. Function has-Right (e: Ent, opRes: OpRes):Boolean returns true if the entity e can perform the opRes.oper operation on the opRes.res resource (or said differently, if the resource is not protected for this operation or if the entity has an explicit permission). In addition, the pattern is described with two formal properties. PRTAuth1, when an access request respects the access rights, the resource access is finally realized. PRTAuth2, a resource access must respect access rights.

Problem Decomposition

Following our method, the problem is decomposed into smaller subproblems, so that a global solution emerges from a combination of smaller solutions. The structure of the two initial properties PRT1Init and PRT2Init, that have to be fulfilled, is similar to the structure of PRTAuth1 and PRTAuth2. The AUTH problem case is retrieved for reused.

Solution Design

Then the solution is realized by combining the initial problem with the AUTH problem case. The combination strategy can be a composition of self-contained and separated components, an application of patterns, or a specialization of a problem case and its solutions.

Because the AUTH problem case is structured as a pattern, the most appropriate combination mechanism is the pattern application. It is realized in two steps, first, verification of the initial conditions, and second, the application of transformations. At the first step, some hypotheses have to be fulfilled. For instance one must identify an Access state in the design, where the authorization mechanism has to be introduced. In the case study, the following hypotheses must be respected: -Hypothesis 1, the reception of a message is carried out by reading the input fifo. This happen in a transition from the Idle state to the Receive state; Hypothesis 2, the sending of a message is carried out by a write into the output fifo, along a transition from the Sending state to the Idle state; -Hypothesis 3, each transition to the Compute state has a source Receive state; -Hypothesis 4, the Access state has only one source state, Compute.

If these hypotheses are respected, the second step produces a solution according to the pattern definition, as depicted by figure 4. The transformation rules are not presented in the article, but can be found in [START_REF] Obeid | Validation Formelle d Implantation de Patrons de Securite[END_REF].

The architecture is secured using the authorization pattern. This finite state machine represents the secured behavior of and LC2.

Solution Verification and Diagnosis

Verification can be done using several techniques such as static analysis, theorem proving, or model checking. The later is a formal technique that, given a formal model of the system and a set of properties, explores all possible system states in a brute-force manner [START_REF] Baier | Principles of model checking[END_REF]. If abnormalities are detected in the design, counter examples are produced, i.e a trace from the initial state to an unexpected situation. Then diagnosis is triggered based on the observations of such traces. We use a model checker to check exhaustively the properties for this model. The verification validates a solution for the problem, but note that other solutions may also exists for this problem.

Iterating Through Problem and Solution Spaces

Assume that a new security policy is required for the same architecture, some counter-measures must be triggered in case of a security violation. According to the method, existing problem cases can be retrieved. The checkpoint pattern (CHP ) allows to apply specific regulations, and defines properties that are closed to the new security constraints. The pattern is retrieved, and applied by taking into account the (AUTH ) solution found previously, thus AUTH is now a part of the problem.

The CHP problem case has been applied, and the solution verified. The resulting solution gathers two solutions, the checkpoint solution and the authorization solution. It can be retained in a knowledge base as a new reusable component named for instance SECACCESS.

We suppose that the architecture must evolves because a new local controller LC3 is required. The new problem can rapidly be solved if one reuse the SE-CACCESS component.

System Design and Diagnosis Support

In this section we will present the conceptual model that sustains the approach applied on the case study, as well as tools we built [START_REF] Leilde | An Organizing System to Perform and Enable Verification and Diagnosis Activities[END_REF]. The model has two parts, the former related to the reuse of verified designs 4.1, and the latter related to diagnosis management and support 4.2. Problem cases are the links between both parts.

Problem cases for System Design

Decomposing a complex problem into smaller problems that are more manageable and easier to solve, is a natural way to reduce the design complexity. When past experiences are available, this method can be improved by analogical reasoning, i.e. reusing past known problems. At the same time, it raises the issue of the way to capture different problems.

A problem is reified as a problem case. A conceptual model is provided as an illustration (figure 5). A problem case is either atomic or a combination of subproblem cases. An atomic problem case is made of problem elements. A problem case can be of different kinds, a component, a pattern, or a solution. Each problem case gathers a set of problem elements that depends on its kind. For example, states, ports and functions are all problem elements. Some concepts are analogous to the problem frame approach [START_REF] Jackson | Problem frames: analysing and structuring software development problems[END_REF], a problem case is similar to a domain, and problem elements are closed to phenomena.

To be reused, problem cases are combined together. Combination can be of different natures, for instance composition, application and specification inheritance. Composition, is the most easy way for reusing a problem case, as it only requires few adaptations. When the component is too generic, the counterpart is a lack of efficiency. Besides, the application of a pattern generally requires Fig. 5: Problem conceptual model manual implementations. A pattern is a well-defined guidance for a recurring problem, but the solution must be adapted to the context. With specification inheritance, only specifications are reused, and the solution must be fully implemented. Thus, problem cases impact the amount of reuse.

Diagnosis Support

Many researchers [START_REF] Ball | From symptom to cause: localizing errors in counterexample traces[END_REF][START_REF] Cleve | Locating causes of program failures[END_REF][START_REF] Groce | What went wrong: Explaining counterexamples[END_REF][START_REF] Clarke | The localization reduction and counterexample-guided abstraction refinement[END_REF] divide the diagnosis in two main tasks: isolation (localization) and causal analysis. Isolation extracts the subset of elements, part of models, that needs to be corrected. Causal analysis associates causes to the observed abnormalities. These tasks are burden, particularly due to the huge amount of unrelated information the engineer needs to understand and correlate.The semantics gap is an example that is a discrepancy between the formalisms used during design and low-level traces obtained during verification. Reasoning on problems afford the advantage of raising the level of abstraction to a non technical level.

In [START_REF] Leilde | A diagnosis framework for critical systems verification[END_REF], we proposed a formalization of diagnosis. Based on the formalization, a diagnosis can be captured together with problem cases, allowing design or model causes inference (figure 5). Diagnosis is made of (diagnosis elements), either propositional objects or associations. Propositional objects are descriptions about the problem parts (states, traces, properties, problem cases ...). Some descriptions are symptoms of errors (counter-examples). A propositional object is linked to other propositional objects by means of various natures of associations (causal, nature, evolution). A diagnosis may be curative if it aims to find the cause of an error. In our method, a cause can be a model cause or a design cause. A model cause happens when the selected problem is valid (for instance the AUTH pattern is the good choice), but its implementation is not valid (for instance the AUTH pattern is badly implemented). It locates the cause in the application of the pattern. Conversely, a design cause happens when the combination of the problem is valid (for instance the AUTH pattern is correctly implemented), and the combined problem case is not appropriated, or incomplete.

Conclusion

Designing a solution for a given security problem, and diagnosing possible faults in the proposed solution, are tedious tasks. It is mainly due to poorly understood problem, and poorly managed information, that results in a lack of diagnosis support and solution reuse. Our hypothesis is that a method is required for analyzing the current problem, storing relevant information, and reusing known solutions as much as possible. This work paves the way to the elaboration of a verification management tool.

Fig. 3 :

 3 Fig. 3: Authorization Pattern Structure

P

  RT Auth1 : ∀c ∈ Auth, ∀e ∈ Ent, ∀opRes ∈ OpRes, [evtV erif y(c, AccReq(e, opRes)) ∧ right(c, e, opRes) ⇒ ♦evtAccess(c, e, opRes)] P RT Auth2 : ∀c ∈ Auth, ∀e ∈ Ent, ∀opRes ∈ OpRes, [evtAccess(c, e, opRes) ⇒ right(c, e, opRes)].

Fig. 4 :

 4 Fig. 4: Description of the secured application

Each kind of combination is represented with a particular arrow shape.


Vincent Leildé

Vincent Ribaud
email: vincent.ribaud@univ-brest.fr

Ciprian Teodorov

Philippe Dhaussy

Domain-oriented Verification Management

Keywords: Organizing System, Diagnosis, Problem Oriented Method

Basili stated twenty years ago that a software organization that manages quality should have a corporate infrastructure that links together and transcends the single projects by capitalizing on successes and learning from failures. For critical systems design, the verification tasks play a crucial role; when an unexpected situation is detected, the engineer analyzes the cause, performing a diagnosis activity. To improve the quality of the design, diagnosis information have to be managed through a well-defined method and with a suitable system. In this paper we present how a Verification Organizing System together with a problem-oriented method could achieve these issues. The key aspect of the approach is to follow a step-wise building of the solution, reusing known problems that are relevant for the system under study.

Introduction

D. Bjorner defines software engineering as a triptych: from descriptions of the application domain we construct prescriptions of the requirements; and from prescriptions of the requirements we design the software, i.e. construct specifications of software [START_REF] Bjrner | Software Engineering 3[END_REF]. Our area of interest is software formal verification, especially with a model-checking approach. We start the model-checking process with a model of the system under consideration and a formal characterization of the property to be checked, i.e. two legs of the triptych : design and requirements. Then we run the model checker to check the validity of the property in the system model. When property is violated, the model checker provides us with a counterexample (a witness trace) that triggers a diagnosis activity to analyze the trace and to outline the error causes. Consequently, the system model is corrected and a new process cycle -verification, diagnosis, and correction -is repeated. The third leg is a domain-oriented verification defined as a process by which information used in verifying software systems is identified, captured, and organized with the purpose of making it reusable when modeling and verifying new systems.

Our research work is focused on methods and tools intended to ease the verification process, especially the diagnosis activities. Generally speaking, research addressing model-checking and diagnosis issues [START_REF] Alrajeh | Automated support for diagnosis and repair[END_REF][START_REF] Ball | From symptom to cause: localizing errors in counterexample traces[END_REF][START_REF] Bertoli | A symbolic model checking framework for safety analysis, diagnosis, and synthesis[END_REF][START_REF] Gromov | Testing and model-checking techniques for diagnosis[END_REF][START_REF] Holzmann | The Theory and Practice of A Formal Method: NewCoRe[END_REF] are faced with the same difficulties. First, diagnosing the cause of abnormalities suffers from too detailed observations. It is hard, for instance, to localize the relevant parts in a detailed source-level trace when we look for the reasons a verification run failed [START_REF] Groce | What went wrong: Explaining counterexamples[END_REF]. Some techniques focus on linking low level information with more abstract information, like model-based diagnosis [START_REF] Reiter | A theory of diagnosis from first principles[END_REF], or case-based reasoning [START_REF] Agnar | Case-Based Reasoning: Foundational Issues, Methodological Variations, and System Approaches[END_REF]. Second, these techniques require a set of data that is not always available. In addition to the verification steps, the entire verification should be planned, administered, and organized. This is called verification organization by C. Baier and J.-P. Katoen [START_REF] Baier | Principles of model checking[END_REF]. During the engineering process, heterogeneous artifacts are produced, including requirements, system models, properties, runs, or diagnoses. As stated by T. C. Ruys [START_REF] Ruys | Managing the verification trajectory[END_REF], they are poorly managed and controlled. As a result, the expertise is poorly acquired by the verification engineers, and cannot be used for the above techniques. Third, verification at the early stages of the engineering process prevents expensive defects from occurring in the final product. A software organization that manages quality should have a corporate infrastructure that links together and transcends the single projects by capitalizing on successes and learning from failures [START_REF] Basili | Improve software quality by reusing knowledge and experience[END_REF]. These tasks require to manage past diagnosis experiences (gathering a set of heterogeneous artifacts) and to correlate discovered abnormalities with experiences. This can be achieved with a knowledge based system together with a well-defined method.

Briefly stated, our approach aims to answer the issues above with a general diagnosis ontology [START_REF] Leilde | A diagnosis framework for critical systems verification[END_REF], a Verification Organizing System [START_REF] Leilde | An Organizing System to Perform and Enable Verification and Diagnosis Activities[END_REF], and a domainoriented method, the latter being the subject of this paper. Some relevant parts of the ontology will be presented in section 3.1. The organizing system -an intentionally arranged collection of resources and the interactions they support [START_REF] Glushko | Foundations for Organizing Systems. The Discipline of Organizing[END_REF] -makes easier the management of verification objects and supports reasoning interactions that facilitates diagnosis decisions; some features related to the method are drafted in section 5.1.

The method we propose in this paper relies on the idea of performing round trips between problem and solution spaces for improving the verification process. It should help the engineer to bring closer high-level information and abnormalities observations. It focuses on a progressive constitution of a knowledge base, containing both problems and solutions, that can be reused. Solutions are packaging formal designs and verification runs, and problems are formalized with a set of properties together with a structure of various solutions.

Section 2 overviews background and related work. In section 3, we present the proposed method, its steps and a straightforward example. Section 4 shows the application of the method on the mutual exclusion problem. Section 5 discusses the knowledge base and its services, and section 6 concludes this study.

Background and Related Work

A. Newell and H. A. Simon introduced in [START_REF] Newell | Human problem solving[END_REF] the problem-space hypothesis: the fundamental organization unit of all human goal-oriented activity is the problem space. M. Jackson introduced the concept of problem frame for presenting, classifying and understanding software development problems. Problem frames structure the analysis of the world in which the problem is located -the problem domain -and describe what is there and what effects one would like a system located therein to achieve [START_REF] Hall | Relating software requirements and architectures using problem frames[END_REF]. A problem frame is defined in terms of its context and the characteristics of its domains, interfaces and requirements [START_REF] Jackson | Problem frames: analysing and structuring software development problems[END_REF]. The problem frame approach allows engineers to build domain expertise and let practitioners gain experience from this knowledge base. POSE (Problem Oriented Software Engineering) [START_REF] Hall | Problem Oriented Software Engineering: A design-theoretic framework for software engineering[END_REF] is an extension and generalization of problem frames. It is a representation and step-wise transformation of software problems to progress towards the solution. Software architecture [START_REF]Pattern-oriented software architecture: a system of patterns[END_REF], as well as development framework and design patterns [START_REF]Design patterns: elements of reusable object-oriented software[END_REF] have same goals of knowledge construction, share and reuse. This kind of knowledge is generally attributed to the solution space. Compelling arguments justify an early understanding of stakeholders' requirements (focus on the problem). Equally compelling arguments justify an early construction of a suitable software-system architecture (focus on the solution).

Life-cycle model evolved from waterfall models to spiral models. Fine-grained spiral models are used by agile methods. The cornerstone of these processes is that developers craft a system's requirements and its architecture concurrently, and interleave their development [START_REF] Swartout | On the inevitable intertwining of specification and implementation[END_REF]. Researchers from the Open University proposed an adaptation of the spiral life-cycle model, called the Twin Peaks Model to emphasize the equal status given to requirements and architecture [START_REF] Hall | Relating software requirements and architectures using problem frames[END_REF]. The proposed model of software development is an iterative process during which problem structures and solution structures are detailed and enriched. In this context, the Open University team sees the use of architectural support as aiding the focus on the essential design requirements of the problem by allowing design concerns to be treated more abstractly and to be combined with behavioural requirements [START_REF] Hall | Relating software requirements and architectures using problem frames[END_REF]. They extended problem frames towards this end.

In case of inadequate or unknown solution, problem-oriented approaches facilitate diagnosis. A well-known artificial intelligence approach, CBR (Case Based Reasoning), reduces the diagnosis effort by remembering a similar situation and by reusing information and knowledge of that situation. It proposes a method in four steps, retrieve, reuse, refine and retain. To some extent, the method we propose in this paper borrows the Twin Peaks idea of performing round trips between problem and solution spaces for leveraging diagnoses.

Method

The method focuses on a progressive understanding of the problem. First, this should help the designer to find rapidly a solution to his problem, by decomposing the problem in smaller subproblems, and reusing existing solutions. Second, it should help the verifier to understand the root causes of abnormalities for a selected solution, by feeding diagnosis task with relevant information. This section describes formalization of problems, and the different steps of the flow.

Problem Formalization

According to V. Venkatasubramanian [START_REF] Venkatasubramanian | A review of process fault detection and diagnosis[END_REF], Abnormal Event Management, a key component of supervisory control, involves the timely detection of an abnormal event, diagnosing its causal origins and then taking appropriate supervisory control decisions and actions to bring the process back to a normal, safe, operating state. Generally speaking, we have three main tasks; fault detection, diagnosis, and correction. Let see the tasks in a model-checking approach. Fault detection establishes that a system run raises an abnormal event: the exhaustive exploration encounters a state that violates the property under consideration, the model checker provides a counterexample, an execution path that leads from the initial system state to the violating state. Many researchers [START_REF] Ball | From symptom to cause: localizing errors in counterexample traces[END_REF][START_REF] Cleve | Locating causes of program failures[END_REF][START_REF] Groce | What went wrong: Explaining counterexamples[END_REF][START_REF] Clarke | The localization reduction and counterexample-guided abstraction refinement[END_REF] divide the diagnosis in two main tasks: isolation (localization) and causal analysis. Isolation extracts the subset of model parts that needs to be corrected. Causal analysis associates causes to the observed abnormalities. These are generally burden tasks, particularly due to a huge amount of unrelated information the engineer needs to understand and correlate. One example, known as the semantic gap, is the discrepancy between the formalisms used during design and low-level traces obtained during verification.

Reasoning on problem cases afford the advantage of raising the level of abstraction to a non technical level. A conceptual model of the domain is given in figure 1. A problem is reified under a problem case. A problem case is composed of subproblem cases, that are made of propositional objects. Propositional objects are descriptions about the system components, such as processes, states, runs, traces or properties. Some propositional objects may be defined as checkpoints, key elements to be observed during the diagnosis activity. A propositional object is linked to other propositional objects by means of associations of different kinds: causal, nature, evolution. In the same way, problem cases are connected together with associations, through hooks exposing connection points. A set of associations between problem cases is an hypothesis of combination. This hypothesis may causes abnormalities, for instance when a problem case property is violated, and thus reveals an issue. The issue organizes results in a diagnosis. Finally problem cases may be reused as solutions for further designs.

We find analogous concepts in the problem frame approach, a problem case is similar to a domain, and propositional objects are closed to phenomena.

Illustration

To illustrate how the conceptual model is used, let us consider the following example. Suppose a board game with one board and two players. The board asks an infinite number of questions to each player, in a non deterministic manner. A player gives either a right answer, that increases its score by one point, or a wrong answer, and no point is awarded. The match ends when a player reaches 3 points. The behavior of the solution is presented in figure 2. -----------------→ Sj. Si and Sj are states, arrows stand for transitions, labeled with events that causes the transition to be triggered. A condition is a boolean expression, and an action represents some variable assignments or events sending. When an event occurs, the guard condition is evaluated and the transition is taken only if the condition is true, performing the action.

The model is made of three processes, player one, player two and a board, and two variables, score one (s1) and score two (s2). Players share the same behavior. They wait for a question from the board (event p1 is a question from the board to player one, and event p2 is a question from the board to player two). Each player replies to the board. The response can be right (event r1 or r2) or wrong (event w1 or w2). When the board is in the idle state (Bi), it asks a question, either to player one or player two (respectively by sending events p1 or p2), if and only if none of the players have a score equals to 3 (c1 condition is false). If a question is asked to player one, the board goes in state BP1, and if a question is asked to player two, the board goes in state BP2. In these states, the board waits for a response, either a right response (event r1 or r2) and in that case the score is incremented, or a wrong response (event w1 or w2). When one of the players reaches a score of 3, the board goes in state EP1 or EP2, and the game is finished. Note that all the processes components (transitions, event or states) are represented by observations. This model is not fair because in some case, the board may ask more questions to one player rather the other. To enable fairness, one can modify the design intuitively, or reuse a shared experience, represented as a problem case. Turn mechanism consists in memorizing the current entity that is authorized to do something. The authorized entity changes alternatively, thus, turn is a possible mechanism for fairness. As depicted in figure 3, a turn problem case contains a variable turn, representing the current turn memorized, and a mechanism to change the turn.

To combine turn with the current design, one relies on turn connection points called hooks. The turn problem case provides two hooks, one for changing the turn, and one for retrieving the turn variable. Combination can be achieved at the expense of updating the design and defining hypotheses of connection between the system design and turn problem case. Each connection between hooks are association with different semantics (causal, nature...).

The combination is a causal set of actions invoked from the Bi state. The turn change is invoked, then, a new turn value is retrieved, indicating the recipient for the next question. Since each question causes the change of the turn, fairness property is held.

This example presented how a problem case is defined, and how it can be combined with known problem cases to produce a new solution. In certain cases, when problem cases cannot be matched, combination through composition is impossible, and other mechanisms may be used. In the following section, we present the method and the various combinations mechanisms.

Method Steps

The step-wise method is presented by the activity diagram in figure 4. The method is reiterated until a satisfactory solution is achieved. (1) The problem is formulated as a set of properties and constraints (architectural, technical choices), according to the conceptual model of figure 1. For instance, "at the end of the game, each player has played the same number of times". (2) The problem is decomposed into subproblems, either known problems -called problem cases -selected from a knowledge base, or unknown situations. For instance, "a turn mechanism is used". (3) When the need for a concrete view occurs, we move towards the solution space. The potential solution elements are organized. For instance, "the turn problem case is introduced into the current solution". (4) We consider how to combine the selected problem cases together. This solution may be either composed [START_REF] Basili | Improve software quality by reusing knowledge and experience[END_REF] with other problem cases, applied as a pattern(6), or integrated(7) 3 . (8) At this point, we built a part of the expected solution; hence we are able to start a verification cycle. When abnormalities are observed, it triggers a diagnosis process. Verification results are tracked in the knowledge base. ( 9) Diagnosis reasoning process is performed, problem cases are used to enhance low-level observations, and the whole system provides the user with inference capabilities. The design is corrected, and the verification endeavor repeated. In some cases, the selected problem cases does not suit, hence we have to backtrack and rework the problem combination, and it might be useful to keep track of this failed attempt.

This step-wide method is repeated several times while useful components can be combined. The engineer is left with a reduced problem for which no known solution exist and where a classical design and verification activity has to be done.

The method performs roundtrips between two parts, the problem space, that consists in the problem elaboration, and the solution space, that consists in design and verifying the solution. While the problem elaboration produces specification to the solution design, the resulting solution produces expanded specifications (from design choices) to the problem space. This is similar to the Twin Peak proposal [START_REF] Hall | Relating software requirements and architectures using problem frames[END_REF], a software iterative development process that focuses on the combination of problem structures and solutions structures.

The method applicability is illustrated in the next section onto a mutual exclusion problem design.

Method Application: Alice and Bob Share a Yard

We borrow our example from an invited talk given by Leslie Lamport [START_REF] Lamport | Solved problems, unsolved problems and non-problems in concurrency[END_REF] about two neighbors, Alice and Bob. Alice and Bob share a yard, but also have dogs, and naturally they want to let the dogs use the yard. The problem is that these dogs don't like each other, and they fight, so only one dog at a time can be in the yard. In the rest of the article we will talk only about Alice and Bob nor their pets. To demonstrate how our method can be applied, we build this example from some initial requirements, and from a minimal set of domain knowledge.

Domain Description

We suppose that a knowledge base as been defined from previous experiences. In particular, it contains the following problems extracted from [START_REF] Lamport | The mutual exclusion problem: part Ia theory of interprocess communication[END_REF] [START_REF] Lamport | The mutual exclusion problem: partIIstatement and solutions[END_REF]. For improving the readability, the i-th property is named P i and each state (named Si) in a process (named PRi) is noted P Ri@Si.

A concurrent system problem is composed of asynchronous processes, noted P Ri. A basic property is that there be no deadlock; the set of processes must ensure the property noted P Deadlock.

In the mutual exclusion problem, each process of the collection, alternately executes a critical section noted PRi@CS and a noncritical section noted PRi@NCS. Two processes cannot execute their critical sections concurrently. A process structure is composed of the following states: -noncritical (P Ri@N CSi); -trying (P Ri@T i); -critical (P Ri@CSi); -exit (P Ri@Ei). Both processes in figure 5 conform to the structure. Mutual exclusion problem must ensure the following properties: (1) P M utex defined : "For any pair of distinct processes P Ri and P Rj, no pair of operation executions P Ri@CSi and P Ri@CSj are concurrent". Equivalent in LTL as ¬ P Ri@CS ∧ P Rj@CS. (2) P N olockout (starvation free): In every execution, if a process is in P Ri@T i, then later there is a configuration where the same process is in P Ri@CS. Because the mutual exclusion is a concurrent system problem, it must ensure P Deadlock. If there is a deadlock, it means that "one or more processes are trying to enter P Ri@CS, but no process ever does". There is also the possibility that a deadlock occurs because all the processes are stuck in their P Ri@T i statements.

First Solution

Problem Formalization The initial requirement are "Alice and Bob pets can reach the yard", and "Alice and Bob pets must not be together in the yard". The requirements are formalized as P 1 : (Alice@T rying → ♦Alice@Y ard), P 2 : (Bob@T rying → ♦Bob@Y ard), P 3 : ¬(Alice@Y ard ∧ Bob@Y ard). In the rest of the example, we omit P1 and P2.

Problem Decomposition Following the method, we decompose our problem and we look for known subproblems. The P3 formula structure is similar to the abstract formula of mutual exclusion, P M utex : ¬(P Ri@CS ∧ P Rj@CS), considering that PRi is Alice, PRj is Bob and CS is the Yard. We make the assumption that they address the same problem, and thus new properties emerge from this assumption, P Deadlock and P N oLockout, described as ¬ ♦(Alice@CS∨ Bob@CS).

Design and Pattern Application

The design is illustrated in figure 5. There are two processes Alice and Bob, and a shared variable Y ard. Both processes use the mutual exclusion structure, thus we apply this pattern.

Each process (Alice and Bob) conforms to the structure presented in section 4.1. The behavior is the following: Alice tries to access the yard (Alice@T rying); then Alice goes into the yard (Alice@Y ard), the Yard corresponds to the CS ; and finally exit the yard(Alice@Exit). The same goes for Bob.

Verification and Diagnosis

Verification can be done using several techniques such as static analysis, theorem proving, or model checking. The later is a formal technique that, given a formal model of the system and a set of properties, explores all possible system states in a brute-force manner [START_REF] Baier | Principles of model checking[END_REF]. If abnormalities are detected in the design, counter examples are produced, i.e a trace from the initial state to an unexpected situation. Then diagnosis is triggered based on the observations of such traces. We use a model checker to check exhaustively the properties for this model. P M utex is violated, indicating that Alice and Bob can be together in the yard at the same time. Since the structure of mutual exclusion problem is applied to Alice and Bob, each element of Alice and Bob can be understood from the point of view of mutual exclusion problem.

Second Solution -Turns

Problem Decomposition At this point, we need a mechanism to ensure the access to the critical section. Browsing the knowledge base, we can choose to pick the "turn" problem case. From the specification point of view, turn is defined by a (turn) variable, and two properties, P Change: after a process has finished its execution turn must be changed; P T urn: a process cannot be in execution if it is not its turn.

Design and Solution Integration

The turn case is used to alternate the yard access. The design is presented with the automata in figure 6. The turn mechanism has to be combined with Alice and Bob structure (N CS → T r → CS → Ex). We suppose that the combination is complex enough to require an ad hoc integration. The process that had the last access is stored, using the turn integer variable. A process checks the value of the turn variable in P Ri@T rying statement. If the value is equal to its personal turn, it is authorized to access the yard. Then, P Ri@Exit statement sets the turn variable to the other process.

Verification and Diagnosis

A new run is performed, the initial requirement P M utex is verified, but P N oLockout is violated.

Integration implies that the concepts of an integrated problem are widespread into the solution. Thus, parts of the problem are difficult to observe. According to the description of P N oLockout, "In every execution, if some processor is in Fig. 6. Automata for Alice and Bob using Turn the entry section in a configuration, then there is a later configuration in which that same processor is in the critical section". By analogy Bob is continuously in Bob@T rying state, and cannot pursue in the yard. Thus Bob has not the turn anymore, because Alice is never in Alice@T rying.

Problem Reformulation

Turn approach is formalized and stored in the knowledge base as follows. Turn is defined by a (turn) variable, followed by the properties: P Change: after P Ri@Exit, turn must be equals to 1 and After P Rj@Exit, turn must be equals to 0; P T urn: P Ri cannot be in the P Ri@CS if turn is not equals to 0 and P Rj cannot be in the P Rj@CS if turn is not equals to 1.

Using Flags

Problem Decomposition The turn problem case is interesting if we not consider the P N oLockout property. Another idea consists in sharing the intention of Alice and Bob to access the yard. This intention can be captured using two flags, one for Alice and one for Bob. A raised flag means that the person wants to go in the yard, and reciprocally, a lowered flag means the person doesn't want to.

Design of a new Solution

The new solution is based on an array named f lag of two booleans. The first boolean indicates if Alice want to access to the Alice@Y ard or not. The second boolean indicates if Bob want to access to the Bob@Y ard or not. Alice can access to the Y ard if and only if Bob hasn't raised his f lag. The same goes for Bob. When Alice or Bob are in the yard, he/she raises the f lag. Finally the f lag is lowered in the Exit state. The design is illustrated in figure 7. Suppose that Alice and Bob are interrupted in their T rying section. At this point each have claimed for entering in the yard but is not yet sure if the Yard is in use. Then each of them sees the f lag of the other one and wait. Each is waiting indefinitely for the other, a deadlock has occurred.

Flag Problem Formulation

We formulate the new approach using f lags. It contains an array of two boolean called f lags, and a set of following properties: (1) P Raise, P Ri raises its f lag in P Ri@CS state, and P Rj raises its f lag in P Rj@CS state; (2) P Lower, P Ri lower its f lag in P Ri@Exit state and P Rj lower its f lag in P Rj@Exit state;

(3) P W ait, P Ri cannot access P Ri@CS if f lag of P Rj is raised, and P Rj cannot access P Rj@CS if f lag of P Ri is true.

Taking Turns and Raising Flags

Problem Formulation Now, we decide to design a solution that solves all the problems mentioned above. We know that the property P M utex is fulfilled either with a turn or a flag. But the first solution violates PNolockout property, and the second violates PDeadlock property. We try to combine these problem cases together to fulfill all properties.

Design and Solution Integration Flag problem supposes that a flag raised by a process indicates its intention to enter in the critical section. Turn problem supposes a priority to enter in the critical section. We combine these two mechanisms; entering to the critical section is granted for P Ri if P Rj does not want to enter the critical section, or if P Rj has given up priority to P Ri by setting turn to P Ri. The design is given in figure 8. For readability sake, only the automaton of Alice is depicted.

Tool Support

This approach applies when problems and known solutions are available. It supposes to combine the method with appropriated tooling for creating, storing, querying and retrieving problem cases.

A Verification Organizing System

In a previous article [START_REF] Leilde | An Organizing System to Perform and Enable Verification and Diagnosis Activities[END_REF], we presented the Verification Organizing System (VOS) "an Organizing System is an intentionally arranged collection of resources and the interactions they support [START_REF] Glushko | Foundations for Organizing Systems. The Discipline of Organizing[END_REF]." The VOS is a three-layered infrastructure made of a storage tier, a knowledge tier, and an access tier.

The storage tier is characterized by a variety of sources, heterogeneous with respect to several dimensions concerning form and content properties. It is based on a Software Configuration Management (SCM) system that controls versioned artifacts produced. It includes no exhaustively verification endeavors (run, traces), properties or models, andproblem cases.

The knowledge tier, a logic-based, knowledge-rich level, plays the central role of a shared language to connect people to people, people to information, and information to information, represented as an ontology. It allows for knowledge creation, query and inference.

The access tier is used for diagnosis tools interoperability. Heterogeneous tools can interoperate by the underlying mechanism of model federation [START_REF] Guychard | Conceptual interoperability through Models Federation[END_REF].

These tools can be classified in three categories, model-based, process-historybased and interaction-based. Model-based tools assumes that a model of the system is available [START_REF] Reiter | A theory of diagnosis from first principles[END_REF] allowing to localize the subset of system's constituents generating abnormalities. Process history-based tools relies on the availability of large amount of historical process data, and thus, can be used for extracting knowledge [START_REF] Liu | AFChecker: Effective model checking for context-aware adaptive applications[END_REF], or reasoning [START_REF] Agnar | Case-Based Reasoning: Foundational Issues, Methodological Variations, and System Approaches[END_REF]. Interaction-based tools allow for observing, controlling, understanding and altering the system execution. Examples includes omniscient debuggers [START_REF] Pothier | Scalable omniscient debugging[END_REF], or visualization tools [START_REF] Hamou-Lhadj | A survey of trace exploration tools and techniques[END_REF].

Knowledge and Inference

Figure 9 illustrates the various artifacts produced at each step of the method. Problems (1) are progressively decomposed into other problem cases [START_REF] Alrajeh | Automated support for diagnosis and repair[END_REF]. Given the problem case structure, the organizing system can be used for querying and retrieving problems cases that are the most relevant. This may be achieved, for instance, according to three tasks, search, initially match, and select [START_REF] Agnar | Case-Based Reasoning: Foundational Issues, Methodological Variations, and System Approaches[END_REF]. Combining problem cases ( 4) is achieved with a certain level of automation. Composition (5) is the most automated way. Problem cases are on the shelf solutions connected through well defined connection points. For pattern application [START_REF] Bertoli | A symbolic model checking framework for safety analysis, diagnosis, and synthesis[END_REF], the degree of freedom lies in the rules of application between the problem pattern and the given solution. Integration (7) is a completely ad-hoc combination. [START_REF]Pattern-oriented software architecture: a system of patterns[END_REF] It shows how the previous combination techniques may affect the diagnosis task. Errors are represented with black stars. Composition mainly results in connections errors, pattern application mainly generates errors in the rules of pattern application, and integration may produce widespread errors. Finally, a solution is kept in the organizing system. It involves the selection of relevant information from the new problem case to keep.

Conclusion

Designing a solution for a given problem, and diagnosing possible faults in the proposed solution, are tedious tasks. It is mainly due to poorly understood problem, and poorly managed information, that results in a lack of diagnosis support and solution reuse. Our hypothesis is that a method is required for analyzing the current problem, storing relevant information, and reusing known solutions as much as possible. When a new solution is designed, for which abnormalities are observed, problem cases enhance the initial observations with more intelligible information. This work paves the way to the elaboration of problem-centered diagnosis tools, proposing adapted views and relevant checkpoints fostering the diagnosis activity.

Fig. 1 .

 1 Fig. 1. Problem conceptual model

Fig. 2 .

 2 Fig. 2. Initial problem, first design

Fig. 3 .

 3 Fig. 3. Simple problem, second design

Fig. 4 .

 4 Fig. 4. Method steps

Fig. 5 .

 5 Fig. 5. Automata for Alice and Bob 1

Fig. 7 .

 7 Fig. 7. Automata for Alice and Bob using Flag

Fig. 8 .

 8 Fig. 8. Automata for Alice and Bob using Flags and Turns Verification and Problem Reformulation It turns out that the whole set of properties are verified, thus the solution is acceptable. Finally, we formulate our problem of Alice and Bob sharing a yard, as a combination of Concurrent Process, Mutual Exclusion, Turn and Flag problem cases.

Fig. 9 .

 9 Fig. 9. Artifacts produced

Each kind of combination is represented with a particular arrow shape.