La Chronique du mois ou les Cahiers patriotiques de E. Clavière, C. Condorcet, L. Mercier, A. Auger, J. Oswald, N. Bonneville, J. Bidermann, A. Broussonet, A. Guy-Kersaint, J. P. Brissot, J. Ph. Garran de Coulon, J. Dussaulx, F. Lanthenas et Collot-d'Herbois

1792/05-09 (T3).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/10 (N11).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/02 (N3).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/08 (N8).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/06 (N7).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/03 (N4).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/01 (N2).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1896/12 (N1).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/05 (N6).

L'Image : revue artistique et littéraire ornée de figures sur bois, paraissant tous les mois / [secrétaire de la rédaction, Jules Rais ; administrateur, Tony Beltrand]

1897/09 (N10).

Reusable formal architectures for networked systems

Today's networked systems are becoming increasingly complex and diverse. The current simulation and runtime verification techniques do not provide support for developing such systems efficiently; moreover, the reliability of the simulated/verified systems is not thoroughly ensured. To address these challenges, the use of formal techniques to reason about network system development is growing, while at the same time, the mathematical background necessary for using formal techniques is a barrier for network designers to efficiently employ them. Thus, these techniques are not vastly used for developing networked systems. The objective of this thesis is to propose formal approaches for the development of reliable networked systems, by taking efficiency into account. With respect to reliability, we propose the architectural development of correct-by-construction networked system models. With respect to efficiency, we propose reusable network architectures as well as network development. At the core of our development methodology, we employ the abstraction and refinement techniques for the development and analysis of networked systems. We evaluate our proposal by employing the proposed architectures to a pervasive class of dynamic networks, i.e., wireless sensor network architectures as well as to a pervasive class of static networks, i.e., network-on-chip architectures. The ultimate goal of our research is to put forward the idea of building libraries of pre-proved rules for the efficient modelling, development, and analysis of networked systems. We take into account both qualitative and quantitative analysis of networks via varied formal tool support, using a theorem prover the Rodin platform and a statistical model checker the SMC-Uppaal.

Itinéraires de la correspondance d'Orient de Michaud et Poujolat, avec les différentes marches des croisés

Kartta kuuluu A. E. Nordenskiöldin kokoelmaan

Rigorous development of safety-critical systems

Nowadays, computer-based systems tend to become more complex and control increasingly critical functions affecting different areas of human activities. Failures of such systems might result in loss of human lives as well as significant damage to the environment. Therefore, their safety needs to be ensured. However, the development of safety-critical systems is not a trivial exercise. Hence, to preclude design faults and guarantee the desired behaviour, different industrial standards prescribe the use of rigorous techniques for development and verification of such systems. The more critical the system is, the more rigorous approach should be undertaken. To ensure safety of a critical computer-based system, satisfaction of the safety requirements imposed on this system should be demonstrated. This task involves a number of activities. In particular, a set of the safety requirements is usually derived by conducting various safety analysis techniques. Strong assurance that the system satisfies the safety requirements can be provided by formal methods, i.e., mathematically-based techniques. At the same time, the evidence that the system under consideration meets the imposed safety requirements might be demonstrated by constructing safety cases. However, the overall safety assurance process of critical computerbased systems remains insufficiently defined due to the following reasons. Firstly, there are semantic differences between safety requirements and formal models. Informally represented safety requirements should be translated into the underlying formal language to enable further veri cation. Secondly, the development of formal models of complex systems can be labour-intensive and time consuming. Thirdly, there are only a few well-defined methods for integration of formal verification results into safety cases. This thesis proposes an integrated approach to the rigorous development and verification of safety-critical systems that (1) facilitates elicitation of safety requirements and their incorporation into formal models, (2) simplifies formal modelling and verification by proposing specification and refinement patterns, and (3) assists in the construction of safety cases from the artefacts generated by formal reasoning. Our chosen formal framework is Event-B. It allows us to tackle the complexity of safety-critical systems as well as to structure safety requirements by applying abstraction and stepwise refinement. The Rodin platform, a tool supporting Event-B, assists in automatic model transformations and proof-based verification of the desired system properties. The proposed approach has been validated by several case studies from different application domains.

Formal development of resilient distributed systems

Resilience is the property of a system to remain trustworthy despite changes. Changes of a different nature, whether due to failures of system components or varying operational conditions, significantly increase the complexity of system development. Therefore, advanced development technologies are required to build robust and flexible system architectures capable of adapting to such changes. Moreover, powerful quantitative techniques are needed to assess the impact of these changes on various system characteristics. Architectural flexibility is achieved by embedding into the system design the mechanisms for identifying changes and reacting on them. Hence a resilient system should have both advanced monitoring and error detection capabilities to recognise changes as well as sophisticated reconfiguration mechanisms to adapt to them. The aim of such reconfiguration is to ensure that the system stays operational, i.e., remains capable of achieving its goals. Design, verification and assessment of the system reconfiguration mechanisms is a challenging and error prone engineering task. In this thesis, we propose and validate a formal framework for development and assessment of resilient systems. Such a framework provides us with the means to specify and verify complex component interactions, model their cooperative behaviour in achieving system goals, and analyse the chosen reconfiguration strategies. Due to the variety of properties to be analysed, such a framework should have an integrated nature. To ensure the system functional correctness, it should rely on formal modelling and verification, while, to assess the impact of changes on such properties as performance and reliability, it should be combined with quantitative analysis. To ensure scalability of the proposed framework, we choose Event-B as the basis for reasoning about functional correctness. Event-B is a statebased formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has a mature industrial-strength tool support { the Rodin platform. Proof-based verification as well as the reliance on abstraction and decomposition adopted in Event-B provides the designers with a powerful support for the development of complex systems. Moreover, the top-down system development by refinement allows the developers to explicitly express and verify critical system-level properties. Besides ensuring functional correctness, to achieve resilience we also need to analyse a number of non-functional characteristics, such as reliability and performance. Therefore, in this thesis we also demonstrate how formal development in Event-B can be combined with quantitative analysis. Namely, we experiment with integration of such techniques as probabilistic model checking in PRISM and discrete-event simulation in SimPy with formal development in Event-B. Such an integration allows us to assess how changes and di erent recon guration strategies a ect the overall system resilience. The approach proposed in this thesis is validated by a number of case studies from such areas as robotics, space, healthcare and cloud domain.