-
Modeling and Analysis of the Landing Gear System with the Generalized Contracts
Authors:
Abdelkader Khouass,
christian attiogbé,
mohamed messabihi
Abstract:
Nowadays, there are several complex systems in different sectors such as aviation, air traffic control ...etc. These systems do not have a precise perimeter, they are open and made of various specific components built with different languages and environments. The modeling, assembly and analysis of such open and complex heterogeneous systems are challenges in software engineering. This paper descr…
▽ More
Nowadays, there are several complex systems in different sectors such as aviation, air traffic control ...etc. These systems do not have a precise perimeter, they are open and made of various specific components built with different languages and environments. The modeling, assembly and analysis of such open and complex heterogeneous systems are challenges in software engineering. This paper describes how the Minarets method decreases the difficulty of modeling, composition and analysis of the well known case study of the landing gear system. The method consists in: equipping individual components with generalized contracts that integrate various facets related to different concerns, composing these components according to their facets and verifying the resulting system with respect to the involved facets as well. The proposed method may be used or extended to cover more facets, and by strengthening assistance tool through proactive aspects in modeling, composing multi-facets contracts and finally the verification of the heterogeneous systems.
△ Less
Submitted 26 May, 2025; v1 submitted 19 November, 2021;
originally announced November 2021.
-
Multi-Facets Contract for Modeling and Verifying Heterogeneous Systems
Authors:
Abdelkader Khouass,
Christian Attiogbé,
Mohamed Messabihi
Abstract:
Critical and cyber-physical systems (CPS) that exist in large industries, such as nuclear power plants, railway, automotive or aeronautical industries are complex heterogeneous systems. They are complex because they are open, perimeter-less, often built by assembling various heterogeneous and interacting components which are frequently reconfigured due to requirements. Consequently, the modeling a…
▽ More
Critical and cyber-physical systems (CPS) that exist in large industries, such as nuclear power plants, railway, automotive or aeronautical industries are complex heterogeneous systems. They are complex because they are open, perimeter-less, often built by assembling various heterogeneous and interacting components which are frequently reconfigured due to requirements. Consequently, the modeling and analysis of such systems is a challenge in software engineering. We introduce a new method for modeling and verifying heterogeneous systems. The method consists in: equipping individual components with generalized contract, ordering these contracts according to given facets, composing these components and verifying the resulting system with respect to the facets. We illustrate the use of the method by a case study. The proposed method may be extended to cover more facets, and by strengthening assistance tool through proactive aspects in modelling and property verification.
△ Less
Submitted 26 May, 2021; v1 submitted 25 December, 2020;
originally announced December 2020.
-
Architectural Invariants and Correctness of IoT-based Systems
Authors:
Christian Attiogbé,
Jérôme Rocheteau
Abstract:
Internet of Things applications impact more and more industrial areas such as smart manufacturing, smart health monitoring and home automation; physical objects or devices equipped with sensors and actuators are interconnected and then controlled with software applications. Ensuring the correct construction, the well-functioning and the reliability of these applications constitute important issues…
▽ More
Internet of Things applications impact more and more industrial areas such as smart manufacturing, smart health monitoring and home automation; physical objects or devices equipped with sensors and actuators are interconnected and then controlled with software applications. Ensuring the correct construction, the well-functioning and the reliability of these applications constitute important issues for some of these applications which can be critical in case of dysfunction. We propose on the basis of the formal model of their common architectural properties, a generic framework for the formal modelling of IoT-based applications, the rigorous analysis of their consistency properties, their rigorous construction and evolution. Specific properties can be gradually added and checked. The proposed framework is then implemented and experimented using Event-B. We exploit the observation that the main requirements of the IoT-based physical architectures and control software are common to all IoT-based applications; this leaded us to the definition of the generic formal model together with invariant architectural and consistency properties. The proposed approach is generic, extensible, and can be profitably adapted to more general hybrid or cyber-physical systems. Our current implementation is independent of the formal model, it can be achieved in various other formal analysis environments.
△ Less
Submitted 18 December, 2019;
originally announced December 2019.
-
Building Correct SDN-Based Components from a Global Formal Mode
Authors:
Christian Attiogbé
Abstract:
Software Defined Networking (SDN) brings flexibility in the construction and managment of distributed applications by reducing the constraints imposed by physical networks and by moving the control of networks closer to the applications. However mastering SDN still poses numerous challenges among which the design of correct SDN components (more specifically controller and switches). In this work w…
▽ More
Software Defined Networking (SDN) brings flexibility in the construction and managment of distributed applications by reducing the constraints imposed by physical networks and by moving the control of networks closer to the applications. However mastering SDN still poses numerous challenges among which the design of correct SDN components (more specifically controller and switches). In this work we use a formal stepwise approach to model and reason on SDN. Although formal approaches have already been used in this area, this contribution is the first state-based approach; it is based on the Event-B formal method, and it enables a correct-by-construction of SDN components. We provide the steps to build, using several refinements, a global formal model of a SDN system; correct SDN components are then systematically built from the global formal model satisfying the desired properties. Event-B is used to experiment the approach.
△ Less
Submitted 25 June, 2018;
originally announced June 2018.
-
Modelling and Analysing the Landing Gear System: a Solution with Event-B/Rodin
Authors:
Pascal André,
Christian Attiogbé,
Arnaud Lanoix
Abstract:
This paper presents a solution to the landing gear system case study using Event-B and Rodin. We study the whole system (both the digital part and the controlled part). We use feature augmentation to build an abstract model of the whole system and structural refinement to detail more specifically the digital part. The required safety properties are formalised and proved. We propose a specific appr…
▽ More
This paper presents a solution to the landing gear system case study using Event-B and Rodin. We study the whole system (both the digital part and the controlled part). We use feature augmentation to build an abstract model of the whole system and structural refinement to detail more specifically the digital part. The required safety properties are formalised and proved. We propose a specific approach to deal with a family of reachability properties. The experimentations conducted during the study are supported by the Rodin tools. We show that the presented solution is systematic and it can be applied to similar case studies.
△ Less
Submitted 15 March, 2018;
originally announced March 2018.
-
Mastering Heterogeneous Behavioural Models
Authors:
J. Christian Attiogbé
Abstract:
Heterogeneity is one important feature of complex systems, leading to the complexity of their construction and analysis. Moving the heterogeneity at model level helps in mastering the difficulty of composing heterogeneous models which constitute a large system. We propose a method made of an algebra and structure morphisms to deal with the interaction of behavioural models, provided that they are…
▽ More
Heterogeneity is one important feature of complex systems, leading to the complexity of their construction and analysis. Moving the heterogeneity at model level helps in mastering the difficulty of composing heterogeneous models which constitute a large system. We propose a method made of an algebra and structure morphisms to deal with the interaction of behavioural models, provided that they are compatible. We prove that heterogeneous models can interact in a safe way, and therefore complex heterogeneous systems can be built and analysed incrementally. The Uppaal tool is targeted for experimentations.
△ Less
Submitted 21 July, 2017;
originally announced July 2017.
-
Dynamic Composition of Evolving Process Types
Authors:
Christian Attiogbé
Abstract:
Classical approaches like process algebras or labelled transition systems deal with static composition to model non-trivial concurrent or distributed systems; this is not sufficient for systems with dynamic architecture and with variable number of components. We introduce a method to guide the modelling and the dynamic composition of processes to build large distributed systems with dynamic adhoc…
▽ More
Classical approaches like process algebras or labelled transition systems deal with static composition to model non-trivial concurrent or distributed systems; this is not sufficient for systems with dynamic architecture and with variable number of components. We introduce a method to guide the modelling and the dynamic composition of processes to build large distributed systems with dynamic adhoc architecture. The modelling and the composition are based on an event-based approach that favour the decoupling of the system components. The composition uses the sharing of abstract communication channels. The method is appropriate to deal with evolving processes (with mobility, mutation). The event-B method is used for practical support. A fauna and its evolution are considered as a working system; this system presents some specificities, its behaviour is not foreseeable, it has an adhoc (not statically fixed) architecture.
△ Less
Submitted 25 December, 2011;
originally announced December 2011.
-
Multilevel Contracts for Trusted Components
Authors:
Mohamed Messabihi,
Pascal André,
Christian Attiogbé
Abstract:
This article contributes to the design and the verification of trusted components and services. The contracts are declined at several levels to cover then different facets, such as component consistency, compatibility or correctness. The article introduces multilevel contracts and a design+verification process for handling and analysing these contracts in component models. The approach is impleme…
▽ More
This article contributes to the design and the verification of trusted components and services. The contracts are declined at several levels to cover then different facets, such as component consistency, compatibility or correctness. The article introduces multilevel contracts and a design+verification process for handling and analysing these contracts in component models. The approach is implemented with the COSTO platform that supports the Kmelia component model. A case study illustrates the overall approach.
△ Less
Submitted 14 October, 2010;
originally announced October 2010.
-
Can Component/Service-Based Systems Be Proved Correct?
Authors:
Christian Attiogbe
Abstract:
Component-oriented and service-oriented approaches have gained a strong enthusiasm in industries and academia with a particular interest for service-oriented approaches. A component is a software entity with given functionalities, made available by a provider, and used to build other application within which it is integrated. The service concept and its use in web-based application development h…
▽ More
Component-oriented and service-oriented approaches have gained a strong enthusiasm in industries and academia with a particular interest for service-oriented approaches. A component is a software entity with given functionalities, made available by a provider, and used to build other application within which it is integrated. The service concept and its use in web-based application development have a huge impact on reuse practices. Accordingly a considerable part of software architectures is influenced; these architectures are moving towards service-oriented architectures. Therefore applications (re)use services that are available elsewhere and many applications interact, without knowing each other, using services available via service servers and their published interfaces and functionalities. Industries propose, through various consortium, languages, technologies and standards. More academic works are also undertaken concerning semantics and formalisation of components and service-based systems. We consider here both streams of works in order to raise research concerns that will help in building quality software. Are there new challenging problems with respect to service-based software construction? Besides, what are the links and the advances compared to distributed systems?
△ Less
Submitted 10 October, 2009;
originally announced October 2009.
-
Tool-Assisted Multi-Facet Analysis of Formal Specifications (Using Alelier-B and ProB)
Authors:
Christian Attiogbe
Abstract:
Tool-assisted analysis of software systems and convenient guides to practise the formal methods are still motivating challenges. This article addresses these challenges. We ex periment on analysing a formal specification from multiple aspects. The B method and the Atelier-B tool are used for formal specifications, for safety property analysis and for refinements. The ProB tool is used to supplem…
▽ More
Tool-assisted analysis of software systems and convenient guides to practise the formal methods are still motivating challenges. This article addresses these challenges. We ex periment on analysing a formal specification from multiple aspects. The B method and the Atelier-B tool are used for formal specifications, for safety property analysis and for refinements. The ProB tool is used to supplement the study with model checking; it helps to discover errors and there fore to improve the former specifications.
△ Less
Submitted 9 October, 2009;
originally announced October 2009.
-
Modelling and Analysing Dynamic Decentralised Systems
Authors:
Christian Attiogbe
Abstract:
We introduce a method to specify and analyse decentralised dynamic systems; the method is based on the combination of an event-based multi-process system specification approach with a multi-facet analysis approach that considers a reference abstract model and several specific ones derived from the abstract model in order to support facet-wise analysis. The method is illustrated with the modellin…
▽ More
We introduce a method to specify and analyse decentralised dynamic systems; the method is based on the combination of an event-based multi-process system specification approach with a multi-facet analysis approach that considers a reference abstract model and several specific ones derived from the abstract model in order to support facet-wise analysis. The method is illustrated with the modelling and the analysis of a mobile ad-hoc network. The Event-B framework and its related tools B4free and ProB are used to conduct the experiments.
△ Less
Submitted 26 September, 2009;
originally announced September 2009.
-
Semantic Embedding of Petri Nets into Event-B
Authors:
Christian Attiogbe
Abstract:
We present an embedding of Petri nets into B abstract systems. The embedding is achieved by translating both the static structure (modelling aspect) and the evolution semantics of Petri nets. The static structure of a Petri-net is captured within a B abstract system through a graph structure. This abstract system is then included in another abstract system which captures the evolution semantics…
▽ More
We present an embedding of Petri nets into B abstract systems. The embedding is achieved by translating both the static structure (modelling aspect) and the evolution semantics of Petri nets. The static structure of a Petri-net is captured within a B abstract system through a graph structure. This abstract system is then included in another abstract system which captures the evolution semantics of Petri-nets. The evolution semantics results in some B events depending on the chosen policies: basic nets or high level Petri nets. The current embedding enables one to use conjointly Petri nets and Event-B in the same system development, but at different steps and for various analysis.
△ Less
Submitted 24 October, 2005;
originally announced October 2005.
