Search

Your search keyword '"Idir Ait Sadoune"' showing total 3 results
Start Over Author "Idir Ait Sadoune" Publisher springer international publishing
3 results on '"Idir Ait Sadoune"'

1. Formal Modelling of Domain Constraints in Event-B

Author

Linda Mohand-Oussaid, Idir Ait-Sadoune, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), and ANR-13-INSE-0001,IMPEX,Intégration des sémantiques implicite et explicite dans les développements de systèmes discrets fondés sur la preuve.(2013)

Subjects
formal specification, Event- B, Programming language, Computer science, Process (engineering), 020207 software engineering, 02 engineering and technology, Ontology (information science), computer.software_genre, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Domain (software engineering), System requirements, theorem proving, Transformation (function), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Formal specification, Domain constraints, 0202 electrical engineering, electronic engineering, information engineering, Domain knowledge, ontologies, 020201 artificial intelligence & image processing, Software system, computer
Abstract

International audience; When designing a hardware or a software system, the inte-gration of domain constraints becomes a determining factor to ensurea great match with the system requirements. This domain knowledge ismost often modelled using ontologies that allow to express the domaindata properties. In this paper, we propose an approach to integrate do-main ontologies into a system development process based on Event-B. Itconsists to annotate Event-B models using the ontology concepts, thisassumes a formalization of the domain ontology in the Event-B method.Therefore, we propose an extensible generic transformation approachwhich develops an Event-B specification based on an ontology describedin an ontological language. The integration of the Event-B descriptionof a domain ontology allows to constrain the system under design withthe domain ontology and to validate domain properties.

Published
2017
Full Text
View/download PDF

2. Semantic Heterogeneity in the Formal Development of Complex Systems: An Introduction

Author

Jean-Paul Gibson, Idir AIT SADOUNE, Marc Pantel, Département Logiciels et Réseaux (LOR), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP), Télécom SudParis (TSP), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, and Institut National Polytechnique (Toulouse) (Toulouse INP)

Subjects
020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, 020207 software engineering, 02 engineering and technology, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2016
Full Text
View/download PDF

3. Formal Modelling and Verification of Transactional Web Service Composition: A Refinement and Proof Approach with Event-B

Author

Idir Ait-Sadoune, Yamine Ait-Ameur, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, and Institut National Polytechnique (Toulouse) (Toulouse INP)

Subjects
Service (systems architecture), Computer science, Programming language, Event (computing), Semantics (computer science), computer.internet_protocol, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, 01 natural sciences, Business Process Execution Language, Transactional leadership, 010201 computation theory & mathematics, Programming language specification, 0202 electrical engineering, electronic engineering, information engineering, Web service, computer, Scope (computer science)
Abstract

Several languages for describing Web service compositions, like BPEL (Business Process Execution Language), make use of fault and compensation constructs to handle internal and/or external runtime errors of the composed service. This situation particularly occurs for transactional services. However, the absence of a rigorous definition of these BPEL constructors makes it difficult to correctly define the transactional behaviour of a BPEL process. The definitions of such constructs are usually given by their informal descriptions available in the standards. Our contribution proposes an approach to formally define the semantics of these operators. Thus, this paper presents a new Event-B semantics for formal modelling of Web service compositions that covers the scope, the fault and the compensation handlers introduced by the BPEL language specification. It also proposes a methodology showing how we can use Event-B method to design transactional BPEL processes. The proposed approach is illustrated by a case study.

Published
2015
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results