Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

Sorted by: relevance · author · university · dateNew search

You searched for +publisher:"Université Paris-Est" +contributor:("Frappier, Marc"). Showing records 1 – 2 of 2 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Fayolle, Thomas. Combinaison de méthodes formelles pour la spécification de systèmes industriels : Coupling of formal methods for industriel systems specification.

Degree: Docteur es, Informatique, 2017, Université Paris-Est

La spécification d’un système industriel nécessite la collaboration d’un ingénieur connaissant le système à modéliser et d’un ingénieur connaissant le langage de modélisation. L'utilisation d'un langage de spécification graphique, tel que les ASTD (Algebraic State Transition Diagram), permet de faciliter cette collaboration. Dans cette thèse, nous définissons une méthode de spécification graphique et formelle qui combine les ASTD avec les langages Event-B et B. L’ordonnancement des actions de la spécification est décrit par les ASTD et le modèle de données est décrit dans la spécification Event-B. La spécification B permet de vérifier la cohérence du modèle : les événements Event-B doivent pouvoir être exécutés lorsque les transitions associées doivent l’être. Un raffinement combiné des ASTD et d’Event-B permet la spécification incrémental du système. Afin de valider son apport, la méthode de spécification a été utilisée pour la spécification de cas d’études

Specifying industrial systems requires collaboration between an engineer that knows how the system works and an engineer that know the specification language. Graphical specification languages can help this collaboration. In this PhD Thesis a method is defined that combines ASTD (Algebraic State Transition Diagram), a formal graphical notation, with B and Event-B langagues. The ordering of actions is specified using ASTD and the data model is specified using Event-B. B specification is used to verify the consistency of the model : Event-B events have to be executed when the corresponding transitions have to be executed. A combined refinement allows to incrementaly design the system

Advisors/Committee Members: Laleau, Régine (thesis director), Frappier, Marc (thesis director).

Subjects/Keywords: Génie Logiciel; Méthodes Formelles; Système Ferroviaire; Software Engineering; Formal Methods; Railways Systems

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Fayolle, T. (2017). Combinaison de méthodes formelles pour la spécification de systèmes industriels : Coupling of formal methods for industriel systems specification. (Doctoral Dissertation). Université Paris-Est. Retrieved from http://www.theses.fr/2017PESC1078

Chicago Manual of Style (16th Edition):

Fayolle, Thomas. “Combinaison de méthodes formelles pour la spécification de systèmes industriels : Coupling of formal methods for industriel systems specification.” 2017. Doctoral Dissertation, Université Paris-Est. Accessed January 19, 2021. http://www.theses.fr/2017PESC1078.

MLA Handbook (7th Edition):

Fayolle, Thomas. “Combinaison de méthodes formelles pour la spécification de systèmes industriels : Coupling of formal methods for industriel systems specification.” 2017. Web. 19 Jan 2021.

Vancouver:

Fayolle T. Combinaison de méthodes formelles pour la spécification de systèmes industriels : Coupling of formal methods for industriel systems specification. [Internet] [Doctoral dissertation]. Université Paris-Est; 2017. [cited 2021 Jan 19]. Available from: http://www.theses.fr/2017PESC1078.

Council of Science Editors:

Fayolle T. Combinaison de méthodes formelles pour la spécification de systèmes industriels : Coupling of formal methods for industriel systems specification. [Doctoral Dissertation]. Université Paris-Est; 2017. Available from: http://www.theses.fr/2017PESC1078

2. Huynh, Nghi. Vérification et validation de politiques de contrôle d'accès dans le domaine médical : Verification and validation of healthcare access control policies.

Degree: Docteur es, Informatique, 2016, Université Paris-Est

Dans le domaine médical, la numérisation des documents et l’utilisation des dossiers patient électroniques (DPE, ou en anglais EHR pour Electronic Health Record) offrent de nombreux avantages, tels que le gain de place ou encore la facilité de recherche et de transmission de ces données. Les systèmes informatiques doivent reprendre ainsi progressivement le rôle traditionnellement tenu par les archivistes, rôle qui comprenait notamment la gestion des accès à ces données sensibles. Ces derniers doivent en effet être rigoureusement contrôlés pour tenir compte des souhaits de confidentialité des patients, des règles des établissements et de la législation en vigueur. SGAC, ou Solution de Gestion Automatisée du Consentement, a pour but de fournir une solution dans laquelle l’accès aux données du patient serait non seulement basée sur les règles mises en place par le patient lui-même mais aussi sur le règlement de l’établissement et sur la législation. Cependant, cette liberté octroyée au patient est source de divers problèmes : conflits, masquage des données nécessaires aux soins ou encore tout simplement erreurs de saisie. C’est pour cela que la vérification et la validation des règles d’accès sont cruciales : pour effectuer ces vérifications, les méthodes formelles fournissent des moyens fiables de vérification de propriétés tels que les preuves ou la vérification de modèles.Cette thèse propose des méthodes de vérification adaptées à SGAC pour le patient : elle introduit le modèle formel de SGAC, des méthodes de vérifications de propriétés telles l’accessibilité aux données ou encore la détection de document inaccessibles. Afin de mener ces vérifications de manière automatisée, SGAC est modélisé en B et Alloy ; ces différentes modélisations donnent accès aux outils Alloy et ProB, et ainsi à la vérification automatisée de propriétés via la vérification de modèles ou model checking

In healthcare, data digitization and the use of the Electronic Health Records (EHR) offer several benefits, such as reduction of the space occupied by data, or the ease of data search or data exchanges. IT systems must gradually act as the archivists who manage the access over sensitive data. Those have to be checked to be consistent with patient privacy wishes, hospital rules, and laws and regulations.SGAC, or Solution de Gestion Automatisée du Consentement, aims to offer a solution in which access to patient data would be based on patient rules, hospital rules and laws. However, the freedom granted to the patient can cause several problems: conflicts, hiding of the needed data to heal the patient or simply data-capture error. Therefore, verification and validation of policies are crucial: to conduct this verification, formal methods provide reliable ways to verify properties like proofs or model checking.This thesis provides verification methods applied on SGAC for the patient: it introduces the formal model of SGAC, verification methods of properties such as data reachability or hidden data detection. To conduct those verification in an…

Advisors/Committee Members: Laleau, Régine (thesis director), Frappier, Marc (thesis director), Mammar, Amel (thesis director).

Subjects/Keywords: Méthodes formelles; Vérification; Contrôle d'accès; Dmp; Médical; Formal methods; Verification; Access control; Ehr; Healthcare

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Huynh, N. (2016). Vérification et validation de politiques de contrôle d'accès dans le domaine médical : Verification and validation of healthcare access control policies. (Doctoral Dissertation). Université Paris-Est. Retrieved from http://www.theses.fr/2016PESC1042

Chicago Manual of Style (16th Edition):

Huynh, Nghi. “Vérification et validation de politiques de contrôle d'accès dans le domaine médical : Verification and validation of healthcare access control policies.” 2016. Doctoral Dissertation, Université Paris-Est. Accessed January 19, 2021. http://www.theses.fr/2016PESC1042.

MLA Handbook (7th Edition):

Huynh, Nghi. “Vérification et validation de politiques de contrôle d'accès dans le domaine médical : Verification and validation of healthcare access control policies.” 2016. Web. 19 Jan 2021.

Vancouver:

Huynh N. Vérification et validation de politiques de contrôle d'accès dans le domaine médical : Verification and validation of healthcare access control policies. [Internet] [Doctoral dissertation]. Université Paris-Est; 2016. [cited 2021 Jan 19]. Available from: http://www.theses.fr/2016PESC1042.

Council of Science Editors:

Huynh N. Vérification et validation de politiques de contrôle d'accès dans le domaine médical : Verification and validation of healthcare access control policies. [Doctoral Dissertation]. Université Paris-Est; 2016. Available from: http://www.theses.fr/2016PESC1042

.